let X be Subset of LTLB_WFF; :: thesis: X c= tau X

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in X or x in tau X )

defpred S_{1}[ Element of LTLB_WFF ] means ( $1 in X implies $1 in tau X );

assume A1: x in X ; :: thesis: x in tau X

then reconsider x1 = x as Element of LTLB_WFF ;

A2: for n being Element of NAT holds S_{1}[ prop n]
_{1}[r] & S_{1}[s] holds

( S_{1}[r 'U' s] & S_{1}[r => s] )
_{1}[ TFALSUM ]
_{1}[p]
from HILBERT2:sch 2(A7, A2, A4);

hence x in tau X by A1; :: thesis: verum

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in X or x in tau X )

defpred S

assume A1: x in X ; :: thesis: x in tau X

then reconsider x1 = x as Element of LTLB_WFF ;

A2: for n being Element of NAT holds S

proof

A4:
for r, s being Element of LTLB_WFF st S
let n be Element of NAT ; :: thesis: S_{1}[ prop n]

set pr = prop n;

prop n in {(prop n)} by TARSKI:def 1;

then A3: prop n in tau1 . (prop n) by Def4;

assume prop n in X ; :: thesis: prop n in tau X

hence prop n in tau X by A3, Def5; :: thesis: verum

end;set pr = prop n;

prop n in {(prop n)} by TARSKI:def 1;

then A3: prop n in tau1 . (prop n) by Def4;

assume prop n in X ; :: thesis: prop n in tau X

hence prop n in tau X by A3, Def5; :: thesis: verum

( S

proof

A7:
S
let r, s be Element of LTLB_WFF ; :: thesis: ( S_{1}[r] & S_{1}[s] implies ( S_{1}[r 'U' s] & S_{1}[r => s] ) )

assume that

S_{1}[r]
and

S_{1}[s]
; :: thesis: ( S_{1}[r 'U' s] & S_{1}[r => s] )

thus S_{1}[r 'U' s]
:: thesis: S_{1}[r => s]_{1}[r => s]
:: thesis: verum

end;assume that

S

S

thus S

proof

thus
S
set f = r 'U' s;

r 'U' s in {(r 'U' s)} by TARSKI:def 1;

then A5: r 'U' s in tau1 . (r 'U' s) by Def4;

assume r 'U' s in X ; :: thesis: r 'U' s in tau X

hence r 'U' s in tau X by A5, Def5; :: thesis: verum

end;r 'U' s in {(r 'U' s)} by TARSKI:def 1;

then A5: r 'U' s in tau1 . (r 'U' s) by Def4;

assume r 'U' s in X ; :: thesis: r 'U' s in tau X

hence r 'U' s in tau X by A5, Def5; :: thesis: verum

proof

set f = r => s;

tau1 . (r => s) = ({(r => s)} \/ (tau1 . r)) \/ (tau1 . s) by Def4

.= {(r => s)} \/ ((tau1 . r) \/ (tau1 . s)) by XBOOLE_1:4 ;

then A6: ( r => s in {(r => s)} & {(r => s)} c= tau1 . (r => s) ) by TARSKI:def 1, XBOOLE_1:7;

assume r => s in X ; :: thesis: r => s in tau X

hence r => s in tau X by A6, Def5; :: thesis: verum

end;tau1 . (r => s) = ({(r => s)} \/ (tau1 . r)) \/ (tau1 . s) by Def4

.= {(r => s)} \/ ((tau1 . r) \/ (tau1 . s)) by XBOOLE_1:4 ;

then A6: ( r => s in {(r => s)} & {(r => s)} c= tau1 . (r => s) ) by TARSKI:def 1, XBOOLE_1:7;

assume r => s in X ; :: thesis: r => s in tau X

hence r => s in tau X by A6, Def5; :: thesis: verum

proof

for p being Element of LTLB_WFF holds S
set f = TFALSUM ;

TFALSUM in {TFALSUM} by TARSKI:def 1;

then A8: TFALSUM in tau1 . TFALSUM by Def4;

assume TFALSUM in X ; :: thesis: TFALSUM in tau X

hence TFALSUM in tau X by A8, Def5; :: thesis: verum

end;TFALSUM in {TFALSUM} by TARSKI:def 1;

then A8: TFALSUM in tau1 . TFALSUM by Def4;

assume TFALSUM in X ; :: thesis: TFALSUM in tau X

hence TFALSUM in tau X by A8, Def5; :: thesis: verum

hence x in tau X by A1; :: thesis: verum