thus ( H is universal implies ex H1 being ZF-formula ex x being Variable st All x,H1 = H ) :: thesis: ( not H is universal implies ex b₁ being ZF-formula ex x being Variable st Ex x,b₁ = H )

proof

assume H is universal ; :: thesis: ex H1 being ZF-formula ex x being Variable st All x,H1 = H
then consider x being Variable, G being ZF-formula such that
A2: All x,G = H by Def14;
take G ; :: thesis: ex x being Variable st All x,G = H
thus ex x being Variable st All x,G = H by A2; :: thesis: verum

end;

thus ( not H is universal implies ex H1 being ZF-formula ex x being Variable st Ex x,H1 = H ) :: thesis: verum

proof

assume not H is universal ; :: thesis: ex H1 being ZF-formula ex x being Variable st Ex x,H1 = H
then consider x being Variable, G being ZF-formula such that
A3: Ex x,G = H by A1, Def23;
take G ; :: thesis: ex x being Variable st Ex x,G = H
thus ex x being Variable st Ex x,G = H by A3; :: thesis: verum

end;