let p1, p2 be Point of (TOP-REAL 2); 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); 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; ( 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
; (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; JORDAN24:def 1 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); ( 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
; 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; verum