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)));
assume not f is clockwise_oriented ; :: thesis: contradiction
then not Rotate (f,(N-min (L~ f))) is clockwise_oriented by Th40;
then A2: Rev (Rotate (f,(N-min (L~ f)))) is clockwise_oriented by REVROT_1:38;
L~ f = L~ (Rotate (f,(N-min (L~ f)))) by REVROT_1:33;
then UBD (L~ f) = UBD (L~ (Rev (Rotate (f,(N-min (L~ f)))))) by SPPOL_2:22
.= LeftComp (Rev (Rotate (f,(N-min (L~ f))))) by A2, GOBRD14:36
.= RightComp (Rotate (f,(N-min (L~ f)))) by GOBOARD9:23
.= RightComp f by REVROT_1:37 ;
hence contradiction by A1, SPRECT_4:6; :: thesis: verum