let r be Real; :: thesis: Tcircle ((0. ()),r) is SubSpace of Trectangle ((- r),r,(- r),r)
set C = Tcircle ((0. ()),r);
set T = Trectangle ((- r),r,(- r),r);
the carrier of (Tcircle ((0. ()),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. ()),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 () : ( - 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. ()),r)) ; :: thesis: x in the carrier of (Trectangle ((- r),r,(- r),r))
reconsider x = x as Point of () by ;
the carrier of (Tcircle ((0. ()),r)) = Sphere ((0. ()),r) by Th9;
then A3: |.x.| = r by ;
A4: |.(x `2).| <= |.x.| by JGRAPH_1:33;
then A5: - r <= x `2 by ;
A6: |.(x `1).| <= |.x.| by JGRAPH_1:33;
then A7: x `1 <= r by ;
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 ;
- r <= x `1 by ;
hence x in the carrier of (Trectangle ((- r),r,(- r),r)) by A1, A8, A7, A5, A9; :: thesis: verum
end;
hence Tcircle ((0. ()),r) is SubSpace of Trectangle ((- r),r,(- r),r) by TSEP_1:4; :: thesis: verum