let f be constant standard special_circular_sequence; :: thesis: for i, j being Nat st 1 <= i & j <= len (GoB f) & i < j holds
(LSeg (((GoB f) * (1,(width (GoB f)))),((GoB f) * (i,(width (GoB f)))))) /\ (LSeg (((GoB f) * (j,(width (GoB f)))),((GoB f) * ((len (GoB f)),(width (GoB f)))))) = {}
let i, j be Nat; :: thesis: ( 1 <= i & j <= len (GoB f) & i < j implies (LSeg (((GoB f) * (1,(width (GoB f)))),((GoB f) * (i,(width (GoB f)))))) /\ (LSeg (((GoB f) * (j,(width (GoB f)))),((GoB f) * ((len (GoB f)),(width (GoB f)))))) = {} )
assume that
A1: 1 <= i and
A2: j <= len (GoB f) and
A3: i < j ; :: thesis: (LSeg (((GoB f) * (1,(width (GoB f)))),((GoB f) * (i,(width (GoB f)))))) /\ (LSeg (((GoB f) * (j,(width (GoB f)))),((GoB f) * ((len (GoB f)),(width (GoB f)))))) = {}
set A = LSeg (((GoB f) * (1,(width (GoB f)))),((GoB f) * (i,(width (GoB f)))));
set B = LSeg (((GoB f) * (j,(width (GoB f)))),((GoB f) * ((len (GoB f)),(width (GoB f)))));
assume (LSeg (((GoB f) * (1,(width (GoB f)))),((GoB f) * (i,(width (GoB f)))))) /\ (LSeg (((GoB f) * (j,(width (GoB f)))),((GoB f) * ((len (GoB f)),(width (GoB f)))))) <> {} ; :: thesis: contradiction
then LSeg (((GoB f) * (1,(width (GoB f)))),((GoB f) * (i,(width (GoB f))))) meets LSeg (((GoB f) * (j,(width (GoB f)))),((GoB f) * ((len (GoB f)),(width (GoB f))))) ;
then consider x being object such that
A4: x in LSeg (((GoB f) * (1,(width (GoB f)))),((GoB f) * (i,(width (GoB f))))) and
A5: x in LSeg (((GoB f) * (j,(width (GoB f)))),((GoB f) * ((len (GoB f)),(width (GoB f))))) by XBOOLE_0:3;
reconsider x1 = x as Point of (TOP-REAL 2) by A4;
A6: 1 <= width (GoB f) by GOBOARD7:33;
A7: i <= len (GoB f) by A2, A3, XXREAL_0:2;
((GoB f) * (1,(width (GoB f)))) `1 <= ((GoB f) * (i,(width (GoB f)))) `1

proof

per cases ( i = 1 or i > 1 ) by A1, XXREAL_0:1;

suppose i = 1 ; :: thesis: ((GoB f) * (1,(width (GoB f)))) `1 <= ((GoB f) * (i,(width (GoB f)))) `1

hence ((GoB f) * (1,(width (GoB f)))) `1 <= ((GoB f) * (i,(width (GoB f)))) `1 ; :: thesis: verum

end;

suppose i > 1 ; :: thesis: ((GoB f) * (1,(width (GoB f)))) `1 <= ((GoB f) * (i,(width (GoB f)))) `1

hence ((GoB f) * (1,(width (GoB f)))) `1 <= ((GoB f) * (i,(width (GoB f)))) `1 by A6, A7, GOBOARD5:3; :: thesis: verum

end;

end;

end;

then A8: x1 `1 <= ((GoB f) * (i,(width (GoB f)))) `1 by A4, TOPREAL1:3;
A9: ((GoB f) * (j,(width (GoB f)))) `1 > ((GoB f) * (i,(width (GoB f)))) `1 by A1, A2, A3, A6, GOBOARD5:3;
A10: 1 <= j by A1, A3, XXREAL_0:2;
((GoB f) * (j,(width (GoB f)))) `1 <= ((GoB f) * ((len (GoB f)),(width (GoB f)))) `1

proof

per cases ( j < len (GoB f) or j = len (GoB f) ) by A2, XXREAL_0:1;

suppose j < len (GoB f) ; :: thesis: ((GoB f) * (j,(width (GoB f)))) `1 <= ((GoB f) * ((len (GoB f)),(width (GoB f)))) `1

hence ((GoB f) * (j,(width (GoB f)))) `1 <= ((GoB f) * ((len (GoB f)),(width (GoB f)))) `1 by A6, A10, GOBOARD5:3; :: thesis: verum

end;

suppose j = len (GoB f) ; :: thesis: ((GoB f) * (j,(width (GoB f)))) `1 <= ((GoB f) * ((len (GoB f)),(width (GoB f)))) `1

hence ((GoB f) * (j,(width (GoB f)))) `1 <= ((GoB f) * ((len (GoB f)),(width (GoB f)))) `1 ; :: thesis: verum

end;

end;

end;

then x1 `1 >= ((GoB f) * (j,(width (GoB f)))) `1 by A5, TOPREAL1:3;
hence contradiction by A8, A9, XXREAL_0:2; :: thesis: verum