let z, x, y be LD-EqClass; :: thesis: ( ex t, u being GRZ-formula st
( x = LD-EqClassOf t & y = LD-EqClassOf u & z = LD-EqClassOf (t '=' u) ) implies ex t, u being GRZ-formula st
( y = LD-EqClassOf t & x = LD-EqClassOf u & z = LD-EqClassOf (t '=' u) ) )
given t, u being GRZ-formula such that A1: ( x = LD-EqClassOf t & y = LD-EqClassOf u & z = LD-EqClassOf (t '=' u) ) ; :: thesis: ex t, u being GRZ-formula st
( y = LD-EqClassOf t & x = LD-EqClassOf u & z = LD-EqClassOf (t '=' u) )
take u ; :: thesis: ex u being GRZ-formula st
( y = LD-EqClassOf u & x = LD-EqClassOf u & z = LD-EqClassOf (u '=' u) )
take t ; :: thesis: ( y = LD-EqClassOf u & x = LD-EqClassOf t & z = LD-EqClassOf (u '=' t) )
u '=' t LD-= t '=' u ;
hence ( y = LD-EqClassOf u & x = LD-EqClassOf t & z = LD-EqClassOf (u '=' t) ) by A1, Th80; :: thesis: verum