let p be Element of LTLB_WFF ; :: thesis: tau1 . p c= Sub . p

defpred S_{1}[ Element of LTLB_WFF ] means tau1 . $1 c= Sub . $1;

set f = TFALSUM ;

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] )

.= Sub . TFALSUM by Def6 ;

then A6: S_{1}[ TFALSUM ]
;

for p being Element of LTLB_WFF holds S_{1}[p]
from HILBERT2:sch 2(A6, A1, A2);

hence tau1 . p c= Sub . p ; :: thesis: verum

defpred S

set f = TFALSUM ;

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;

tau1 . (prop n) = {(prop n)} by Def4

.= Sub . (prop n) by Def6 ;

hence S_{1}[ prop n]
; :: thesis: verum

end;set pr = prop n;

tau1 . (prop n) = {(prop n)} by Def4

.= Sub . (prop n) by Def6 ;

hence S

( S

proof

tau1 . TFALSUM =
{TFALSUM}
by Def4
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;

{(r 'U' s)} c= Sub . (r 'U' s) by Th24, ZFMISC_1:31;

hence S_{1}[r 'U' s]
by Def4; :: thesis: verum

end;{(r 'U' s)} c= Sub . (r 'U' s) by Th24, ZFMISC_1:31;

hence S

.= Sub . TFALSUM by Def6 ;

then A6: S

for p being Element of LTLB_WFF holds S

hence tau1 . p c= Sub . p ; :: thesis: verum