let f be non constant standard special_circular_sequence; :: thesis: for i, j being Element of 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 Element of 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 A1: ( 1 <= i & j <= len (GoB f) & 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))) by XBOOLE_0:def 7;
then consider x being set such that
A2: ( x in LSeg ((GoB f) * 1,(width (GoB f))),((GoB f) * i,(width (GoB f))) & 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 A2;
A3: ( 1 <= width (GoB f) & 1 <= i & i <= len (GoB f) ) by A1, GOBOARD7:35, 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 A3, GOBOARD5:4; :: thesis: verum

end;

end;

end;

then A4: ( x1 `1 >= ((GoB f) * 1,(width (GoB f))) `1 & x1 `1 <= ((GoB f) * i,(width (GoB f))) `1 ) by A2, TOPREAL1:9;
A5: ((GoB f) * j,(width (GoB f))) `1 > ((GoB f) * i,(width (GoB f))) `1 by A1, A3, GOBOARD5:4;
A6: 1 <= j by A1, 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 A1, 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 A3, A6, GOBOARD5:4; :: 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) * (len (GoB f)),(width (GoB f))) `1 & x1 `1 >= ((GoB f) * j,(width (GoB f))) `1 ) by A2, TOPREAL1:9;
hence contradiction by A4, A5, XXREAL_0:2; :: thesis: verum