let r, s, t, x be Real; ( ( 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 ( ( 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
;
].(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 ;
TARSKI:def 3 ( 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.]
;
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;
verum
end;
].(x - t),s.] c= ].(x - t),(x + t).[ /\ [.r,s.]
proof
let u be
object ;
TARSKI:def 3 ( not u in ].(x - t),s.] or u in ].(x - t),(x + t).[ /\ [.r,s.] )
assume A9:
u in ].(x - t),s.]
;
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;
verum
end; hence
].(x - t),(x + t).[ /\ [.r,s.] = ].(x - t),s.]
by A6;
verum
end;
hereby ( 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
;
].(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 ;
TARSKI:def 3 ( 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.]
;
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;
verum
end;
[.r,(x + t).[ c= ].(x - t),(x + t).[ /\ [.r,s.]
proof
let u be
object ;
TARSKI:def 3 ( not u in [.r,(x + t).[ or u in ].(x - t),(x + t).[ /\ [.r,s.] )
assume A15:
u in [.r,(x + t).[
;
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;
verum
end; hence
].(x - t),(x + t).[ /\ [.r,s.] = [.r,(x + t).[
by A12;
verum
end;