let A be QC-alphabet ; :: thesis: Subformulae (FALSUM A) = {(VERUM A),(FALSUM A)}
thus Subformulae (FALSUM A) c= {(VERUM A),(FALSUM A)} :: according to XBOOLE_0:def 10 :: thesis: {(VERUM A),(FALSUM A)} c= Subformulae (FALSUM A)

proof

let a be object ; :: according to TARSKI:def 3 :: thesis: ( not a in Subformulae (FALSUM A) or a in {(VERUM A),(FALSUM A)} )
assume a in Subformulae (FALSUM A) ; :: thesis: a in {(VERUM A),(FALSUM A)}
then ex F being Element of QC-WFF A st
( F = a & F is_subformula_of FALSUM A ) by Def22;
then ( a = FALSUM A or a = VERUM A ) by Th81;
hence a in {(VERUM A),(FALSUM A)} by TARSKI:def 2; :: thesis: verum

end;

let a be object ; :: according to TARSKI:def 3 :: thesis: ( not a in {(VERUM A),(FALSUM A)} or a in Subformulae (FALSUM A) )
assume A1: a in {(VERUM A),(FALSUM A)} ; :: thesis: a in Subformulae (FALSUM A)
then A2: ( a = VERUM A or a = FALSUM A ) by TARSKI:def 2;
reconsider a = a as Element of QC-WFF A by A1, TARSKI:def 2;
a is_subformula_of FALSUM A by A2, Th81;
hence a in Subformulae (FALSUM A) by Def22; :: thesis: verum