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
A3: WFF \ {H} is non empty set

proof

A4: (x. 0 ) '=' (x. 1) in WFF by Def8;
(x. 0 ) '=' (x. 1) <> H by A2, Def10;
then not (x. 0 ) '=' (x. 1) in {H} by TARSKI:def 1;
hence WFF \ {H} is non empty set by A4, XBOOLE_0:def 5; :: thesis: verum

end;

A5: for a being set st a in WFF \ {H} holds
a is FinSequence of NAT by Def8;

A6: now

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

end;

A9: now

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

end;

A12: now

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

end;

now

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 A15: p in WFF \ {H} ; :: thesis: All x,p in WFF \ {H}
then A16: All x,p in WFF by Def8;
reconsider H1 = p as ZF-formula by A15, Def9;
All x,H1 <> H by A2, Def14;
then not All x,p in {H} by TARSKI:def 1;
hence All x,p in WFF \ {H} by A16, XBOOLE_0:def 5; :: thesis: verum

end;

then WFF c= WFF \ {H} by A3, A5, A6, A9, A12, Def8;
then H in WFF \ {H} by A1, TARSKI:def 3;
then ( not H in {H} & H in {H} ) by TARSKI:def 1, XBOOLE_0:def 5;
hence contradiction ; :: thesis: verum