let H be ZF-formula; :: thesis: ( H is being_equality or H is being_membership or H is negative or H is conjunctive or H is universal )
A1: H is Element of WFF by Def9;
assume A2: ( not H is being_equality & not H is being_membership & not H is negative & not H is conjunctive & not H is universal ) ; :: thesis: contradiction
then (x. 0) '=' (x. 1) <> H ;
then A3: not (x. 0) '=' (x. 1) in {H} by TARSKI:def 1;

A4: now :: thesis: for x, y being Variable holds
( x '=' y in WFF \ {H} & x 'in' y in WFF \ {H} )

let x, y be Variable; :: thesis: ( x '=' y in WFF \ {H} & x 'in' y in WFF \ {H} )
x '=' y <> H by A2;
then A5: not x '=' y in {H} by TARSKI:def 1;
x '=' y in WFF by Def8;
hence x '=' y in WFF \ {H} by A5, XBOOLE_0:def 5; :: thesis: x 'in' y in WFF \ {H}
x 'in' y <> H by A2;
then A6: not x 'in' y in {H} by TARSKI:def 1;
x 'in' y in WFF by Def8;
hence x 'in' y in WFF \ {H} by A6, XBOOLE_0:def 5; :: thesis: verum

end;

A7: now :: thesis: for x being Variable
for p being FinSequence of NAT st p in WFF \ {H} holds
All (x,p) in WFF \ {H}

let x be Variable; :: thesis: for p being FinSequence of NAT st p in WFF \ {H} holds
All (x,p) in WFF \ {H}
let p be FinSequence of NAT ; :: thesis: ( p in WFF \ {H} implies All (x,p) in WFF \ {H} )
assume A8: p in WFF \ {H} ; :: thesis: All (x,p) in WFF \ {H}
then reconsider H1 = p as ZF-formula by Def9;
All (x,H1) <> H by A2;
then A9: not All (x,p) in {H} by TARSKI:def 1;
All (x,p) in WFF by A8, Def8;
hence All (x,p) in WFF \ {H} by A9, XBOOLE_0:def 5; :: thesis: verum

end;

A10: now :: thesis: for p, q being FinSequence of NAT st p in WFF \ {H} & q in WFF \ {H} holds
p '&' q in WFF \ {H}

let p, q be FinSequence of NAT ; :: thesis: ( p in WFF \ {H} & q in WFF \ {H} implies p '&' q in WFF \ {H} )
assume A11: ( p in WFF \ {H} & q in WFF \ {H} ) ; :: thesis: p '&' q in WFF \ {H}
then reconsider F = p, G = q as ZF-formula by Def9;
F '&' G <> H by A2;
then A12: not p '&' q in {H} by TARSKI:def 1;
p '&' q in WFF by A11, Def8;
hence p '&' q in WFF \ {H} by A12, XBOOLE_0:def 5; :: thesis: verum

end;

A13: now :: thesis: for p being FinSequence of NAT st p in WFF \ {H} holds
'not' p in WFF \ {H}

let p be FinSequence of NAT ; :: thesis: ( p in WFF \ {H} implies 'not' p in WFF \ {H} )
assume A14: p in WFF \ {H} ; :: thesis: 'not' p in WFF \ {H}
then reconsider H1 = p as ZF-formula by Def9;
'not' H1 <> H by A2;
then A15: not 'not' p in {H} by TARSKI:def 1;
'not' p in WFF by A14, Def8;
hence 'not' p in WFF \ {H} by A15, XBOOLE_0:def 5; :: thesis: verum

end;

(x. 0) '=' (x. 1) in WFF by Def8;
then A16: WFF \ {H} is non empty set by A3, XBOOLE_0:def 5;
for a being set st a in WFF \ {H} holds
a is FinSequence of NAT by Def8;
then WFF c= WFF \ {H} by A16, A4, A13, A10, A7, Def8;
then H in WFF \ {H} by A1;
then not H in {H} by XBOOLE_0:def 5;
hence contradiction by TARSKI:def 1; :: thesis: verum