let p1, p2 be Point of (TOP-REAL 2); :: thesis: for P being Subset of (TOP-REAL 2)
for A being Real st p1,p2 realize-max-dist-in P holds
(Rotate A) . p1,(Rotate A) . p2 realize-max-dist-in (Rotate A) .: P
let P be Subset of (TOP-REAL 2); :: thesis: for A being Real st p1,p2 realize-max-dist-in P holds
(Rotate A) . p1,(Rotate A) . p2 realize-max-dist-in (Rotate A) .: P
let A be Real; :: thesis: ( p1,p2 realize-max-dist-in P implies (Rotate A) . p1,(Rotate A) . p2 realize-max-dist-in (Rotate A) .: P )
reconsider f = Rotate A as Function of (TopSpaceMetr (Euclid 2)),(TopSpaceMetr (Euclid 2)) by Lm1;
set C = P;
A1: dom (Rotate A) = the carrier of (TOP-REAL 2) by FUNCT_2:def 1;
assume A2: p1,p2 realize-max-dist-in P ; :: thesis: (Rotate A) . p1,(Rotate A) . p2 realize-max-dist-in (Rotate A) .: P
then ( p1 in P & p2 in P ) ;
hence ( (Rotate A) . p1 in (Rotate A) .: P & (Rotate A) . p2 in (Rotate A) .: P ) by A1, FUNCT_1:def 6; :: according to JORDAN24:def 1 :: thesis: for x, y being Point of (TOP-REAL 2) st x in (Rotate A) .: P & y in (Rotate A) .: P holds
dist (((Rotate A) . p1),((Rotate A) . p2)) >= dist (x,y)
let x, y be Point of (TOP-REAL 2); :: thesis: ( x in (Rotate A) .: P & y in (Rotate A) .: P implies dist (((Rotate A) . p1),((Rotate A) . p2)) >= dist (x,y) )
assume that
A3: x in (Rotate A) .: P and
A4: y in (Rotate A) .: P ; :: thesis: dist (((Rotate A) . p1),((Rotate A) . p2)) >= dist (x,y)
f is isometric by Th2;
then consider g being isometric Function of (Euclid 2),(Euclid 2) such that
A5: f = g ;
consider yy being object such that
A6: yy in dom (Rotate A) and
A7: yy in P and
A8: (Rotate A) . yy = y by A4, FUNCT_1:def 6;
reconsider yy = yy as Point of (TOP-REAL 2) by A6;
consider xx being object such that
A9: xx in dom (Rotate A) and
A10: xx in P and
A11: (Rotate A) . xx = x by A3, FUNCT_1:def 6;
reconsider xx = xx as Point of (TOP-REAL 2) by A9;
reconsider p19 = p1, p29 = p2, xx9 = xx, yy9 = yy as Point of (Euclid 2) by EUCLID:67;
dist (p1,p2) >= dist (xx,yy) by A2, A10, A7;
then dist (p19,p29) >= dist (xx,yy) by TOPREAL6:def 1;
then dist (p19,p29) >= dist (xx9,yy9) by TOPREAL6:def 1;
then dist ((g . p19),(g . p29)) >= dist (xx9,yy9) by VECTMETR:def 3;
then dist ((g . p19),(g . p29)) >= dist ((g . xx9),(g . yy9)) by VECTMETR:def 3;
then dist (((Rotate A) . p1),((Rotate A) . p2)) >= dist ((g . xx9),(g . yy9)) by A5, TOPREAL6:def 1;
hence dist (((Rotate A) . p1),((Rotate A) . p2)) >= dist (x,y) by A11, A8, A5, TOPREAL6:def 1; :: thesis: verum