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