let A be QC-alphabet ; :: thesis: for F, H being Element of QC-WFF A
for x being bound_QC-variable of A holds
( F is_immediate_constituent_of All (x,H) iff F = H )
let F, H be Element of QC-WFF A; :: thesis: for x being bound_QC-variable of A holds
( F is_immediate_constituent_of All (x,H) iff F = H )
let x be bound_QC-variable of A; :: 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 ;
then A1: ((@ (All (x,H))) . 1) `1 = 3 by QC_LANG1:18;
A2: All (x,H) <> 'not' F by A1, QC_LANG1:18, QC_LANG1:def 19;
A3: for G being Element of QC-WFF A holds
( not All (x,H) = F '&' G & not All (x,H) = G '&' F ) by A1, QC_LANG1:18, QC_LANG1:def 20;
assume ( All (x,H) = 'not' F or ex H1 being Element of QC-WFF A st
( All (x,H) = F '&' H1 or All (x,H) = H1 '&' F ) or ex y being bound_QC-variable of A st All (x,H) = All (y,F) ) ; :: according to QC_LANG2:def 19 :: thesis: F = H
hence F = H by A2, A3, Th5; :: thesis: verum
end;
thus ( F = H implies F is_immediate_constituent_of All (x,H) ) ; :: thesis: verum