tau1 . p c= Sub . p by Th25;
hence not Sub . p is empty ; :: thesis: Sub . p is finite
defpred S₁[ Element of LTLB_WFF ] means Sub . p is finite ;
A1: for n being Element of NAT holds S₁[ prop n]

proof

let n be Element of NAT ; :: thesis: S₁[ prop n]
Sub . (prop n) = {(prop n)} by Def6;
hence S₁[ prop n] ; :: thesis: verum

end;

A2: for r, s being Element of LTLB_WFF st S₁[r] & S₁[s] holds
( S₁[r 'U' s] & S₁[r => s] )

proof

let r, s be Element of LTLB_WFF ; :: thesis: ( S₁[r] & S₁[s] implies ( S₁[r 'U' s] & S₁[r => s] ) )
assume A3: ( S₁[r] & S₁[s] ) ; :: thesis: ( S₁[r 'U' s] & S₁[r => s] )
Sub . (r 'U' s) = ((tau1 . (untn (r,s))) \/ (Sub . r)) \/ (Sub . s) by Def6;
hence S₁[r 'U' s] by A3; :: thesis: S₁[r => s]
Sub . (r => s) = ({(r => s)} \/ (Sub . r)) \/ (Sub . s) by Def6;
hence S₁[r => s] by A3; :: thesis: verum

end;

A4: S₁[ TFALSUM ] by Def6;
for p being Element of LTLB_WFF holds S₁[p] from HILBERT2:sch 2(A4, A1, A2);
hence Sub . p is finite ; :: thesis: verum