let r be real number ; :: thesis: Tcircle (0. (TOP-REAL 2)),r is SubSpace of Trectangle (- r),r,(- r),r
set C = Tcircle (0. (TOP-REAL 2)),r;
set T = Trectangle (- r),r,(- r),r;
the carrier of (Tcircle (0. (TOP-REAL 2)),r) c= the carrier of (Trectangle (- r),r,(- r),r)
proof
let x be
set ;
:: according to TARSKI:def 3 :: thesis: ( not x in the carrier of (Tcircle (0. (TOP-REAL 2)),r) or x in the carrier of (Trectangle (- r),r,(- r),r) )
assume A1:
x in the
carrier of
(Tcircle (0. (TOP-REAL 2)),r)
;
:: thesis: x in the carrier of (Trectangle (- r),r,(- r),r)
then
not
Tcircle (0. (TOP-REAL 2)),
r is
empty
;
then reconsider x =
x as
Point of
(TOP-REAL 2) by A1, PRE_TOPC:55;
A2:
closed_inside_of_rectangle (- r),
r,
(- r),
r = { p where p is Point of (TOP-REAL 2) : ( - r <= p `1 & p `1 <= r & - r <= p `2 & p `2 <= r ) }
by JGRAPH_6:def 2;
A3:
the
carrier of
(Trectangle (- r),r,(- r),r) = closed_inside_of_rectangle (- r),
r,
(- r),
r
by PRE_TOPC:29;
the
carrier of
(Tcircle (0. (TOP-REAL 2)),r) = Sphere (0. (TOP-REAL 2)),
r
by Th9;
then A4:
|.x.| = r
by A1, TOPREAL9:12;
(
abs (x `1 ) <= |.x.| &
abs (x `2 ) <= |.x.| )
by JGRAPH_1:50;
then
(
- r <= x `1 &
x `1 <= r &
- r <= x `2 &
x `2 <= r )
by A4, ABSVALUE:12;
hence
x in the
carrier of
(Trectangle (- r),r,(- r),r)
by A2, A3;
:: thesis: verum
end;
hence
Tcircle (0. (TOP-REAL 2)),r is SubSpace of Trectangle (- r),r,(- r),r
by TSEP_1:4; :: thesis: verum