defpred S₁[ Element of LTL_axioms ] means ( $1 is LTL_TAUT_OF_PL or $1 is axltl1 or $1 is axltl1a or $1 is axltl2 or $1 is axltl3 or $1 is axltl4 or $1 is axltl5 or $1 is axltl6 );
set X = { p where p is Element of LTL_axioms : S₁[p] } ;
{ p where p is Element of LTL_axioms : S₁[p] } c= LTLB_WFF

let x be object ; :: according to TARSKI:def 3 :: thesis:
assume x in { p where p is Element of LTL_axioms : S₁[p] } ; :: thesis:
then ex p being Element of LTL_axioms st
( x = p & S₁[p] ) ;
hence x in LTLB_WFF ; :: thesis:

end;

then reconsider X = { p where p is Element of LTL_axioms : S₁[p] } as Subset of LTLB_WFF ;
let A be Element of LTL_axioms ; :: thesis:
X is with_LTL_axioms

end;

end;

end;

thus ('X' (p => q)) => (('X' p) => ('X' q)) in X :: thesis:

reconsider pp = ('X' (p => q)) => (('X' p) => ('X' q)) as Element of LTL_axioms by Def17;
S₁[pp] by Def24;
hence ('X' (p => q)) => (('X' p) => ('X' q)) in X ; :: thesis:

end;

reconsider pp = ('G' p) => (p '&&' ('X' ('G' p))) as Element of LTL_axioms by Def17;
S₁[pp] by Def25;
hence ('G' p) => (p '&&' ('X' ('G' p))) in X ; :: thesis:

end;

reconsider pp = (p 'U' q) => (('X' q) 'or' ('X' (p '&&' (p 'U' q)))) as Element of LTL_axioms by Def17;
S₁[pp] by Def26;
hence (p 'U' q) => (('X' q) 'or' ('X' (p '&&' (p 'U' q)))) in X ; :: thesis:

end;

thus (('X' q) 'or' ('X' (p '&&' (p 'U' q)))) => (p 'U' q) in X :: thesis:

reconsider pp = (('X' q) 'or' ('X' (p '&&' (p 'U' q)))) => (p 'U' q) as Element of LTL_axioms by Def17;
S₁[pp] by Def27;
hence (('X' q) 'or' ('X' (p '&&' (p 'U' q)))) => (p 'U' q) in X ; :: thesis:

end;

reconsider pp = (p 'U' q) => ('X' ('F' q)) as Element of LTL_axioms by Def17;
S₁[pp] by Def28;
hence (p 'U' q) => ('X' ('F' q)) in X ; :: thesis:

end;