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 consider F being LTL-formula such that
B1: ( F = {} & F is_subformula_of H ) by MODELC_2:def 24;
thus contradiction by B1, CARD_1:47, MODELC_2:3; :: thesis: verum