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

proof

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

end;

let a be object ; :: according to TARSKI:def 3 :: thesis: ( not a in {(VERUM A)} or a in Subformulae (VERUM A) )
assume a in {(VERUM A)} ; :: thesis: a in Subformulae (VERUM A)
then a = VERUM A by TARSKI:def 1;
hence a in Subformulae (VERUM A) by Def22; :: thesis: verum