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) ) ;
(x 'in' y) . 1 = 1 by Th15;
hence contradiction by A1, Th16, Th17, FINSEQ_1:41; :: thesis: verum