let A be QC-alphabet ; :: thesis: for F, G, H being Element of QC-WFF A holds
( F is_immediate_constituent_of G '&' H iff ( F = G or F = H ) )
let F, G, H be Element of QC-WFF A; :: 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

G '&' H is conjunctive ;
then A1: ((@ (G '&' H)) . 1) `1 = 2 by QC_LANG1:18;
A2: G '&' H <> 'not' F by A1, QC_LANG1:18, QC_LANG1:def 19;
A3: for x being bound_QC-variable of A holds not G '&' H = All (x,F) by A1, QC_LANG1:18, QC_LANG1:def 21;
assume ( G '&' H = 'not' F or ex H1 being Element of QC-WFF A st
( G '&' H = F '&' H1 or G '&' H = H1 '&' F ) or ex x being bound_QC-variable of A st G '&' H = All (x,F) ) ; :: according to QC_LANG2:def 19 :: thesis: ( F = G or F = H )
hence ( F = G or F = H ) by A2, A3, Th2; :: 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