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