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
set C = 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 )
assume A2: p1,p2 realize-max-dist-in P ; :: thesis: (Rotate A) . p1,(Rotate A) . p2 realize-max-dist-in (Rotate A) .: P
then A3: ( p1 in P & p2 in P & ( for x, y being Point of (TOP-REAL 2) st x in P & y in P holds
dist p1,p2 >= dist x,y ) ) by Def1;
dom (Rotate A) = the carrier of (TOP-REAL 2) by FUNCT_2:def 1;
hence ( (Rotate A) . p1 in (Rotate A) .: P & (Rotate A) . p2 in (Rotate A) .: P ) by A3, FUNCT_1:def 12; :: 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 A4: ( x in (Rotate A) .: P & y in (Rotate A) .: P ) ; :: thesis: dist ((Rotate A) . p1),((Rotate A) . p2) >= dist x,y
consider xx being set such that
A5: ( xx in dom (Rotate A) & xx in P & (Rotate A) . xx = x ) by A4, FUNCT_1:def 12;
reconsider xx = xx as Point of (TOP-REAL 2) by A5;
consider yy being set such that
A6: ( yy in dom (Rotate A) & yy in P & (Rotate A) . yy = y ) by A4, FUNCT_1:def 12;
reconsider yy = yy as Point of (TOP-REAL 2) by A6;
reconsider f = Rotate A as Function of (TopSpaceMetr (Euclid 2)),(TopSpaceMetr (Euclid 2)) by XX;
f is isometric by Th2;
then consider g being isometric Function of (Euclid 2),(Euclid 2) such that
A7: f = g by Def2;
reconsider p1' = p1, p2' = p2, xx' = xx, yy' = yy as Point of (Euclid 2) by EUCLID:71;
dist p1,p2 >= dist xx,yy by A2, A5, A6, Def1;
then dist p1',p2' >= dist xx,yy by TOPREAL6:def 1;
then dist p1',p2' >= dist xx',yy' by TOPREAL6:def 1;
then dist (g . p1'),(g . p2') >= dist xx',yy' by VECTMETR:def 3;
then dist (g . p1'),(g . p2') >= dist (g . xx'),(g . yy') by VECTMETR:def 3;
then dist ((Rotate A) . p1),((Rotate A) . p2) >= dist (g . xx'),(g . yy') by A7, TOPREAL6:def 1;
hence dist ((Rotate A) . p1),((Rotate A) . p2) >= dist x,y by A5, A6, A7, TOPREAL6:def 1; :: thesis: verum