let F, G, H be ZF-formula; :: thesis: ( F is_immediate_constituent_of G '&' H iff ( F = G or F = H ) )
thus ( not F is_immediate_constituent_of G '&' H or F = G or F = H ) :: thesis: ( ( F = G or F = H ) implies F is_immediate_constituent_of G '&' H )

proof

A1: now :: thesis: for x being Variable holds not G '&' H = All (x,F)

given x being Variable such that A2: G '&' H = All (x,F) ; :: thesis: contradiction
(G '&' H) . 1 = 3 by Th16;
hence contradiction by A2, Th17; :: thesis: verum

end;

A3: now :: thesis: not G '&' H = 'not' F

assume A4: G '&' H = 'not' F ; :: thesis: contradiction
(G '&' H) . 1 = 3 by Th16;
hence contradiction by A4, FINSEQ_1:41; :: thesis: verum

end;

assume F is_immediate_constituent_of G '&' H ; :: thesis: ( F = G or F = H )
then ex H1 being ZF-formula st
( G '&' H = F '&' H1 or G '&' H = H1 '&' F ) by A3, A1;
hence ( F = G or F = H ) by Th30; :: thesis: verum

end;

assume ( F = G or F = H ) ; :: thesis: F is_immediate_constituent_of G '&' H
hence F is_immediate_constituent_of G '&' H ; :: thesis: verum