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) )
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) ; :: 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 A2, PRE_TOPC:55;
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: abs (x `2 ) <= |.x.| by JGRAPH_1:50;
then A5: - r <= x `2 by A3, ABSVALUE:12;
A6: abs (x `1 ) <= |.x.| by JGRAPH_1:50;
then A7: x `1 <= r by A3, ABSVALUE:12;
A8: the carrier of (Trectangle (- r),r,(- r),r) = closed_inside_of_rectangle (- r),r,(- r),r by PRE_TOPC:29;
A9: x `2 <= r by A3, A4, ABSVALUE:12;
- r <= x `1 by A3, A6, ABSVALUE:12;
hence x in the carrier of (Trectangle (- r),r,(- r),r) by A1, A8, A7, A5, A9; :: thesis: verum

end;

hence Tcircle (0. (TOP-REAL 2)),r is SubSpace of Trectangle (- r),r,(- r),r by TSEP_1:4; :: thesis: verum