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

proof

assume ( H is_subformula_of FALSUM & H <> FALSUM ) ; :: thesis: H = VERUM
then H is_proper_subformula_of FALSUM by Def22;
then H is_subformula_of VERUM by Th86;
hence H = VERUM by Th99; :: thesis: verum

end;

VERUM is_immediate_constituent_of FALSUM by Def20;
then VERUM is_proper_subformula_of FALSUM by Th73;
hence ( ( H = FALSUM or H = VERUM ) implies H is_subformula_of FALSUM ) by Def22; :: thesis: verum