let r be non negative Real; :: thesis: for s being Real holds (Rotate s) .: (Sphere ((0. (TOP-REAL 2)),r)) = Sphere ((0. (TOP-REAL 2)),r)
let s be Real; :: thesis: (Rotate s) .: (Sphere ((0. (TOP-REAL 2)),r)) = Sphere ((0. (TOP-REAL 2)),r)
set f = Rotate s;
set C = Sphere ((0. (TOP-REAL 2)),r);
thus (Rotate s) .: (Sphere ((0. (TOP-REAL 2)),r)) c= Sphere ((0. (TOP-REAL 2)),r) :: according to XBOOLE_0:def 10 :: thesis: Sphere ((0. (TOP-REAL 2)),r) c= (Rotate s) .: (Sphere ((0. (TOP-REAL 2)),r))
proof
let y be Point of (TOP-REAL 2); :: according to LATTICE7:def 1 :: thesis: ( not y in (Rotate s) .: (Sphere ((0. (TOP-REAL 2)),r)) or y in Sphere ((0. (TOP-REAL 2)),r) )
assume y in (Rotate s) .: (Sphere ((0. (TOP-REAL 2)),r)) ; :: thesis: y in Sphere ((0. (TOP-REAL 2)),r)
then ex c being Element of (TOP-REAL 2) st
( c in Sphere ((0. (TOP-REAL 2)),r) & y = (Rotate s) . c ) by FUNCT_2:65;
hence y in Sphere ((0. (TOP-REAL 2)),r) by Th48; :: thesis: verum
end;
let y be Point of (TOP-REAL 2); :: according to LATTICE7:def 1 :: thesis: ( not y in Sphere ((0. (TOP-REAL 2)),r) or y in (Rotate s) .: (Sphere ((0. (TOP-REAL 2)),r)) )
set x = (Rotate (- s)) . y;
assume y in Sphere ((0. (TOP-REAL 2)),r) ; :: thesis: y in (Rotate s) .: (Sphere ((0. (TOP-REAL 2)),r))
then (Rotate (- s)) . y in Sphere ((0. (TOP-REAL 2)),r) by Th48;
then (Rotate s) . ((Rotate (- s)) . y) in (Rotate s) .: (Sphere ((0. (TOP-REAL 2)),r)) by FUNCT_2:35;
hence y in (Rotate s) .: (Sphere ((0. (TOP-REAL 2)),r)) by Th46; :: thesis: verum