thus Subformulae FALSUM c= {VERUM ,FALSUM } :: according to XBOOLE_0:def 10 :: thesis: {VERUM ,FALSUM } c= Subformulae FALSUM

proof

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

end;

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