id (TOP-REAL n) is base_rotation ;
hence ex b₁ being Function of (TOP-REAL n),(TOP-REAL n) st b₁ is base_rotation ; :: thesis: verum