tau1 . p c= Sub . p
by Th25;

hence not Sub . p is empty ; :: thesis: Sub . p is finite

defpred S_{1}[ Element of LTLB_WFF ] means Sub . p is finite ;

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 ]
by Def6;

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

hence Sub . p is finite ; :: thesis: verum

hence not Sub . p is empty ; :: thesis: Sub . p is finite

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]

Sub . (prop n) = {(prop n)} by Def6;

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

end;Sub . (prop n) = {(prop n)} by Def6;

hence S

( S

proof

A4:
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 A3: ( S_{1}[r] & S_{1}[s] )
; :: thesis: ( S_{1}[r 'U' s] & S_{1}[r => s] )

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

hence S_{1}[r 'U' s]
by A3; :: thesis: S_{1}[r => s]

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

hence S_{1}[r => s]
by A3; :: thesis: verum

end;assume A3: ( S

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

hence S

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

hence S

for p being Element of LTLB_WFF holds S

hence Sub . p is finite ; :: thesis: verum