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

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

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(A13, A1, A2);

hence ( p => q in tau1 . r implies ( p in tau1 . r & q in tau1 . r ) ) ; :: thesis: verum

defpred S

A1: for n being Element of NAT holds S

proof

A2:
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 p => q in tau1 . (prop n) ; :: thesis: ( p in tau1 . (prop n) & q in tau1 . (prop n) )

then p => q in {(prop n)} by Def4;

then p => q = prop n by TARSKI:def 1;

hence ( p in tau1 . (prop n) & q in tau1 . (prop n) ) by HILBERT2:26; :: thesis: verum

end;set pr = prop n;

assume p => q in tau1 . (prop n) ; :: thesis: ( p in tau1 . (prop n) & q in tau1 . (prop n) )

then p => q in {(prop n)} by Def4;

then p => q = prop n by TARSKI:def 1;

hence ( p in tau1 . (prop n) & q in tau1 . (prop n) ) by HILBERT2:26; :: thesis: verum

( S

proof

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

A3: S_{1}[r]
and

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

A3: S

A4: S

thus S

proof

thus
S
set f = r 'U' s;

assume p => q in tau1 . (r 'U' s) ; :: thesis: ( p in tau1 . (r 'U' s) & q in tau1 . (r 'U' s) )

then p => q in {(r 'U' s)} by Def4;

then p => q = r 'U' s by TARSKI:def 1;

hence ( p in tau1 . (r 'U' s) & q in tau1 . (r 'U' s) ) by HILBERT2:22; :: thesis: verum

end;assume p => q in tau1 . (r 'U' s) ; :: thesis: ( p in tau1 . (r 'U' s) & q in tau1 . (r 'U' s) )

then p => q in {(r 'U' s)} by Def4;

then p => q = r 'U' s by TARSKI:def 1;

hence ( p in tau1 . (r 'U' s) & q in tau1 . (r 'U' s) ) by HILBERT2:22; :: thesis: verum

proof

set f = r => s;

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

then A6: tau1 . s c= tau1 . (r => s) by XBOOLE_1:7;

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

then A7: tau1 . r c= tau1 . (r => s) ;

assume A8: p => q in tau1 . (r => s) ; :: thesis: ( p in tau1 . (r => s) & q in tau1 . (r => s) )

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

then A6: tau1 . s c= tau1 . (r => s) by XBOOLE_1:7;

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

then A7: tau1 . r c= tau1 . (r => s) ;

assume A8: p => q in tau1 . (r => s) ; :: thesis: ( p in tau1 . (r => s) & q in tau1 . (r => s) )

per cases
( p => q in {(r => s)} \/ (tau1 . r) or p => q in tau1 . s )
by A8, A5, XBOOLE_0:def 3;

end;

suppose A9:
p => q in {(r => s)} \/ (tau1 . r)
; :: thesis: ( p in tau1 . (r => s) & q in tau1 . (r => s) )

end;

per cases
( p => q in {(r => s)} or p => q in tau1 . r )
by A9, XBOOLE_0:def 3;

end;

suppose
p => q in {(r => s)}
; :: thesis: ( p in tau1 . (r => s) & q in tau1 . (r => s) )

then A10:
p => q = r => s
by TARSKI:def 1;

then A11: p = r by HILBERT2:20;

r in tau1 . r by Th6;

hence p in tau1 . (r => s) by A11, A7; :: thesis: q in tau1 . (r => s)

A12: q = s by A10, HILBERT2:20;

s in tau1 . s by Th6;

hence q in tau1 . (r => s) by A12, A6; :: thesis: verum

end;then A11: p = r by HILBERT2:20;

r in tau1 . r by Th6;

hence p in tau1 . (r => s) by A11, A7; :: thesis: q in tau1 . (r => s)

A12: q = s by A10, HILBERT2:20;

s in tau1 . s by Th6;

hence q in tau1 . (r => s) by A12, A6; :: thesis: verum

proof

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

assume p => q in tau1 . TFALSUM ; :: thesis: ( p in tau1 . TFALSUM & q in tau1 . TFALSUM )

then p => q in {TFALSUM} by Def4;

then p => q = TFALSUM by TARSKI:def 1;

hence ( p in tau1 . TFALSUM & q in tau1 . TFALSUM ) by HILBERT2:25; :: thesis: verum

end;assume p => q in tau1 . TFALSUM ; :: thesis: ( p in tau1 . TFALSUM & q in tau1 . TFALSUM )

then p => q in {TFALSUM} by Def4;

then p => q = TFALSUM by TARSKI:def 1;

hence ( p in tau1 . TFALSUM & q in tau1 . TFALSUM ) by HILBERT2:25; :: thesis: verum

hence ( p => q in tau1 . r implies ( p in tau1 . r & q in tau1 . r ) ) ; :: thesis: verum