let x, y be Variable; :: thesis: for H being ZF-formula holds not H is_immediate_constituent_of x '=' y
let H be ZF-formula; :: thesis: not H is_immediate_constituent_of x '=' y
assume H is_immediate_constituent_of x '=' y ; :: thesis: contradiction
then A1: ( x '=' y = 'not' H or ex H1 being ZF-formula st
( x '=' y = H '&' H1 or x '=' y = H1 '&' H ) or ex z being Variable st x '=' y = All z,H ) by Def39;
A2: ( (x '=' y) . 1 = 0 & ('not' H) . 1 = 2 ) by Th31, FINSEQ_1:58;
then consider z being Variable such that
A3: x '=' y = All z,H by A1, Th33;
thus contradiction by A2, A3, Th34; :: thesis: verum