thus ( H is conjunctive implies ex G, H1 being ZF-formula st H1 '&' G = H ) :: thesis: ( not H is conjunctive implies ex b₁, H1 being ZF-formula st H1 'or' b₁ = H )

proof

assume H is conjunctive ; :: thesis: ex G, H1 being ZF-formula st H1 '&' G = H
then consider G, F being ZF-formula such that
A2: G '&' F = H by Def13;
take F ; :: thesis: ex H1 being ZF-formula st H1 '&' F = H
thus ex H1 being ZF-formula st H1 '&' F = H by A2; :: thesis: verum

end;

thus ( not H is conjunctive implies ex G, H1 being ZF-formula st H1 'or' G = H ) :: thesis: verum

proof

assume not H is conjunctive ; :: thesis: ex G, H1 being ZF-formula st H1 'or' G = H
then consider G, F being ZF-formula such that
A3: G 'or' F = H by A1, Def20;
take F ; :: thesis: ex H1 being ZF-formula st H1 'or' F = H
thus ex H1 being ZF-formula st H1 'or' F = H by A3; :: thesis: verum

end;