let A be QC-alphabet ; :: thesis: for F, H being Element of QC-WFF A holds Subformulae (H '&' F) = ((Subformulae H) \/ (Subformulae F)) \/ {(H '&' F)}
let F, H be Element of QC-WFF A; :: thesis: Subformulae (H '&' F) = ((Subformulae H) \/ (Subformulae F)) \/ {(H '&' F)}
thus Subformulae (H '&' F) c= ((Subformulae H) \/ (Subformulae F)) \/ {(H '&' F)} :: according to XBOOLE_0:def 10 :: thesis: ((Subformulae H) \/ (Subformulae F)) \/ {(H '&' F)} c= Subformulae (H '&' F)

proof

let a be object ; :: according to TARSKI:def 3 :: thesis: ( not a in Subformulae (H '&' F) or a in ((Subformulae H) \/ (Subformulae F)) \/ {(H '&' F)} )
assume a in Subformulae (H '&' F) ; :: thesis: a in ((Subformulae H) \/ (Subformulae F)) \/ {(H '&' F)}
then consider G being Element of QC-WFF A such that
A1: G = a and
A2: G is_subformula_of H '&' F by Def22;

now :: thesis: ( G <> H '&' F implies a in (Subformulae H) \/ (Subformulae F) )

assume G <> H '&' F ; :: thesis: a in (Subformulae H) \/ (Subformulae F)
then G is_proper_subformula_of H '&' F by A2;
then ( G is_subformula_of H or G is_subformula_of F ) by Th69;
then ( a in Subformulae H or a in Subformulae F ) by A1, Def22;
hence a in (Subformulae H) \/ (Subformulae F) by XBOOLE_0:def 3; :: thesis: verum

end;

then ( a in (Subformulae H) \/ (Subformulae F) or a in {(H '&' F)} ) by A1, TARSKI:def 1;
hence a in ((Subformulae H) \/ (Subformulae F)) \/ {(H '&' F)} by XBOOLE_0:def 3; :: thesis: verum

end;

let a be object ; :: according to TARSKI:def 3 :: thesis: ( not a in ((Subformulae H) \/ (Subformulae F)) \/ {(H '&' F)} or a in Subformulae (H '&' F) )
assume A3: a in ((Subformulae H) \/ (Subformulae F)) \/ {(H '&' F)} ; :: thesis: a in Subformulae (H '&' F)

A4: now :: thesis: ( a in {(H '&' F)} implies a in Subformulae (H '&' F) )

assume a in {(H '&' F)} ; :: thesis: a in Subformulae (H '&' F)
then a = H '&' F by TARSKI:def 1;
hence a in Subformulae (H '&' F) by Def22; :: thesis: verum

end;

A5: now :: thesis: ( a in Subformulae F implies a in Subformulae (H '&' F) )

assume a in Subformulae F ; :: thesis: a in Subformulae (H '&' F)
then consider G being Element of QC-WFF A such that
A6: G = a and
A7: G is_subformula_of F by Def22;
F is_immediate_constituent_of H '&' F ;
then F is_proper_subformula_of H '&' F by Th53;
then F is_subformula_of H '&' F ;
then G is_subformula_of H '&' F by A7, Th57;
hence a in Subformulae (H '&' F) by A6, Def22; :: thesis: verum

end;

A8: now :: thesis: ( a in Subformulae H implies a in Subformulae (H '&' F) )

assume a in Subformulae H ; :: thesis: a in Subformulae (H '&' F)
then consider G being Element of QC-WFF A such that
A9: G = a and
A10: G is_subformula_of H by Def22;
H is_immediate_constituent_of H '&' F ;
then H is_proper_subformula_of H '&' F by Th53;
then H is_subformula_of H '&' F ;
then G is_subformula_of H '&' F by A10, Th57;
hence a in Subformulae (H '&' F) by A9, Def22; :: thesis: verum

end;

( not a in (Subformulae H) \/ (Subformulae F) or a in Subformulae H or a in Subformulae F ) by XBOOLE_0:def 3;
hence a in Subformulae (H '&' F) by A3, A8, A5, A4, XBOOLE_0:def 3; :: thesis: verum