let f be V8() standard special_circular_sequence; :: thesis: for i, j being 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 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))))) ;
then consider x being object 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:32;
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:4; :: thesis: verum
end;
end;
end;
then A8: x1 `2 <= ((GoB f) * ((len (GoB f)),i)) `2 by A4, TOPREAL1:4;
A9: ((GoB f) * ((len (GoB f)),j)) `2 > ((GoB f) * ((len (GoB f)),i)) `2 by A1, A2, A3, A6, GOBOARD5:4;
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:4; :: 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:4;
hence contradiction by A8, A9, XXREAL_0:2; :: thesis: verum