let p, q be Element of LTLB_WFF ; :: thesis:
defpred S₁[ Element of LTLB_WFF ] means ( $1 in tau1 . q implies tau1 . $1 c= tau1 . q );
A1: for n being Element of NAT holds S₁[ prop n]

let n be Element of NAT ; :: thesis:
set pr = prop n;
assume A2: prop n in tau1 . q ; :: thesis:
let x be object ; :: according to TARSKI:def 3 :: thesis:
assume x in tau1 . (prop n) ; :: thesis:
then x in {(prop n)} by Def4;
hence x in tau1 . q by TARSKI:def 1, A2; :: thesis:

end;

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

let r, s be Element of LTLB_WFF ; :: thesis:
assume that
A4: S₁[r] and
A5: S₁[s] ; :: thesis:
thus S₁[r 'U' s] :: thesis:

set f = r 'U' s;
assume A6: r 'U' s in tau1 . q ; :: thesis:
let x be object ; :: according to TARSKI:def 3 :: thesis:
assume x in tau1 . (r 'U' s) ; :: thesis:
then x in {(r 'U' s)} by Def4;
hence x in tau1 . q by TARSKI:def 1, A6; :: thesis:

end;

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

set f = r => s;
assume A7: r => s in tau1 . q ; :: thesis:
then {(r => s)} c= tau1 . q by ZFMISC_1:31;
then {(r => s)} \/ (tau1 . r) c= tau1 . q by XBOOLE_1:8, A7, Th7, A4;
then A8: ({(r => s)} \/ (tau1 . r)) \/ (tau1 . s) c= tau1 . q by XBOOLE_1:8, A7, Th7, A5;
let x be object ; :: according to TARSKI:def 3 :: thesis:
assume x in tau1 . (r => s) ; :: thesis:
then x in ({(r => s)} \/ (tau1 . r)) \/ (tau1 . s) by Def4;
hence x in tau1 . q by A8; :: thesis:

end;

end;

A9: S₁[ TFALSUM ]

set f = TFALSUM ;
assume A10: TFALSUM in tau1 . q ; :: thesis:
let x be object ; :: according to TARSKI:def 3 :: thesis:
assume x in tau1 . TFALSUM ; :: thesis:
then x in {TFALSUM} by Def4;
hence x in tau1 . q by TARSKI:def 1, A10; :: thesis:

end;

for p being Element of LTLB_WFF holds S₁[p] from HILBERT2:sch 2(A9, A1, A3);
hence ( p in tau1 . q implies tau1 . p c= tau1 . q ) ; :: thesis: