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 that
A1: 1 <= i and
A2: j <= width (GoB f) and
A3: 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
A4: x in LSeg ((GoB f) * (len (GoB f)),1),((GoB f) * (len (GoB f)),i) and
A5: 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 A4;
A6: 1 <= len (GoB f) by GOBOARD7:34;
A7: i <= width (GoB f) by A2, A3, 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 A6, A7, GOBOARD5:5; :: thesis: verum

end;

end;

end;

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