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

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

A2: now

assume A3: G '&' H = 'not' F ; :: thesis: contradiction
( (G '&' H) . 1 = 3 & ('not' F) . 1 = 2 ) by Th33, FINSEQ_1:58;
hence contradiction by A3; :: thesis: verum

end;

now

given x being Variable such that A4: G '&' H = All x,F ; :: thesis: contradiction
( (G '&' H) . 1 = 3 & (All x,F) . 1 = 4 ) by Th33, Th34;
hence contradiction by A4; :: thesis: verum

end;

then ex H1 being ZF-formula st
( G '&' H = F '&' H1 or G '&' H = H1 '&' F ) by A1, A2, Def39;
hence ( F = G or F = H ) by Th47; :: 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 by Def39; :: thesis: verum