let X be Subset of LTLB_WFF; :: thesis: X c= tau X
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in X or x in tau X )
defpred S1[ Element of LTLB_WFF ] means ( $1 in X implies $1 in tau X );
assume A1: x in X ; :: thesis: x in tau X
then reconsider x1 = x as Element of LTLB_WFF ;
A2: for n being Element of NAT holds S1[ prop n]
proof
let n be Element of NAT ; :: thesis: S1[ prop n]
set pr = prop n;
prop n in {(prop n)} by TARSKI:def 1;
then A3: prop n in tau1 . (prop n) by Def4;
assume prop n in X ; :: thesis: prop n in tau X
hence prop n in tau X by A3, Def5; :: thesis: verum
end;
A4: 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] )
thus S1[r 'U' s] :: thesis: S1[r => s]
proof
set f = r 'U' s;
r 'U' s in {(r 'U' s)} by TARSKI:def 1;
then A5: r 'U' s in tau1 . (r 'U' s) by Def4;
assume r 'U' s in X ; :: thesis: r 'U' s in tau X
hence r 'U' s in tau X by A5, Def5; :: thesis: verum
end;
thus S1[r => s] :: thesis: verum
proof
set f = r => s;
tau1 . (r => s) = ({(r => s)} \/ (tau1 . r)) \/ (tau1 . s) by Def4
.= {(r => s)} \/ ((tau1 . r) \/ (tau1 . s)) by XBOOLE_1:4 ;
then A6: ( r => s in {(r => s)} & {(r => s)} c= tau1 . (r => s) ) by TARSKI:def 1, XBOOLE_1:7;
assume r => s in X ; :: thesis: r => s in tau X
hence r => s in tau X by A6, Def5; :: thesis: verum
end;
end;
A7: S1[ TFALSUM ]
proof
set f = TFALSUM ;
TFALSUM in {TFALSUM} by TARSKI:def 1;
then A8: TFALSUM in tau1 . TFALSUM by Def4;
assume TFALSUM in X ; :: thesis: TFALSUM in tau X
hence TFALSUM in tau X by A8, Def5; :: thesis: verum
end;
for p being Element of LTLB_WFF holds S1[p] from HILBERT2:sch 2(A7, A2, A4);
 hence x in tau X by A1; :: thesis: verum