theorem Th53: :: SPRECT_2:53
for f being constant standard special_circular_sequence holds (E-min (L~ f)) `2 < (E-max (L~ f)) `2