Axiom ax_e1 ≪ | index | src | ≫

axiom ax_e1 {x: set}: $ \fo x x \eq x $;