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;