let p be Element of LTLB_WFF ; :: thesis: p in tau1 . p
defpred S1[ Element of LTLB_WFF ] means \$1 in tau1 . \$1;
A1: for n being Element of NAT holds S1[ prop n]
proof
let n be Element of NAT ; :: thesis: S1[ prop n]
tau1 . (prop n) = {(prop n)} by Def4;
hence S1[ prop n] by TARSKI:def 1; :: thesis: verum
end;
A2: for r, s being Element of LTLB_WFF st S1[r] & S1[s] holds
( S1[r 'U' s] & S1[r => s] )
proof
let r, s be Element of LTLB_WFF ; :: thesis: ( S1[r] & S1[s] implies ( S1[r 'U' s] & S1[r => s] ) )
assume that
S1[r] and
S1[s] ; :: thesis: ( S1[r 'U' s] & S1[r => s] )
tau1 . (r 'U' s) = {(r 'U' s)} by Def4;
hence S1[r 'U' s] by TARSKI:def 1; :: thesis: S1[r => s]
tau1 . (r => s) = ({(r => s)} \/ ()) \/ () by Def4;
then ( {(r => s)} c= {(r => s)} \/ () & {(r => s)} \/ () c= tau1 . (r => s) ) by XBOOLE_1:7;
hence S1[r => s] by ZFMISC_1:31; :: thesis: verum
end;
tau1 . TFALSUM = by Def4;
then A3: S1[ TFALSUM ] by TARSKI:def 1;
for p being Element of LTLB_WFF holds S1[p] from HILBERT2:sch 2(A3, A1, A2);
hence p in tau1 . p ; :: thesis: verum