let A be QC-alphabet ; :: thesis: for H being Element of QC-WFF A holds
( H is_subformula_of VERUM A iff H = VERUM A )
let H be Element of QC-WFF A; :: thesis: ( H is_subformula_of VERUM A iff H = VERUM A )
thus ( H is_subformula_of VERUM A implies H = VERUM A ) :: thesis: ( H = VERUM A implies H is_subformula_of VERUM A )

proof

assume A1: H is_subformula_of VERUM A ; :: thesis: H = VERUM A
assume H <> VERUM A ; :: thesis: contradiction
then H is_proper_subformula_of VERUM A by A1, Def21;
hence contradiction by Th64; :: thesis: verum

end;

thus ( H = VERUM A implies H is_subformula_of VERUM A ) ; :: thesis: verum