let f be non constant standard special_circular_sequence; :: thesis: ( LeftComp f = UBD (L~ f) implies f is clockwise_oriented )
assume A1: LeftComp f = UBD (L~ f) ; :: thesis: f is clockwise_oriented
set g = Rotate f,(N-min (L~ f));
A2: L~ f = L~ (Rotate f,(N-min (L~ f))) by REVROT_1:33;
assume not f is clockwise_oriented ; :: thesis: contradiction
then not Rotate f,(N-min (L~ f)) is clockwise_oriented by Th48;
then A3: Rev (Rotate f,(N-min (L~ f))) is clockwise_oriented by REVROT_1:38;
UBD (L~ f) = UBD (L~ (Rev (Rotate f,(N-min (L~ f))))) by A2, SPPOL_2:22
.= LeftComp (Rev (Rotate f,(N-min (L~ f)))) by A3, GOBRD14:46
.= RightComp (Rotate f,(N-min (L~ f))) by GOBOARD9:26
.= RightComp f by REVROT_1:37 ;
hence contradiction by A1, SPRECT_4:7; :: thesis: verum