let f be non empty FinSequence of (TOP-REAL 2); :: thesis: for i, j being Element of NAT st f is special & i <= len (GoB f) & j <= width (GoB f) holds
Int (cell (GoB f),i,j) misses L~ f
let i, j be Element of NAT ; :: thesis: ( f is special & i <= len (GoB f) & j <= width (GoB f) implies Int (cell (GoB f),i,j) misses L~ f )
assume that
A1: f is special and
A2: i <= len (GoB f) and
A3: j <= width (GoB f) ; :: thesis: Int (cell (GoB f),i,j) misses L~ f
assume Int (cell (GoB f),i,j) meets L~ f ; :: thesis: contradiction
then consider x being set such that
A4: x in Int (cell (GoB f),i,j) and
A5: x in L~ f by XBOOLE_0:3;
L~ f = union { (LSeg f,k) where k is Element of NAT : ( 1 <= k & k + 1 <= len f ) } by TOPREAL1:def 6;
then consider X being set such that
A6: x in X and
A7: X in { (LSeg f,k) where k is Element of NAT : ( 1 <= k & k + 1 <= len f ) } by A5, TARSKI:def 4;
consider k being Element of NAT such that
A8: X = LSeg f,k and
( 1 <= k & k + 1 <= len f ) by A7;
reconsider p = x as Point of (TOP-REAL 2) by A6, A8;
A9: Int (cell (GoB f),i,j) = Int ((v_strip (GoB f),i) /\ (h_strip (GoB f),j)) by GOBOARD5:def 3
.= (Int (v_strip (GoB f),i)) /\ (Int (h_strip (GoB f),j)) by TOPS_1:46 ;

per cases ( LSeg f,k is horizontal or LSeg f,k is vertical ) by A1, SPPOL_1:41;

suppose LSeg f,k is horizontal ; :: thesis: contradiction

then consider j0 being Element of NAT such that
A10: ( 1 <= j0 & j0 <= width (GoB f) ) and
A11: for p being Point of (TOP-REAL 2) st p in LSeg f,k holds
p `2 = ((GoB f) * 1,j0) `2 by Th12;

now

assume A12: p in Int (h_strip (GoB f),j) ; :: thesis: contradiction
A13: ( j0 > j implies j0 >= j + 1 ) by NAT_1:13;

per cases ( j0 < j or j0 = j or j0 > j + 1 or j0 = j + 1 ) by A13, XXREAL_0:1;

suppose A14: j0 < j ; :: thesis: contradiction

then j >= 1 by A10, XXREAL_0:2;
then A15: p `2 > ((GoB f) * 1,j) `2 by A3, A12, GOBOARD6:30;
0 <> len (GoB f) by GOBOARD1:def 5;
then 1 <= len (GoB f) by NAT_1:14;
then ((GoB f) * 1,j) `2 > ((GoB f) * 1,j0) `2 by A3, A10, A14, GOBOARD5:5;
hence contradiction by A6, A8, A11, A15; :: thesis: verum

end;

suppose j0 = j ; :: thesis: contradiction

then p `2 > ((GoB f) * 1,j0) `2 by A10, A12, GOBOARD6:30;
hence contradiction by A6, A8, A11; :: thesis: verum

end;

suppose A16: j0 > j + 1 ; :: thesis: contradiction

then j + 1 <= width (GoB f) by A10, XXREAL_0:2;
then j < width (GoB f) by NAT_1:13;
then A17: p `2 < ((GoB f) * 1,(j + 1)) `2 by A12, GOBOARD6:31;
0 <> len (GoB f) by GOBOARD1:def 5;
then ( 1 <= len (GoB f) & j + 1 >= 1 ) by NAT_1:11, NAT_1:14;
then ((GoB f) * 1,(j + 1)) `2 < ((GoB f) * 1,j0) `2 by A10, A16, GOBOARD5:5;
hence contradiction by A6, A8, A11, A17; :: thesis: verum

end;

suppose A18: j0 = j + 1 ; :: thesis: contradiction

then j < width (GoB f) by A10, NAT_1:13;
then p `2 < ((GoB f) * 1,j0) `2 by A12, A18, GOBOARD6:31;
hence contradiction by A6, A8, A11; :: thesis: verum

end;

end;

end;

hence contradiction by A4, A9, XBOOLE_0:def 4; :: thesis: verum

end;

suppose LSeg f,k is vertical ; :: thesis: contradiction

then consider i0 being Element of NAT such that
A19: ( 1 <= i0 & i0 <= len (GoB f) ) and
A20: for p being Point of (TOP-REAL 2) st p in LSeg f,k holds
p `1 = ((GoB f) * i0,1) `1 by Th13;

now

assume A21: p in Int (v_strip (GoB f),i) ; :: thesis: contradiction
A22: ( i0 > i implies i0 >= i + 1 ) by NAT_1:13;

per cases ( i0 < i or i0 = i or i0 > i + 1 or i0 = i + 1 ) by A22, XXREAL_0:1;

suppose A23: i0 < i ; :: thesis: contradiction

then i >= 1 by A19, XXREAL_0:2;
then A24: p `1 > ((GoB f) * i,1) `1 by A2, A21, GOBOARD6:32;
0 <> width (GoB f) by GOBOARD1:def 5;
then 1 <= width (GoB f) by NAT_1:14;
then ((GoB f) * i,1) `1 > ((GoB f) * i0,1) `1 by A2, A19, A23, GOBOARD5:4;
hence contradiction by A6, A8, A20, A24; :: thesis: verum

end;

suppose i0 = i ; :: thesis: contradiction

then p `1 > ((GoB f) * i0,1) `1 by A19, A21, GOBOARD6:32;
hence contradiction by A6, A8, A20; :: thesis: verum

end;

suppose A25: i0 > i + 1 ; :: thesis: contradiction

then i + 1 <= len (GoB f) by A19, XXREAL_0:2;
then i < len (GoB f) by NAT_1:13;
then A26: p `1 < ((GoB f) * (i + 1),1) `1 by A21, GOBOARD6:33;
0 <> width (GoB f) by GOBOARD1:def 5;
then ( 1 <= width (GoB f) & i + 1 >= 1 ) by NAT_1:11, NAT_1:14;
then ((GoB f) * (i + 1),1) `1 < ((GoB f) * i0,1) `1 by A19, A25, GOBOARD5:4;
hence contradiction by A6, A8, A20, A26; :: thesis: verum

end;

suppose A27: i0 = i + 1 ; :: thesis: contradiction

then i < len (GoB f) by A19, NAT_1:13;
then p `1 < ((GoB f) * i0,1) `1 by A21, A27, GOBOARD6:33;
hence contradiction by A6, A8, A20; :: thesis: verum

end;

end;

end;

hence contradiction by A4, A9, XBOOLE_0:def 4; :: thesis: verum

end;

end;