let A be QC-alphabet ; :: thesis: for H being Element of QC-WFF A holds
( H is_subformula_of FALSUM A iff ( H = FALSUM A or H = VERUM A ) )
let H be Element of QC-WFF A; :: thesis: ( H is_subformula_of FALSUM A iff ( H = FALSUM A or H = VERUM A ) )
thus ( not H is_subformula_of FALSUM A or H = FALSUM A or H = VERUM A ) :: thesis: ( ( H = FALSUM A or H = VERUM A ) implies H is_subformula_of FALSUM A )
proof
assume ( H is_subformula_of FALSUM A & H <> FALSUM A ) ; :: thesis: H = VERUM A
then H is_proper_subformula_of FALSUM A ;
then H is_subformula_of VERUM A by Th66;
hence H = VERUM A by Th79; :: thesis: verum
end;
VERUM A is_immediate_constituent_of FALSUM A ;
then VERUM A is_proper_subformula_of FALSUM A by Th53;
hence ( ( H = FALSUM A or H = VERUM A ) implies H is_subformula_of FALSUM A ) ; :: thesis: verum