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 S1[ 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 S1[ prop n]
proof
let n be Element of NAT ; :: thesis: S1[ 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 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
A3: S1[r] and
A4: 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;
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 S1[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: S1[ 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 S1[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