theorem Th36: :: ZF_LANG:36

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