let A be QC-alphabet ; :: thesis: for H being Element of QC-WFF A
for x being bound_QC-variable of A holds Subformulae (All (x,H)) = (Subformulae H) \/ {(All (x,H))}
let H be Element of QC-WFF A; :: thesis: for x being bound_QC-variable of A holds Subformulae (All (x,H)) = (Subformulae H) \/ {(All (x,H))}
let x be bound_QC-variable of A; :: thesis: Subformulae (All (x,H)) = (Subformulae H) \/ {(All (x,H))}
thus Subformulae (All (x,H)) c= (Subformulae H) \/ {(All (x,H))} :: according to XBOOLE_0:def 10 :: thesis: (Subformulae H) \/ {(All (x,H))} c= Subformulae (All (x,H))
proof
let a be object ; :: according to TARSKI:def 3 :: thesis: ( not a in Subformulae (All (x,H)) or a in (Subformulae H) \/ {(All (x,H))} )
assume a in Subformulae (All (x,H)) ; :: thesis: a in (Subformulae H) \/ {(All (x,H))}
then consider F being Element of QC-WFF A such that
A1: F = a and
A2: F is_subformula_of All (x,H) by Def22;
now :: thesis: ( F <> All (x,H) implies a in Subformulae H )
assume F <> All (x,H) ; :: thesis: a in Subformulae H
then F is_proper_subformula_of All (x,H) by A2;
then F is_subformula_of H by Th71;
hence a in Subformulae H by A1, Def22; :: thesis: verum
end;
then ( a in Subformulae H or a in {(All (x,H))} ) by A1, TARSKI:def 1;
hence a in (Subformulae H) \/ {(All (x,H))} by XBOOLE_0:def 3; :: thesis: verum
end;
let a be object ; :: according to TARSKI:def 3 :: thesis: ( not a in (Subformulae H) \/ {(All (x,H))} or a in Subformulae (All (x,H)) )
assume A3: a in (Subformulae H) \/ {(All (x,H))} ; :: thesis: a in Subformulae (All (x,H))
A4: now :: thesis: ( a in Subformulae H implies a in Subformulae (All (x,H)) )
assume a in Subformulae H ; :: thesis: a in Subformulae (All (x,H))
then consider F being Element of QC-WFF A such that
A5: F = a and
A6: F is_subformula_of H by Def22;
H is_immediate_constituent_of All (x,H) ;
then H is_proper_subformula_of All (x,H) by Th53;
then H is_subformula_of All (x,H) ;
then F is_subformula_of All (x,H) by A6, Th57;
hence a in Subformulae (All (x,H)) by A5, Def22; :: thesis: verum
end;
now :: thesis: ( a in {(All (x,H))} implies a in Subformulae (All (x,H)) )
assume a in {(All (x,H))} ; :: thesis: a in Subformulae (All (x,H))
then a = All (x,H) by TARSKI:def 1;
hence a in Subformulae (All (x,H)) by Def22; :: thesis: verum
end;
hence a in Subformulae (All (x,H)) by A3, A4, XBOOLE_0:def 3; :: thesis: verum