defpred S₁[ object ] means for D being set st D is with_LTL_axioms holds
$1 in D;
consider D0 being set such that
A1: for x being object holds
( x in D0 iff ( x in LTLB_WFF & S₁[x] ) ) from XBOOLE_0:sch 1();
D0 c= LTLB_WFF by A1;
then reconsider D0 = D0 as Subset of LTLB_WFF ;
take D0 ; :: thesis: ( D0 is with_LTL_axioms & ( for D being Subset of LTLB_WFF st D is with_LTL_axioms holds
D0 c= D ) )
thus D0 is with_LTL_axioms :: thesis: for D being Subset of LTLB_WFF st D is with_LTL_axioms holds
D0 c= D

proof

let p, q be Element of LTLB_WFF ; :: according to LTLAXIO1:def 17 :: thesis: ( ( p is LTL_TAUT_OF_PL implies p in D0 ) & ('not' ('X' p)) => ('X' ('not' p)) in D0 & ('X' ('not' p)) => ('not' ('X' p)) in D0 & ('X' (p => q)) => (('X' p) => ('X' q)) in D0 & ('G' p) => (p '&&' ('X' ('G' p))) in D0 & (p 'U' q) => (('X' q) 'or' ('X' (p '&&' (p 'U' q)))) in D0 & (('X' q) 'or' ('X' (p '&&' (p 'U' q)))) => (p 'U' q) in D0 & (p 'U' q) => ('X' ('F' q)) in D0 )
thus ( p is LTL_TAUT_OF_PL implies p in D0 ) :: thesis: ( ('not' ('X' p)) => ('X' ('not' p)) in D0 & ('X' ('not' p)) => ('not' ('X' p)) in D0 & ('X' (p => q)) => (('X' p) => ('X' q)) in D0 & ('G' p) => (p '&&' ('X' ('G' p))) in D0 & (p 'U' q) => (('X' q) 'or' ('X' (p '&&' (p 'U' q)))) in D0 & (('X' q) 'or' ('X' (p '&&' (p 'U' q)))) => (p 'U' q) in D0 & (p 'U' q) => ('X' ('F' q)) in D0 )

proof

assume p is LTL_TAUT_OF_PL ; :: thesis: p in D0
then for D being set st D is with_LTL_axioms holds
p in D ;
hence p in D0 by A1; :: thesis: verum

end;

for D being set st D is with_LTL_axioms holds
('not' ('X' p)) => ('X' ('not' p)) in D ;
hence ('not' ('X' p)) => ('X' ('not' p)) in D0 by A1; :: thesis: ( ('X' ('not' p)) => ('not' ('X' p)) in D0 & ('X' (p => q)) => (('X' p) => ('X' q)) in D0 & ('G' p) => (p '&&' ('X' ('G' p))) in D0 & (p 'U' q) => (('X' q) 'or' ('X' (p '&&' (p 'U' q)))) in D0 & (('X' q) 'or' ('X' (p '&&' (p 'U' q)))) => (p 'U' q) in D0 & (p 'U' q) => ('X' ('F' q)) in D0 )
for D being set st D is with_LTL_axioms holds
('X' ('not' p)) => ('not' ('X' p)) in D ;
hence ('X' ('not' p)) => ('not' ('X' p)) in D0 by A1; :: thesis: ( ('X' (p => q)) => (('X' p) => ('X' q)) in D0 & ('G' p) => (p '&&' ('X' ('G' p))) in D0 & (p 'U' q) => (('X' q) 'or' ('X' (p '&&' (p 'U' q)))) in D0 & (('X' q) 'or' ('X' (p '&&' (p 'U' q)))) => (p 'U' q) in D0 & (p 'U' q) => ('X' ('F' q)) in D0 )
for D being set st D is with_LTL_axioms holds
('X' (p => q)) => (('X' p) => ('X' q)) in D ;
hence ('X' (p => q)) => (('X' p) => ('X' q)) in D0 by A1; :: thesis: ( ('G' p) => (p '&&' ('X' ('G' p))) in D0 & (p 'U' q) => (('X' q) 'or' ('X' (p '&&' (p 'U' q)))) in D0 & (('X' q) 'or' ('X' (p '&&' (p 'U' q)))) => (p 'U' q) in D0 & (p 'U' q) => ('X' ('F' q)) in D0 )
for D being set st D is with_LTL_axioms holds
('G' p) => (p '&&' ('X' ('G' p))) in D ;
hence ('G' p) => (p '&&' ('X' ('G' p))) in D0 by A1; :: thesis: ( (p 'U' q) => (('X' q) 'or' ('X' (p '&&' (p 'U' q)))) in D0 & (('X' q) 'or' ('X' (p '&&' (p 'U' q)))) => (p 'U' q) in D0 & (p 'U' q) => ('X' ('F' q)) in D0 )
for D being set st D is with_LTL_axioms holds
(p 'U' q) => (('X' q) 'or' ('X' (p '&&' (p 'U' q)))) in D ;
hence (p 'U' q) => (('X' q) 'or' ('X' (p '&&' (p 'U' q)))) in D0 by A1; :: thesis: ( (('X' q) 'or' ('X' (p '&&' (p 'U' q)))) => (p 'U' q) in D0 & (p 'U' q) => ('X' ('F' q)) in D0 )
for D being set st D is with_LTL_axioms holds
(('X' q) 'or' ('X' (p '&&' (p 'U' q)))) => (p 'U' q) in D ;
hence (('X' q) 'or' ('X' (p '&&' (p 'U' q)))) => (p 'U' q) in D0 by A1; :: thesis: (p 'U' q) => ('X' ('F' q)) in D0
for D being set st D is with_LTL_axioms holds
(p 'U' q) => ('X' ('F' q)) in D ;
hence (p 'U' q) => ('X' ('F' q)) in D0 by A1; :: thesis: verum

end;

let D be Subset of LTLB_WFF; :: thesis: ( D is with_LTL_axioms implies D0 c= D )
assume A2: D is with_LTL_axioms ; :: thesis: D0 c= D
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in D0 or x in D )
assume x in D0 ; :: thesis: x in D
hence x in D by A1, A2; :: thesis: verum