let F, H be ZF-formula; :: thesis: Subformulae (H '&' F) = ((Subformulae H) \/ (Subformulae F)) \/ {(H '&' F)}

now :: thesis: for a being object holds
( ( a in Subformulae (H '&' F) implies a in ((Subformulae H) \/ (Subformulae F)) \/ {(H '&' F)} ) & ( a in ((Subformulae H) \/ (Subformulae F)) \/ {(H '&' F)} implies a in Subformulae (H '&' F) ) )

let a be object ; :: thesis: ( ( a in Subformulae (H '&' F) implies a in ((Subformulae H) \/ (Subformulae F)) \/ {(H '&' F)} ) & ( a in ((Subformulae H) \/ (Subformulae F)) \/ {(H '&' F)} implies a in Subformulae (H '&' F) ) )
A1: ( not a in (Subformulae H) \/ (Subformulae F) or a in Subformulae H or a in Subformulae F ) by XBOOLE_0:def 3;
thus ( a in Subformulae (H '&' F) implies a in ((Subformulae H) \/ (Subformulae F)) \/ {(H '&' F)} ) :: thesis: ( a in ((Subformulae H) \/ (Subformulae F)) \/ {(H '&' F)} implies a in Subformulae (H '&' F) )

proof

assume a in Subformulae (H '&' F) ; :: thesis: a in ((Subformulae H) \/ (Subformulae F)) \/ {(H '&' F)}
then consider G being ZF-formula such that
A2: G = a and
A3: G is_subformula_of H '&' F by Def42;

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 A3;
then ( G is_subformula_of H or G is_subformula_of F ) by Th70;
then ( a in Subformulae H or a in Subformulae F ) by A2, Def42;
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 A2, TARSKI:def 1;
hence a in ((Subformulae H) \/ (Subformulae F)) \/ {(H '&' F)} by XBOOLE_0:def 3; :: thesis: verum

end;

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 A5: a = H '&' F by TARSKI:def 1;
H '&' F is_subformula_of H '&' F by Th59;
hence a in Subformulae (H '&' F) by A5, Def42; :: thesis: verum

end;

A6: 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 ZF-formula such that
A7: G = a and
A8: G is_subformula_of F by Def42;
F is_immediate_constituent_of H '&' F ;
then F is_proper_subformula_of H '&' F by Th61;
then F is_subformula_of H '&' F ;
then G is_subformula_of H '&' F by A8, Th65;
hence a in Subformulae (H '&' F) by A7, Def42; :: thesis: verum

end;

A9: 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 ZF-formula such that
A10: G = a and
A11: G is_subformula_of H by Def42;
H is_immediate_constituent_of H '&' F ;
then H is_proper_subformula_of H '&' F by Th61;
then H is_subformula_of H '&' F ;
then G is_subformula_of H '&' F by A11, Th65;
hence a in Subformulae (H '&' F) by A10, Def42; :: thesis: verum

end;

assume a in ((Subformulae H) \/ (Subformulae F)) \/ {(H '&' F)} ; :: thesis: a in Subformulae (H '&' F)
hence a in Subformulae (H '&' F) by A1, A9, A6, A4, XBOOLE_0:def 3; :: thesis: verum

end;

hence Subformulae (H '&' F) = ((Subformulae H) \/ (Subformulae F)) \/ {(H '&' F)} by TARSKI:2; :: thesis: verum