for H being ZF-formula st H is being_equality holds
H = (Var1 H) '=' (Var2 H)