let p, q be Element of LTLB_WFF ; :: thesis: ( p in tau1 . q implies tau1 . p c= tau1 . q )

defpred S_{1}[ Element of LTLB_WFF ] means ( $1 in tau1 . q implies tau1 . $1 c= tau1 . q );

A1: 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(A9, A1, A3);

hence ( p in tau1 . q implies tau1 . p c= tau1 . q ) ; :: thesis: verum

defpred S

A1: for n being Element of NAT holds S

proof

A3:
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;

assume A2: prop n in tau1 . q ; :: thesis: tau1 . (prop n) c= tau1 . q

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in tau1 . (prop n) or x in tau1 . q )

assume x in tau1 . (prop n) ; :: thesis: x in tau1 . q

then x in {(prop n)} by Def4;

hence x in tau1 . q by TARSKI:def 1, A2; :: thesis: verum

end;set pr = prop n;

assume A2: prop n in tau1 . q ; :: thesis: tau1 . (prop n) c= tau1 . q

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in tau1 . (prop n) or x in tau1 . q )

assume x in tau1 . (prop n) ; :: thesis: x in tau1 . q

then x in {(prop n)} by Def4;

hence x in tau1 . q by TARSKI:def 1, A2; :: thesis: verum

( S

proof

A9:
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

A4: S_{1}[r]
and

A5: 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

A4: S

A5: S

thus S

proof

thus
S
set f = r 'U' s;

assume A6: r 'U' s in tau1 . q ; :: thesis: tau1 . (r 'U' s) c= tau1 . q

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in tau1 . (r 'U' s) or x in tau1 . q )

assume x in tau1 . (r 'U' s) ; :: thesis: x in tau1 . q

then x in {(r 'U' s)} by Def4;

hence x in tau1 . q by TARSKI:def 1, A6; :: thesis: verum

end;assume A6: r 'U' s in tau1 . q ; :: thesis: tau1 . (r 'U' s) c= tau1 . q

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in tau1 . (r 'U' s) or x in tau1 . q )

assume x in tau1 . (r 'U' s) ; :: thesis: x in tau1 . q

then x in {(r 'U' s)} by Def4;

hence x in tau1 . q by TARSKI:def 1, A6; :: thesis: verum

proof

set f = r => s;

assume A7: r => s in tau1 . q ; :: thesis: tau1 . (r => s) c= tau1 . q

then {(r => s)} c= tau1 . q by ZFMISC_1:31;

then {(r => s)} \/ (tau1 . r) c= tau1 . q by XBOOLE_1:8, A7, Th7, A4;

then A8: ({(r => s)} \/ (tau1 . r)) \/ (tau1 . s) c= tau1 . q by XBOOLE_1:8, A7, Th7, A5;

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in tau1 . (r => s) or x in tau1 . q )

assume x in tau1 . (r => s) ; :: thesis: x in tau1 . q

then x in ({(r => s)} \/ (tau1 . r)) \/ (tau1 . s) by Def4;

hence x in tau1 . q by A8; :: thesis: verum

end;assume A7: r => s in tau1 . q ; :: thesis: tau1 . (r => s) c= tau1 . q

then {(r => s)} c= tau1 . q by ZFMISC_1:31;

then {(r => s)} \/ (tau1 . r) c= tau1 . q by XBOOLE_1:8, A7, Th7, A4;

then A8: ({(r => s)} \/ (tau1 . r)) \/ (tau1 . s) c= tau1 . q by XBOOLE_1:8, A7, Th7, A5;

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in tau1 . (r => s) or x in tau1 . q )

assume x in tau1 . (r => s) ; :: thesis: x in tau1 . q

then x in ({(r => s)} \/ (tau1 . r)) \/ (tau1 . s) by Def4;

hence x in tau1 . q by A8; :: thesis: verum

proof

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

assume A10: TFALSUM in tau1 . q ; :: thesis: tau1 . TFALSUM c= tau1 . q

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in tau1 . TFALSUM or x in tau1 . q )

assume x in tau1 . TFALSUM ; :: thesis: x in tau1 . q

then x in {TFALSUM} by Def4;

hence x in tau1 . q by TARSKI:def 1, A10; :: thesis: verum

end;assume A10: TFALSUM in tau1 . q ; :: thesis: tau1 . TFALSUM c= tau1 . q

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in tau1 . TFALSUM or x in tau1 . q )

assume x in tau1 . TFALSUM ; :: thesis: x in tau1 . q

then x in {TFALSUM} by Def4;

hence x in tau1 . q by TARSKI:def 1, A10; :: thesis: verum

hence ( p in tau1 . q implies tau1 . p c= tau1 . q ) ; :: thesis: verum