let H be Element of QC-WFF ; :: thesis: ( H is_subformula_of VERUM iff H = VERUM )
thus ( H is_subformula_of VERUM implies H = VERUM ) :: thesis: ( H = VERUM implies H is_subformula_of VERUM )

proof

assume A1: H is_subformula_of VERUM ; :: thesis: H = VERUM
assume H <> VERUM ; :: thesis: contradiction
then H is_proper_subformula_of VERUM by A1, Def22;
hence contradiction by Th58, Th75; :: thesis: verum

end;

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