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 S₁[ 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 S₁[ prop n]

proof

let n be Element of NAT ; :: thesis: S₁[ 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 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
S₁[r] and
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 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 S₁[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: S₁[ 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 S₁[p] from HILBERT2:sch 2(A7, A2, A4);
hence x in tau X by A1; :: thesis: verum