let t be GRZ-formula; :: thesis: ( t is conjunctive iff ex u, v being GRZ-formula st t = u '&' v )
thus ( t is conjunctive 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 conjunctive )

proof

assume t is conjunctive ; :: 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 conjunctive ) by Th4, POLNOT_1:83; :: thesis: verum