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))

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

hence
Tcircle ((0. (TOP-REAL 2)),r) is SubSpace of Trectangle ((- r),r,(- r),r)
by TSEP_1:4; :: thesis: verum
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;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