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

proof

let a be set ; :: according to TARSKI:def 3 :: thesis: ( not a in Subformulae VERUM or a in {VERUM } )
assume a in Subformulae VERUM ; :: thesis: a in {VERUM }
then consider F being Element of QC-WFF such that
A1: ( F = a & F is_subformula_of VERUM ) by Def23;
F = VERUM by A1, Th99;
hence a in {VERUM } by A1, TARSKI:def 1; :: thesis: verum

end;

let a be set ; :: according to TARSKI:def 3 :: thesis: ( not a in {VERUM } or a in Subformulae VERUM )
assume a in {VERUM } ; :: thesis: a in Subformulae VERUM
then ( a = VERUM & VERUM is_subformula_of VERUM ) by TARSKI:def 1;
hence a in Subformulae VERUM by Def23; :: thesis: verum