let t be GRZ-formula; :: thesis: ( t is being_equality iff ex u, v being GRZ-formula st t = u '=' v )
thus ( t is being_equality implies ex u, v being GRZ-formula st t = u '=' v ) :: thesis: ( ex u, v being GRZ-formula st t = u '=' v implies t is being_equality )
proof
assume t is being_equality ; :: thesis: ex u, v being GRZ-formula st t = u '=' v
then consider u, v being GRZ-formula such that
A3: t = (Polish-binOp (GRZ-symbols,GRZ-arity,'=')) . (u,v) by Th4, POLNOT_1:82;
take u ; :: thesis: ex v being GRZ-formula st t = u '=' v
take v ; :: thesis: t = u '=' v
thus t = u '=' v by A3; :: thesis: verum
end;
thus ( ex u, v being GRZ-formula st t = u '=' v implies t is being_equality ) by Th4, POLNOT_1:83; :: thesis: verum