let r be Real; 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
object ;
TARSKI:def 3 ( not x in the carrier of (Tcircle ((0. (TOP-REAL 2)),r)) or x in the carrier of (Trectangle ((- r),r,(- r),r)) )
A1:
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;
assume A2:
x in the
carrier of
(Tcircle ((0. (TOP-REAL 2)),r))
;
x in the carrier of (Trectangle ((- r),r,(- r),r))
reconsider x =
x as
Point of
(TOP-REAL 2) by A2, PRE_TOPC:25;
the
carrier of
(Tcircle ((0. (TOP-REAL 2)),r)) = Sphere (
(0. (TOP-REAL 2)),
r)
by Th9;
then A3:
|.x.| = r
by A2, TOPREAL9:12;
A4:
|.(x `2).| <= |.x.|
by JGRAPH_1:33;
then A5:
- r <= x `2
by A3, ABSVALUE:5;
A6:
|.(x `1).| <= |.x.|
by JGRAPH_1:33;
then A7:
x `1 <= r
by A3, ABSVALUE:5;
A8:
the
carrier of
(Trectangle ((- r),r,(- r),r)) = closed_inside_of_rectangle (
(- r),
r,
(- r),
r)
by PRE_TOPC:8;
A9:
x `2 <= r
by A3, A4, ABSVALUE:5;
- r <= x `1
by A3, A6, ABSVALUE:5;
hence
x in the
carrier of
(Trectangle ((- r),r,(- r),r))
by A1, A8, A7, A5, A9;
verum
end;
hence
Tcircle ((0. (TOP-REAL 2)),r) is SubSpace of Trectangle ((- r),r,(- r),r)
by TSEP_1:4; verum