let A be QC-alphabet ; 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; 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; ( F is_immediate_constituent_of All (x,H) iff F = H )
thus
( F is_immediate_constituent_of All (x,H) implies F = H )
( 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) )
;
QC_LANG2:def 19 F = H
hence
F = H
by A2, A3, Th5;
verum
end;
thus
( F = H implies F is_immediate_constituent_of All (x,H) )
; verum