let p be Element of LTLB_WFF ; :: thesis: tau1 . p c= Sub . p
defpred S₁[ Element of LTLB_WFF ] means tau1 . $1 c= Sub . $1;
set f = TFALSUM ;
A1: for n being Element of NAT holds S₁[ prop n]

proof

let n be Element of NAT ; :: thesis: S₁[ prop n]
set pr = prop n;
tau1 . (prop n) = {(prop n)} by Def4
.= Sub . (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 that
A3: S₁[r] and
A4: S₁[s] ; :: thesis: ( S₁[r 'U' s] & S₁[r => s] )
thus S₁[r 'U' s] :: thesis: S₁[r => s]

proof

set f = r 'U' s;
{(r 'U' s)} c= Sub . (r 'U' s) by Th24, ZFMISC_1:31;
hence S₁[r 'U' s] by Def4; :: thesis: verum

end;

thus S₁[r => s] :: thesis: verum

proof

set f = r => s;
A5: Sub . (r => s) = ({(r => s)} \/ (Sub . r)) \/ (Sub . s) by Def6;
( {(r => s)} \/ (tau1 . r) c= {(r => s)} \/ (Sub . r) & tau1 . (r => s) = ({(r => s)} \/ (tau1 . r)) \/ (tau1 . s) ) by XBOOLE_1:13, A3, Def4;
hence S₁[r => s] by A5, A4, XBOOLE_1:13; :: thesis: verum

end;

end;

tau1 . TFALSUM = {TFALSUM} by Def4
.= Sub . TFALSUM by Def6 ;
then A6: S₁[ TFALSUM ] ;
for p being Element of LTLB_WFF holds S₁[p] from HILBERT2:sch 2(A6, A1, A2);
hence tau1 . p c= Sub . p ; :: thesis: verum