let A, B, p, q be Element of LTLB_WFF ; :: thesis: ( p in Sub . (A 'U' B) & A 'U' B in Sub . q implies p in Sub . q )

set aub = A 'U' B;

set f = TFALSUM ;

defpred S_{1}[ Element of LTLB_WFF ] means ( A 'U' B in Sub . $1 implies p in Sub . $1 );

A1: for n being Element of NAT holds S_{1}[ prop n]

A3: for r, s being Element of LTLB_WFF st S_{1}[r] & S_{1}[s] holds

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

hence ( not A 'U' B in Sub . q or p in Sub . q ) ; :: thesis: verum

set aub = A 'U' B;

set f = TFALSUM ;

defpred S

A1: for n being Element of NAT holds S

proof

assume A2:
p in Sub . (A 'U' B)
; :: thesis: ( not A 'U' B in Sub . q or p in Sub . q )
let n be Element of NAT ; :: thesis: S_{1}[ prop n]

set pr = prop n;

assume A 'U' B in Sub . (prop n) ; :: thesis: p in Sub . (prop n)

then A 'U' B in {(prop n)} by Def6;

then A 'U' B = prop n by TARSKI:def 1;

hence p in Sub . (prop n) by HILBERT2:24; :: thesis: verum

end;set pr = prop n;

assume A 'U' B in Sub . (prop n) ; :: thesis: p in Sub . (prop n)

then A 'U' B in {(prop n)} by Def6;

then A 'U' B = prop n by TARSKI:def 1;

hence p in Sub . (prop n) by HILBERT2:24; :: thesis: verum

A3: for r, s being Element of LTLB_WFF st S

( S

proof

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

A6: tau1 . r c= Sub . r by Th25;

A7: Sub . (r 'U' s) = ((tau1 . (untn (r,s))) \/ (Sub . r)) \/ (Sub . s) by Def6;

then A8: Sub . s c= Sub . (r 'U' s) by XBOOLE_1:7;

( Sub . r c= (tau1 . (untn (r,s))) \/ (Sub . r) & (tau1 . (untn (r,s))) \/ (Sub . r) c= Sub . (r 'U' s) ) by XBOOLE_1:7, A7;

then A9: Sub . r c= Sub . (r 'U' s) ;

assume A 'U' B in Sub . (r 'U' s) ; :: thesis: p in Sub . (r 'U' s)

then A10: A 'U' B in ((tau1 . (untn (r,s))) \/ (Sub . r)) \/ (Sub . s) by Def6;

A11: tau1 . s c= Sub . s by Th25;

end;A6: tau1 . r c= Sub . r by Th25;

A7: Sub . (r 'U' s) = ((tau1 . (untn (r,s))) \/ (Sub . r)) \/ (Sub . s) by Def6;

then A8: Sub . s c= Sub . (r 'U' s) by XBOOLE_1:7;

( Sub . r c= (tau1 . (untn (r,s))) \/ (Sub . r) & (tau1 . (untn (r,s))) \/ (Sub . r) c= Sub . (r 'U' s) ) by XBOOLE_1:7, A7;

then A9: Sub . r c= Sub . (r 'U' s) ;

assume A 'U' B in Sub . (r 'U' s) ; :: thesis: p in Sub . (r 'U' s)

then A10: A 'U' B in ((tau1 . (untn (r,s))) \/ (Sub . r)) \/ (Sub . s) by Def6;

A11: tau1 . s c= Sub . s by Th25;

per cases
( A 'U' B in (tau1 . (untn (r,s))) \/ (Sub . r) or A 'U' B in Sub . s )
by A10, XBOOLE_0:def 3;

end;

suppose A12:
A 'U' B in (tau1 . (untn (r,s))) \/ (Sub . r)
; :: thesis: p in Sub . (r 'U' s)

end;

per cases
( A 'U' B in tau1 . (untn (r,s)) or A 'U' B in Sub . r )
by A12, XBOOLE_0:def 3;

end;

suppose
A 'U' B in tau1 . (untn (r,s))
; :: thesis: p in Sub . (r 'U' s)

then
A 'U' B in tau1 . (('not' s) '&&' ('not' (r '&&' (r 'U' s))))
by Th9;

then ( A 'U' B in tau1 . ('not' s) or A 'U' B in tau1 . ('not' (r '&&' (r 'U' s))) ) by Th10;

then A13: ( A 'U' B in tau1 . s or A 'U' B in tau1 . (r '&&' (r 'U' s)) ) by Th9;

end;then ( A 'U' B in tau1 . ('not' s) or A 'U' B in tau1 . ('not' (r '&&' (r 'U' s))) ) by Th10;

then A13: ( A 'U' B in tau1 . s or A 'U' B in tau1 . (r '&&' (r 'U' s)) ) by Th9;

per cases
( A 'U' B in tau1 . r or A 'U' B in tau1 . s or A 'U' B in tau1 . (r 'U' s) )
by A13, Th10;

end;

proof

set f = r => s;

A15: Sub . (r => s) = ({(r => s)} \/ (Sub . r)) \/ (Sub . s) by Def6;

then A16: Sub . s c= Sub . (r => s) by XBOOLE_1:7;

( Sub . r c= {(r => s)} \/ (Sub . r) & {(r => s)} \/ (Sub . r) c= Sub . (r => s) ) by XBOOLE_1:7, A15;

then A17: Sub . r c= Sub . (r => s) ;

assume A 'U' B in Sub . (r => s) ; :: thesis: p in Sub . (r => s)

then A18: A 'U' B in ({(r => s)} \/ (Sub . r)) \/ (Sub . s) by Def6;

end;A15: Sub . (r => s) = ({(r => s)} \/ (Sub . r)) \/ (Sub . s) by Def6;

then A16: Sub . s c= Sub . (r => s) by XBOOLE_1:7;

( Sub . r c= {(r => s)} \/ (Sub . r) & {(r => s)} \/ (Sub . r) c= Sub . (r => s) ) by XBOOLE_1:7, A15;

then A17: Sub . r c= Sub . (r => s) ;

assume A 'U' B in Sub . (r => s) ; :: thesis: p in Sub . (r => s)

then A18: A 'U' B in ({(r => s)} \/ (Sub . r)) \/ (Sub . s) by Def6;

per cases
( A 'U' B in {(r => s)} \/ (Sub . r) or A 'U' B in Sub . s )
by A18, XBOOLE_0:def 3;

end;

proof

for p being Element of LTLB_WFF holds S
assume
A 'U' B in Sub . TFALSUM
; :: thesis: p in Sub . TFALSUM

then A 'U' B in {TFALSUM} by Def6;

then A 'U' B = TFALSUM by TARSKI:def 1;

hence p in Sub . TFALSUM by HILBERT2:23; :: thesis: verum

end;then A 'U' B in {TFALSUM} by Def6;

then A 'U' B = TFALSUM by TARSKI:def 1;

hence p in Sub . TFALSUM by HILBERT2:23; :: thesis: verum

hence ( not A 'U' B in Sub . q or p in Sub . q ) ; :: thesis: verum