let p, q, r be Element of LTLB_WFF ; :: thesis: ( p => q in tau1 . r implies ( p in tau1 . r & q in tau1 . r ) )
defpred S₁[ Element of LTLB_WFF ] means ( p => q in tau1 . $1 implies ( p in tau1 . $1 & q in tau1 . $1 ) );
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;
assume p => q in tau1 . (prop n) ; :: thesis: ( p in tau1 . (prop n) & q in tau1 . (prop n) )
then p => q in {(prop n)} by Def4;
then p => q = prop n by TARSKI:def 1;
hence ( p in tau1 . (prop n) & q in tau1 . (prop n) ) by HILBERT2:26; :: 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;
assume p => q in tau1 . (r 'U' s) ; :: thesis: ( p in tau1 . (r 'U' s) & q in tau1 . (r 'U' s) )
then p => q in {(r 'U' s)} by Def4;
then p => q = r 'U' s by TARSKI:def 1;
hence ( p in tau1 . (r 'U' s) & q in tau1 . (r 'U' s) ) by HILBERT2:22; :: thesis: verum

end;

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

proof

set f = r => s;
A5: tau1 . (r => s) = ({(r => s)} \/ (tau1 . r)) \/ (tau1 . s) by Def4;
then A6: tau1 . s c= tau1 . (r => s) by XBOOLE_1:7;
( tau1 . r c= {(r => s)} \/ (tau1 . r) & {(r => s)} \/ (tau1 . r) c= tau1 . (r => s) ) by XBOOLE_1:7, A5;
then A7: tau1 . r c= tau1 . (r => s) ;
assume A8: p => q in tau1 . (r => s) ; :: thesis: ( p in tau1 . (r => s) & q in tau1 . (r => s) )

per cases ( p => q in {(r => s)} \/ (tau1 . r) or p => q in tau1 . s ) by A8, A5, XBOOLE_0:def 3;

suppose A9: p => q in {(r => s)} \/ (tau1 . r) ; :: thesis: ( p in tau1 . (r => s) & q in tau1 . (r => s) )

per cases ( p => q in {(r => s)} or p => q in tau1 . r ) by A9, XBOOLE_0:def 3;

suppose p => q in {(r => s)} ; :: thesis: ( p in tau1 . (r => s) & q in tau1 . (r => s) )

then A10: p => q = r => s by TARSKI:def 1;
then A11: p = r by HILBERT2:20;
r in tau1 . r by Th6;
hence p in tau1 . (r => s) by A11, A7; :: thesis: q in tau1 . (r => s)
A12: q = s by A10, HILBERT2:20;
s in tau1 . s by Th6;
hence q in tau1 . (r => s) by A12, A6; :: thesis: verum

end;

suppose p => q in tau1 . r ; :: thesis: ( p in tau1 . (r => s) & q in tau1 . (r => s) )

hence ( p in tau1 . (r => s) & q in tau1 . (r => s) ) by A3, A7; :: thesis: verum

end;

end;

end;

suppose p => q in tau1 . s ; :: thesis: ( p in tau1 . (r => s) & q in tau1 . (r => s) )

hence ( p in tau1 . (r => s) & q in tau1 . (r => s) ) by A4, A6; :: thesis: verum

end;

end;

end;

end;

A13: S₁[ TFALSUM ]

proof

set f = TFALSUM ;
assume p => q in tau1 . TFALSUM ; :: thesis: ( p in tau1 . TFALSUM & q in tau1 . TFALSUM )
then p => q in {TFALSUM} by Def4;
then p => q = TFALSUM by TARSKI:def 1;
hence ( p in tau1 . TFALSUM & q in tau1 . TFALSUM ) by HILBERT2:25; :: thesis: verum

end;

for p being Element of LTLB_WFF holds S₁[p] from HILBERT2:sch 2(A13, A1, A2);
hence ( p => q in tau1 . r implies ( p in tau1 . r & q in tau1 . r ) ) ; :: thesis: verum