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 and
A2: F is_subformula_of VERUM by Def23;
F = VERUM by A2, 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 by TARSKI:def 1;
hence a in Subformulae VERUM by Def23; :: thesis: verum