let F, G, H be Element of QC-WFF ; :: 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: ( G '&' H = 'not' F or ex H1 being Element of QC-WFF st
( G '&' H = F '&' H1 or G '&' H = H1 '&' F ) or ex x being bound_QC-variable st G '&' H = All x,F ) ; :: according to QC_LANG2:def 20 :: thesis: ( F = G or F = H )
G '&' H is conjunctive by QC_LANG1:def 19;
then A2: ((@ (G '&' H)) . 1) `1 = 2 by QC_LANG1:49;

A3: now

assume A4: G '&' H = 'not' F ; :: thesis: contradiction
'not' F is negative by QC_LANG1:def 18;
hence contradiction by A2, A4, QC_LANG1:49; :: thesis: verum

end;

now

given x being bound_QC-variable such that A5: G '&' H = All x,F ; :: thesis: contradiction
All x,F is universal by QC_LANG1:def 20;
hence contradiction by A2, A5, QC_LANG1:49; :: thesis: verum

end;

hence ( F = G or F = H ) by A1, A3, Th3; :: 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 Def20; :: thesis: verum