let r be Real; :: 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 object ; :: 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))
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; :: thesis: verum

end;

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