let H be LTL-formula; :: thesis: for W being Subset of (Subformulae H) holds not {} in W
let W be Subset of (Subformulae H); :: thesis: not {} in W
assume {} in W ; :: thesis: contradiction
then ex F being LTL-formula st
( F = {} & F is_subformula_of H ) by MODELC_2:def 24;
hence contradiction by CARD_1:27, MODELC_2:3; :: thesis: verum