let r, s, t, x be Real; :: thesis: ( ( r <= x - t & x + t <= s implies ].(x - t),(x + t).[ /\ [.r,s.] = ].(x - t),(x + t).[ ) & ( r <= x - t & s < x + t implies ].(x - t),(x + t).[ /\ [.r,s.] = ].(x - t),s.] ) & ( x - t < r & x + t <= s implies ].(x - t),(x + t).[ /\ [.r,s.] = [.r,(x + t).[ ) & ( x - t < r & s < x + t implies ].(x - t),(x + t).[ /\ [.r,s.] = [.r,s.] ) )
hereby :: thesis: ( ( r <= x - t & s < x + t implies ].(x - t),(x + t).[ /\ [.r,s.] = ].(x - t),s.] ) & ( x - t < r & x + t <= s implies ].(x - t),(x + t).[ /\ [.r,s.] = [.r,(x + t).[ ) & ( x - t < r & s < x + t implies ].(x - t),(x + t).[ /\ [.r,s.] = [.r,s.] ) )
assume that
A1: r <= x - t and
A2: x + t <= s ; :: thesis: ].(x - t),(x + t).[ /\ [.r,s.] = ].(x - t),(x + t).[
].(x - t),(x + t).[ c= [.r,s.]
proof
let u be object ; :: according to TARSKI:def 3 :: thesis: ( not u in ].(x - t),(x + t).[ or u in [.r,s.] )
assume A3: u in ].(x - t),(x + t).[ ; :: thesis: u in [.r,s.]
then reconsider u1 = u as Real ;
( x - t < u1 & u1 < x + t ) by A3, XXREAL_1:4;
then ( r <= u1 & u1 <= s ) by A1, A2, XXREAL_0:2;
hence u in [.r,s.] by XXREAL_1:1; :: thesis: verum
end;
hence ].(x - t),(x + t).[ /\ [.r,s.] = ].(x - t),(x + t).[ by XBOOLE_1:17, XBOOLE_1:19; :: thesis: verum
end;
hereby :: thesis: ( ( x - t < r & x + t <= s implies ].(x - t),(x + t).[ /\ [.r,s.] = [.r,(x + t).[ ) & ( x - t < r & s < x + t implies ].(x - t),(x + t).[ /\ [.r,s.] = [.r,s.] ) )
assume that
A4: r <= x - t and
A5: s < x + t ; :: thesis: ].(x - t),(x + t).[ /\ [.r,s.] = ].(x - t),s.]
A6: ].(x - t),(x + t).[ /\ [.r,s.] c= ].(x - t),s.]
proof
let u be object ; :: according to TARSKI:def 3 :: thesis: ( not u in ].(x - t),(x + t).[ /\ [.r,s.] or u in ].(x - t),s.] )
assume A7: u in ].(x - t),(x + t).[ /\ [.r,s.] ; :: thesis: u in ].(x - t),s.]
then A8: ( u in ].(x - t),(x + t).[ & u in [.r,s.] ) by XBOOLE_0:def 4;
reconsider u1 = u as Real by A7;
( x - t < u1 & u1 <= s ) by A8, XXREAL_1:1, XXREAL_1:4;
hence u in ].(x - t),s.] by XXREAL_1:2; :: thesis: verum
end;
].(x - t),s.] c= ].(x - t),(x + t).[ /\ [.r,s.]
proof
let u be object ; :: according to TARSKI:def 3 :: thesis: ( not u in ].(x - t),s.] or u in ].(x - t),(x + t).[ /\ [.r,s.] )
assume A9: u in ].(x - t),s.] ; :: thesis: u in ].(x - t),(x + t).[ /\ [.r,s.]
then reconsider u1 = u as Real ;
( x - t < u1 & u1 <= s ) by A9, XXREAL_1:2;
then ( x - t < u1 & u1 < x + t & r <= u1 & u1 <= s ) by A4, A5, XXREAL_0:2;
then ( u in ].(x - t),(x + t).[ & u in [.r,s.] ) by XXREAL_1:1, XXREAL_1:4;
hence u in ].(x - t),(x + t).[ /\ [.r,s.] by XBOOLE_0:def 4; :: thesis: verum
end;
hence ].(x - t),(x + t).[ /\ [.r,s.] = ].(x - t),s.] by A6; :: thesis: verum
end;
hereby :: thesis: ( x - t < r & s < x + t implies ].(x - t),(x + t).[ /\ [.r,s.] = [.r,s.] )
assume that
A10: x - t < r and
A11: x + t <= s ; :: thesis: ].(x - t),(x + t).[ /\ [.r,s.] = [.r,(x + t).[
A12: ].(x - t),(x + t).[ /\ [.r,s.] c= [.r,(x + t).[
proof
let u be object ; :: according to TARSKI:def 3 :: thesis: ( not u in ].(x - t),(x + t).[ /\ [.r,s.] or u in [.r,(x + t).[ )
assume A13: u in ].(x - t),(x + t).[ /\ [.r,s.] ; :: thesis: u in [.r,(x + t).[
then A14: ( u in ].(x - t),(x + t).[ & u in [.r,s.] ) by XBOOLE_0:def 4;
reconsider u1 = u as Real by A13;
( r <= u1 & u1 < x + t ) by A14, XXREAL_1:4, XXREAL_1:1;
hence u in [.r,(x + t).[ by XXREAL_1:3; :: thesis: verum
end;
[.r,(x + t).[ c= ].(x - t),(x + t).[ /\ [.r,s.]
proof
let u be object ; :: according to TARSKI:def 3 :: thesis: ( not u in [.r,(x + t).[ or u in ].(x - t),(x + t).[ /\ [.r,s.] )
assume A15: u in [.r,(x + t).[ ; :: thesis: u in ].(x - t),(x + t).[ /\ [.r,s.]
then reconsider u1 = u as Real ;
( r <= u1 & u1 < x + t ) by A15, XXREAL_1:3;
then ( x - t < u1 & u1 < x + t & r <= u1 & u1 <= s ) by A10, A11, XXREAL_0:2;
then ( u in ].(x - t),(x + t).[ & u in [.r,s.] ) by XXREAL_1:1, XXREAL_1:4;
hence u in ].(x - t),(x + t).[ /\ [.r,s.] by XBOOLE_0:def 4; :: thesis: verum
end;
hence ].(x - t),(x + t).[ /\ [.r,s.] = [.r,(x + t).[ by A12; :: thesis: verum
end;
hereby :: thesis: verum
assume that
A16: x - t < r and
A17: s < x + t ; :: thesis: ].(x - t),(x + t).[ /\ [.r,s.] = [.r,s.]
[.r,s.] c= ].(x - t),(x + t).[
proof
let u be object ; :: according to TARSKI:def 3 :: thesis: ( not u in [.r,s.] or u in ].(x - t),(x + t).[ )
assume A18: u in [.r,s.] ; :: thesis: u in ].(x - t),(x + t).[
then reconsider u1 = u as Real ;
( r <= u1 & u1 <= s ) by A18, XXREAL_1:1;
then ( x - t < u1 & u1 < x + t ) by A16, A17, XXREAL_0:2;
hence u in ].(x - t),(x + t).[ by XXREAL_1:4; :: thesis: verum
end;
hence ].(x - t),(x + t).[ /\ [.r,s.] = [.r,s.] by XBOOLE_1:17, XBOOLE_1:19; :: thesis: verum
end;