defpred S_{1}[ 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_{1}[p] } ;

{ p where p is Element of LTL_axioms : S_{1}[p] } c= LTLB_WFF
_{1}[p] } as Subset of LTLB_WFF ;

let A be Element of LTL_axioms ; :: thesis: ( A is LTL_TAUT_OF_PL or A is axltl1 or A is axltl1a or A is axltl2 or A is axltl3 or A is axltl4 or A is axltl5 or A is axltl6 )

X is with_LTL_axioms

then A in X ;

then ex p being Element of LTL_axioms st

( A = p & S_{1}[p] )
;

hence S_{1}[A]
; :: thesis: verum

set X = { p where p is Element of LTL_axioms : S

{ p where p is Element of LTL_axioms : S

proof

then reconsider X = { p where p is Element of LTL_axioms : S
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in { p where p is Element of LTL_axioms : S_{1}[p] } or x in LTLB_WFF )

assume x in { p where p is Element of LTL_axioms : S_{1}[p] }
; :: thesis: x in LTLB_WFF

then ex p being Element of LTL_axioms st

( x = p & S_{1}[p] )
;

hence x in LTLB_WFF ; :: thesis: verum

end;assume x in { p where p is Element of LTL_axioms : S

then ex p being Element of LTL_axioms st

( x = p & S

hence x in LTLB_WFF ; :: thesis: verum

let A be Element of LTL_axioms ; :: thesis: ( A is LTL_TAUT_OF_PL or A is axltl1 or A is axltl1a or A is axltl2 or A is axltl3 or A is axltl4 or A is axltl5 or A is axltl6 )

X is with_LTL_axioms

proof

then
( A in LTL_axioms & LTL_axioms c= X )
by Def18;
let p be Element of LTLB_WFF ; :: according to LTLAXIO1:def 17 :: thesis: for q being Element of LTLB_WFF holds

( ( p is LTL_TAUT_OF_PL implies p in X ) & ('not' ('X' p)) => ('X' ('not' p)) in X & ('X' ('not' p)) => ('not' ('X' p)) in X & ('X' (p => q)) => (('X' p) => ('X' q)) in X & ('G' p) => (p '&&' ('X' ('G' p))) in X & (p 'U' q) => (('X' q) 'or' ('X' (p '&&' (p 'U' q)))) in X & (('X' q) 'or' ('X' (p '&&' (p 'U' q)))) => (p 'U' q) in X & (p 'U' q) => ('X' ('F' q)) in X )

let q be Element of LTLB_WFF ; :: thesis: ( ( p is LTL_TAUT_OF_PL implies p in X ) & ('not' ('X' p)) => ('X' ('not' p)) in X & ('X' ('not' p)) => ('not' ('X' p)) in X & ('X' (p => q)) => (('X' p) => ('X' q)) in X & ('G' p) => (p '&&' ('X' ('G' p))) in X & (p 'U' q) => (('X' q) 'or' ('X' (p '&&' (p 'U' q)))) in X & (('X' q) 'or' ('X' (p '&&' (p 'U' q)))) => (p 'U' q) in X & (p 'U' q) => ('X' ('F' q)) in X )

thus ( p is LTL_TAUT_OF_PL implies p in X ) :: thesis: ( ('not' ('X' p)) => ('X' ('not' p)) in X & ('X' ('not' p)) => ('not' ('X' p)) in X & ('X' (p => q)) => (('X' p) => ('X' q)) in X & ('G' p) => (p '&&' ('X' ('G' p))) in X & (p 'U' q) => (('X' q) 'or' ('X' (p '&&' (p 'U' q)))) in X & (('X' q) 'or' ('X' (p '&&' (p 'U' q)))) => (p 'U' q) in X & (p 'U' q) => ('X' ('F' q)) in X )

end;( ( p is LTL_TAUT_OF_PL implies p in X ) & ('not' ('X' p)) => ('X' ('not' p)) in X & ('X' ('not' p)) => ('not' ('X' p)) in X & ('X' (p => q)) => (('X' p) => ('X' q)) in X & ('G' p) => (p '&&' ('X' ('G' p))) in X & (p 'U' q) => (('X' q) 'or' ('X' (p '&&' (p 'U' q)))) in X & (('X' q) 'or' ('X' (p '&&' (p 'U' q)))) => (p 'U' q) in X & (p 'U' q) => ('X' ('F' q)) in X )

let q be Element of LTLB_WFF ; :: thesis: ( ( p is LTL_TAUT_OF_PL implies p in X ) & ('not' ('X' p)) => ('X' ('not' p)) in X & ('X' ('not' p)) => ('not' ('X' p)) in X & ('X' (p => q)) => (('X' p) => ('X' q)) in X & ('G' p) => (p '&&' ('X' ('G' p))) in X & (p 'U' q) => (('X' q) 'or' ('X' (p '&&' (p 'U' q)))) in X & (('X' q) 'or' ('X' (p '&&' (p 'U' q)))) => (p 'U' q) in X & (p 'U' q) => ('X' ('F' q)) in X )

thus ( p is LTL_TAUT_OF_PL implies p in X ) :: thesis: ( ('not' ('X' p)) => ('X' ('not' p)) in X & ('X' ('not' p)) => ('not' ('X' p)) in X & ('X' (p => q)) => (('X' p) => ('X' q)) in X & ('G' p) => (p '&&' ('X' ('G' p))) in X & (p 'U' q) => (('X' q) 'or' ('X' (p '&&' (p 'U' q)))) in X & (('X' q) 'or' ('X' (p '&&' (p 'U' q)))) => (p 'U' q) in X & (p 'U' q) => ('X' ('F' q)) in X )

proof

thus
('not' ('X' p)) => ('X' ('not' p)) in X
:: thesis: ( ('X' ('not' p)) => ('not' ('X' p)) in X & ('X' (p => q)) => (('X' p) => ('X' q)) in X & ('G' p) => (p '&&' ('X' ('G' p))) in X & (p 'U' q) => (('X' q) 'or' ('X' (p '&&' (p 'U' q)))) in X & (('X' q) 'or' ('X' (p '&&' (p 'U' q)))) => (p 'U' q) in X & (p 'U' q) => ('X' ('F' q)) in X )
assume A1:
p is LTL_TAUT_OF_PL
; :: thesis: p in X

then reconsider p1 = p as Element of LTL_axioms by Def17;

S_{1}[p1]
by A1;

hence p in X ; :: thesis: verum

end;then reconsider p1 = p as Element of LTL_axioms by Def17;

S

hence p in X ; :: thesis: verum

proof

thus
('X' ('not' p)) => ('not' ('X' p)) in X
:: thesis: ( ('X' (p => q)) => (('X' p) => ('X' q)) in X & ('G' p) => (p '&&' ('X' ('G' p))) in X & (p 'U' q) => (('X' q) 'or' ('X' (p '&&' (p 'U' q)))) in X & (('X' q) 'or' ('X' (p '&&' (p 'U' q)))) => (p 'U' q) in X & (p 'U' q) => ('X' ('F' q)) in X )
reconsider pp = ('not' ('X' p)) => ('X' ('not' p)) as Element of LTL_axioms by Def17;

S_{1}[pp]
by Def22;

hence ('not' ('X' p)) => ('X' ('not' p)) in X ; :: thesis: verum

end;S

hence ('not' ('X' p)) => ('X' ('not' p)) in X ; :: thesis: verum

proof

thus
('X' (p => q)) => (('X' p) => ('X' q)) in X
:: thesis: ( ('G' p) => (p '&&' ('X' ('G' p))) in X & (p 'U' q) => (('X' q) 'or' ('X' (p '&&' (p 'U' q)))) in X & (('X' q) 'or' ('X' (p '&&' (p 'U' q)))) => (p 'U' q) in X & (p 'U' q) => ('X' ('F' q)) in X )
reconsider pp = ('X' ('not' p)) => ('not' ('X' p)) as Element of LTL_axioms by Def17;

S_{1}[pp]
by Def23;

hence ('X' ('not' p)) => ('not' ('X' p)) in X ; :: thesis: verum

end;S

hence ('X' ('not' p)) => ('not' ('X' p)) in X ; :: thesis: verum

proof

thus
('G' p) => (p '&&' ('X' ('G' p))) in X
:: thesis: ( (p 'U' q) => (('X' q) 'or' ('X' (p '&&' (p 'U' q)))) in X & (('X' q) 'or' ('X' (p '&&' (p 'U' q)))) => (p 'U' q) in X & (p 'U' q) => ('X' ('F' q)) in X )
reconsider pp = ('X' (p => q)) => (('X' p) => ('X' q)) as Element of LTL_axioms by Def17;

S_{1}[pp]
by Def24;

hence ('X' (p => q)) => (('X' p) => ('X' q)) in X ; :: thesis: verum

end;S

hence ('X' (p => q)) => (('X' p) => ('X' q)) in X ; :: thesis: verum

proof

thus
(p 'U' q) => (('X' q) 'or' ('X' (p '&&' (p 'U' q)))) in X
:: thesis: ( (('X' q) 'or' ('X' (p '&&' (p 'U' q)))) => (p 'U' q) in X & (p 'U' q) => ('X' ('F' q)) in X )
reconsider pp = ('G' p) => (p '&&' ('X' ('G' p))) as Element of LTL_axioms by Def17;

S_{1}[pp]
by Def25;

hence ('G' p) => (p '&&' ('X' ('G' p))) in X ; :: thesis: verum

end;S

hence ('G' p) => (p '&&' ('X' ('G' p))) in X ; :: thesis: verum

proof

thus
(('X' q) 'or' ('X' (p '&&' (p 'U' q)))) => (p 'U' q) in X
:: thesis: (p 'U' q) => ('X' ('F' q)) in X
reconsider pp = (p 'U' q) => (('X' q) 'or' ('X' (p '&&' (p 'U' q)))) as Element of LTL_axioms by Def17;

S_{1}[pp]
by Def26;

hence (p 'U' q) => (('X' q) 'or' ('X' (p '&&' (p 'U' q)))) in X ; :: thesis: verum

end;S

hence (p 'U' q) => (('X' q) 'or' ('X' (p '&&' (p 'U' q)))) in X ; :: thesis: verum

proof

thus
(p 'U' q) => ('X' ('F' q)) in X
:: thesis: verum
reconsider pp = (('X' q) 'or' ('X' (p '&&' (p 'U' q)))) => (p 'U' q) as Element of LTL_axioms by Def17;

S_{1}[pp]
by Def27;

hence (('X' q) 'or' ('X' (p '&&' (p 'U' q)))) => (p 'U' q) in X ; :: thesis: verum

end;S

hence (('X' q) 'or' ('X' (p '&&' (p 'U' q)))) => (p 'U' q) in X ; :: thesis: verum

then A in X ;

then ex p being Element of LTL_axioms st

( A = p & S

hence S