let F, H be Element of QC-WFF ; :: thesis: for x being bound_QC-variable holds
( F is_immediate_constituent_of All (x,H) iff F = H )
let x be bound_QC-variable; :: thesis: ( F is_immediate_constituent_of All (x,H) iff F = H )
thus ( F is_immediate_constituent_of All (x,H) implies F = H ) :: thesis: ( F = H implies F is_immediate_constituent_of All (x,H) )

proof

All (x,H) is universal by QC_LANG1:def 19;
then A1: ((@ (All (x,H))) . 1) `1 = 3 by QC_LANG1:16;

A2: now

A3: 'not' F is negative by QC_LANG1:def 17;
assume All (x,H) = 'not' F ; :: thesis: contradiction
hence contradiction by A1, A3, QC_LANG1:16; :: thesis: verum

end;

A4: now

given G being Element of QC-WFF such that A5: ( All (x,H) = F '&' G or All (x,H) = G '&' F ) ; :: thesis: contradiction
( F '&' G is conjunctive & G '&' F is conjunctive ) by QC_LANG1:def 18;
hence contradiction by A1, A5, QC_LANG1:16; :: thesis: verum

end;

assume ( All (x,H) = 'not' F or ex H1 being Element of QC-WFF st
( All (x,H) = F '&' H1 or All (x,H) = H1 '&' F ) or ex y being bound_QC-variable st All (x,H) = All (y,F) ) ; :: according to QC_LANG2:def 19 :: thesis: F = H
hence F = H by A2, A4, Th6; :: thesis: verum

end;

thus ( F = H implies F is_immediate_constituent_of All (x,H) ) by Def20; :: thesis: verum