let f be non constant standard special_circular_sequence; :: thesis: for i, j being Element of NAT st 1 <= i & j <= width (GoB f) & i < j holds
(LSeg ((GoB f) * (len (GoB f)),1),((GoB f) * (len (GoB f)),i)) /\ (LSeg ((GoB f) * (len (GoB f)),j),((GoB f) * (len (GoB f)),(width (GoB f)))) = {}
let i, j be Element of NAT ; :: thesis: ( 1 <= i & j <= width (GoB f) & i < j implies (LSeg ((GoB f) * (len (GoB f)),1),((GoB f) * (len (GoB f)),i)) /\ (LSeg ((GoB f) * (len (GoB f)),j),((GoB f) * (len (GoB f)),(width (GoB f)))) = {} )
assume A1: ( 1 <= i & j <= width (GoB f) & i < j ) ; :: thesis: (LSeg ((GoB f) * (len (GoB f)),1),((GoB f) * (len (GoB f)),i)) /\ (LSeg ((GoB f) * (len (GoB f)),j),((GoB f) * (len (GoB f)),(width (GoB f)))) = {}
set A = LSeg ((GoB f) * (len (GoB f)),1),((GoB f) * (len (GoB f)),i);
set B = LSeg ((GoB f) * (len (GoB f)),j),((GoB f) * (len (GoB f)),(width (GoB f)));
assume (LSeg ((GoB f) * (len (GoB f)),1),((GoB f) * (len (GoB f)),i)) /\ (LSeg ((GoB f) * (len (GoB f)),j),((GoB f) * (len (GoB f)),(width (GoB f)))) <> {} ; :: thesis: contradiction
then LSeg ((GoB f) * (len (GoB f)),1),((GoB f) * (len (GoB f)),i) meets LSeg ((GoB f) * (len (GoB f)),j),((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) * (len (GoB f)),1),((GoB f) * (len (GoB f)),i) & x in LSeg ((GoB f) * (len (GoB f)),j),((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 <= len (GoB f) & 1 <= i & i <= width (GoB f) ) by A1, GOBOARD7:34, XXREAL_0:2;
((GoB f) * (len (GoB f)),1) `2 <= ((GoB f) * (len (GoB f)),i) `2

proof

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

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

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

end;

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

hence ((GoB f) * (len (GoB f)),1) `2 <= ((GoB f) * (len (GoB f)),i) `2 by A3, GOBOARD5:5; :: thesis: verum

end;

end;

end;

then A4: ( x1 `2 >= ((GoB f) * (len (GoB f)),1) `2 & x1 `2 <= ((GoB f) * (len (GoB f)),i) `2 ) by A2, TOPREAL1:10;
A5: ((GoB f) * (len (GoB f)),j) `2 > ((GoB f) * (len (GoB f)),i) `2 by A1, A3, GOBOARD5:5;
A6: 1 <= j by A1, XXREAL_0:2;
((GoB f) * (len (GoB f)),j) `2 <= ((GoB f) * (len (GoB f)),(width (GoB f))) `2

proof

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

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

hence ((GoB f) * (len (GoB f)),j) `2 <= ((GoB f) * (len (GoB f)),(width (GoB f))) `2 by A3, A6, GOBOARD5:5; :: thesis: verum

end;

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

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

end;

end;

end;

then ( x1 `2 <= ((GoB f) * (len (GoB f)),(width (GoB f))) `2 & x1 `2 >= ((GoB f) * (len (GoB f)),j) `2 ) by A2, TOPREAL1:10;
hence contradiction by A4, A5, XXREAL_0:2; :: thesis: verum