let F, H be LTL-formula; :: thesis: ( F is_subformula_of H implies Subformulae F c= Subformulae H )
assume A1: F is_subformula_of H ; :: thesis: Subformulae F c= Subformulae H
let a be set ; :: according to TARSKI:def 3 :: thesis: ( not a in Subformulae F or a in Subformulae H )
assume a in Subformulae F ; :: thesis: a in Subformulae H
then consider F1 being LTL-formula such that
A2: ( F1 = a & F1 is_subformula_of F ) by Def103;
F1 is_subformula_of H by A1, A2, Th121;
hence a in Subformulae H by A2, Def103; :: thesis: verum