let i, j be Nat; :: thesis: for G being Go-board
for p being Point of (TOP-REAL 2) st 1 <= i & i + 1 <= len G & 1 <= j & j + 1 <= width G & p in Values G & p in cell (G,i,j) holds
p is_extremal_in cell (G,i,j)
let G be Go-board; :: thesis: for p being Point of (TOP-REAL 2) st 1 <= i & i + 1 <= len G & 1 <= j & j + 1 <= width G & p in Values G & p in cell (G,i,j) holds
p is_extremal_in cell (G,i,j)
let p be Point of (TOP-REAL 2); :: thesis: ( 1 <= i & i + 1 <= len G & 1 <= j & j + 1 <= width G & p in Values G & p in cell (G,i,j) implies p is_extremal_in cell (G,i,j) )
assume that
A1: ( 1 <= i & i + 1 <= len G & 1 <= j & j + 1 <= width G ) and
A2: p in Values G and
A3: p in cell (G,i,j) ; :: thesis: p is_extremal_in cell (G,i,j)
for a, b being Point of (TOP-REAL 2) st p in LSeg (a,b) & LSeg (a,b) c= cell (G,i,j) & not p = a holds
p = b

proof

let a, b be Point of (TOP-REAL 2); :: thesis: ( p in LSeg (a,b) & LSeg (a,b) c= cell (G,i,j) & not p = a implies p = b )
assume that
A4: p in LSeg (a,b) and
A5: LSeg (a,b) c= cell (G,i,j) ; :: thesis: ( p = a or p = b )
A6: a in LSeg (a,b) by RLTOPSP1:68;
A7: b in LSeg (a,b) by RLTOPSP1:68;
assume that
A8: a <> p and
A9: b <> p ; :: thesis: contradiction

per cases ( p = G * (i,j) or p = G * (i,(j + 1)) or p = G * ((i + 1),(j + 1)) or p = G * ((i + 1),j) ) by A1, A2, A3, Th19;

suppose A10: p = G * (i,j) ; :: thesis: contradiction

then A11: p `2 <= b `2 by A1, A5, A7, Th17;
A12: p `1 <= a `1 by A1, A5, A6, A10, Th17;
A13: p `1 <= b `1 by A1, A5, A7, A10, Th17;
A14: p `2 <= a `2 by A1, A5, A6, A10, Th17;

now :: thesis: contradiction

per cases ( ( a `1 <= b `1 & a `2 <= b `2 ) or ( a `1 <= b `1 & b `2 < a `2 ) or ( b `1 < a `1 & a `2 <= b `2 ) or ( b `1 < a `1 & b `2 < a `2 ) ) ;

suppose A15: ( a `1 <= b `1 & a `2 <= b `2 ) ; :: thesis: contradiction

then a `2 <= p `2 by A4, TOPREAL1:4;
then A16: a `2 = p `2 by A14, XXREAL_0:1;
a `1 <= p `1 by A4, A15, TOPREAL1:3;
then a `1 = p `1 by A12, XXREAL_0:1;
hence contradiction by A8, A16, TOPREAL3:6; :: thesis: verum

end;

suppose A17: ( a `1 <= b `1 & b `2 < a `2 ) ; :: thesis: contradiction

then b `2 <= p `2 by A4, TOPREAL1:4;
then A18: b `2 = p `2 by A11, XXREAL_0:1;
A19: a `1 <= p `1 by A4, A17, TOPREAL1:3;
then A20: a `1 = p `1 by A12, XXREAL_0:1;
then a `2 <> p `2 by A8, TOPREAL3:6;
then LSeg (a,b) is vertical by A4, A6, A12, A19, SPPOL_1:18, XXREAL_0:1;
then a `1 = b `1 by SPPOL_1:16;
hence contradiction by A9, A20, A18, TOPREAL3:6; :: thesis: verum

end;

suppose A21: ( b `1 < a `1 & a `2 <= b `2 ) ; :: thesis: contradiction

then a `2 <= p `2 by A4, TOPREAL1:4;
then A22: a `2 = p `2 by A14, XXREAL_0:1;
A23: b `1 <= p `1 by A4, A21, TOPREAL1:3;
then A24: b `1 = p `1 by A13, XXREAL_0:1;
then b `2 <> p `2 by A9, TOPREAL3:6;
then LSeg (a,b) is vertical by A4, A7, A13, A23, SPPOL_1:18, XXREAL_0:1;
then a `1 = b `1 by SPPOL_1:16;
hence contradiction by A8, A24, A22, TOPREAL3:6; :: thesis: verum

end;

suppose A25: ( b `1 < a `1 & b `2 < a `2 ) ; :: thesis: contradiction

then b `2 <= p `2 by A4, TOPREAL1:4;
then A26: b `2 = p `2 by A11, XXREAL_0:1;
b `1 <= p `1 by A4, A25, TOPREAL1:3;
then b `1 = p `1 by A13, XXREAL_0:1;
hence contradiction by A9, A26, TOPREAL3:6; :: thesis: verum

end;

end;

end;

hence contradiction ; :: thesis: verum

end;

suppose A27: p = G * (i,(j + 1)) ; :: thesis: contradiction

then A28: b `2 <= p `2 by A1, A5, A7, Th17;
A29: p `1 = (G * (i,j)) `1 by A1, A27, Th16;
then A30: p `1 <= a `1 by A1, A5, A6, Th17;
A31: p `1 <= b `1 by A1, A5, A7, A29, Th17;
A32: a `2 <= p `2 by A1, A5, A6, A27, Th17;

now :: thesis: contradiction

per cases ( ( a `1 <= b `1 & a `2 <= b `2 ) or ( a `1 <= b `1 & b `2 < a `2 ) or ( b `1 < a `1 & a `2 <= b `2 ) or ( b `1 < a `1 & b `2 < a `2 ) ) ;

suppose A33: ( a `1 <= b `1 & a `2 <= b `2 ) ; :: thesis: contradiction

then p `2 <= b `2 by A4, TOPREAL1:4;
then A34: b `2 = p `2 by A28, XXREAL_0:1;
A35: a `1 <= p `1 by A4, A33, TOPREAL1:3;
then A36: a `1 = p `1 by A30, XXREAL_0:1;
then a `2 <> p `2 by A8, TOPREAL3:6;
then LSeg (a,b) is vertical by A4, A6, A30, A35, SPPOL_1:18, XXREAL_0:1;
then a `1 = b `1 by SPPOL_1:16;
hence contradiction by A9, A36, A34, TOPREAL3:6; :: thesis: verum

end;

suppose A37: ( a `1 <= b `1 & b `2 < a `2 ) ; :: thesis: contradiction

then p `2 <= a `2 by A4, TOPREAL1:4;
then A38: a `2 = p `2 by A32, XXREAL_0:1;
a `1 <= p `1 by A4, A37, TOPREAL1:3;
then a `1 = p `1 by A30, XXREAL_0:1;
hence contradiction by A8, A38, TOPREAL3:6; :: thesis: verum

end;

suppose A39: ( b `1 < a `1 & a `2 <= b `2 ) ; :: thesis: contradiction

then p `2 <= b `2 by A4, TOPREAL1:4;
then A40: b `2 = p `2 by A28, XXREAL_0:1;
b `1 <= p `1 by A4, A39, TOPREAL1:3;
then b `1 = p `1 by A31, XXREAL_0:1;
hence contradiction by A9, A40, TOPREAL3:6; :: thesis: verum

end;

suppose A41: ( b `1 < a `1 & b `2 < a `2 ) ; :: thesis: contradiction

then p `2 <= a `2 by A4, TOPREAL1:4;
then A42: a `2 = p `2 by A32, XXREAL_0:1;
A43: b `1 <= p `1 by A4, A41, TOPREAL1:3;
then A44: b `1 = p `1 by A31, XXREAL_0:1;
then b `2 <> p `2 by A9, TOPREAL3:6;
then LSeg (a,b) is vertical by A4, A7, A31, A43, SPPOL_1:18, XXREAL_0:1;
then a `1 = b `1 by SPPOL_1:16;
hence contradiction by A8, A44, A42, TOPREAL3:6; :: thesis: verum

end;

end;

end;

hence contradiction ; :: thesis: verum

end;

suppose A45: p = G * ((i + 1),(j + 1)) ; :: thesis: contradiction

then A46: p `1 = (G * ((i + 1),j)) `1 by A1, Th16;
then A47: a `1 <= p `1 by A1, A5, A6, Th17;
A48: p `2 = (G * (i,(j + 1))) `2 by A1, A45, Th16;
then A49: b `2 <= p `2 by A1, A5, A7, Th17;
A50: b `1 <= p `1 by A1, A5, A7, A46, Th17;
A51: a `2 <= p `2 by A1, A5, A6, A48, Th17;

now :: thesis: contradiction

per cases ( ( a `1 <= b `1 & a `2 <= b `2 ) or ( a `1 <= b `1 & b `2 < a `2 ) or ( b `1 < a `1 & a `2 <= b `2 ) or ( b `1 < a `1 & b `2 < a `2 ) ) ;

suppose A52: ( a `1 <= b `1 & a `2 <= b `2 ) ; :: thesis: contradiction

then p `2 <= b `2 by A4, TOPREAL1:4;
then A53: b `2 = p `2 by A49, XXREAL_0:1;
p `1 <= b `1 by A4, A52, TOPREAL1:3;
then b `1 = p `1 by A50, XXREAL_0:1;
hence contradiction by A9, A53, TOPREAL3:6; :: thesis: verum

end;

suppose A54: ( a `1 <= b `1 & b `2 < a `2 ) ; :: thesis: contradiction

then p `2 <= a `2 by A4, TOPREAL1:4;
then A55: a `2 = p `2 by A51, XXREAL_0:1;
A56: p `1 <= b `1 by A4, A54, TOPREAL1:3;
then A57: b `1 = p `1 by A50, XXREAL_0:1;
then b `2 <> p `2 by A9, TOPREAL3:6;
then LSeg (a,b) is vertical by A4, A7, A50, A56, SPPOL_1:18, XXREAL_0:1;
then a `1 = b `1 by SPPOL_1:16;
hence contradiction by A8, A57, A55, TOPREAL3:6; :: thesis: verum

end;

suppose A58: ( b `1 < a `1 & a `2 <= b `2 ) ; :: thesis: contradiction

then p `2 <= b `2 by A4, TOPREAL1:4;
then A59: b `2 = p `2 by A49, XXREAL_0:1;
A60: p `1 <= a `1 by A4, A58, TOPREAL1:3;
then A61: a `1 = p `1 by A47, XXREAL_0:1;
then a `2 <> p `2 by A8, TOPREAL3:6;
then LSeg (a,b) is vertical by A4, A6, A47, A60, SPPOL_1:18, XXREAL_0:1;
then a `1 = b `1 by SPPOL_1:16;
hence contradiction by A9, A61, A59, TOPREAL3:6; :: thesis: verum

end;

suppose A62: ( b `1 < a `1 & b `2 < a `2 ) ; :: thesis: contradiction

then p `2 <= a `2 by A4, TOPREAL1:4;
then A63: a `2 = p `2 by A51, XXREAL_0:1;
p `1 <= a `1 by A4, A62, TOPREAL1:3;
then a `1 = p `1 by A47, XXREAL_0:1;
hence contradiction by A8, A63, TOPREAL3:6; :: thesis: verum

end;

end;

end;

hence contradiction ; :: thesis: verum

end;

suppose A64: p = G * ((i + 1),j) ; :: thesis: contradiction

then A65: p `2 = (G * (i,j)) `2 by A1, Th16;
then A66: p `2 <= b `2 by A1, A5, A7, Th17;
A67: a `1 <= p `1 by A1, A5, A6, A64, Th17;
A68: b `1 <= p `1 by A1, A5, A7, A64, Th17;
A69: p `2 <= a `2 by A1, A5, A6, A65, Th17;

now :: thesis: contradiction

per cases ( ( a `1 <= b `1 & a `2 <= b `2 ) or ( a `1 <= b `1 & b `2 < a `2 ) or ( b `1 < a `1 & a `2 <= b `2 ) or ( b `1 < a `1 & b `2 < a `2 ) ) ;

suppose A70: ( a `1 <= b `1 & a `2 <= b `2 ) ; :: thesis: contradiction

then a `2 <= p `2 by A4, TOPREAL1:4;
then A71: a `2 = p `2 by A69, XXREAL_0:1;
A72: p `1 <= b `1 by A4, A70, TOPREAL1:3;
then A73: b `1 = p `1 by A68, XXREAL_0:1;
then b `2 <> p `2 by A9, TOPREAL3:6;
then LSeg (a,b) is vertical by A4, A7, A68, A72, SPPOL_1:18, XXREAL_0:1;
then a `1 = b `1 by SPPOL_1:16;
hence contradiction by A8, A73, A71, TOPREAL3:6; :: thesis: verum

end;

suppose A74: ( a `1 <= b `1 & b `2 < a `2 ) ; :: thesis: contradiction

then b `2 <= p `2 by A4, TOPREAL1:4;
then A75: b `2 = p `2 by A66, XXREAL_0:1;
p `1 <= b `1 by A4, A74, TOPREAL1:3;
then b `1 = p `1 by A68, XXREAL_0:1;
hence contradiction by A9, A75, TOPREAL3:6; :: thesis: verum

end;

suppose A76: ( b `1 < a `1 & a `2 <= b `2 ) ; :: thesis: contradiction

then a `2 <= p `2 by A4, TOPREAL1:4;
then A77: a `2 = p `2 by A69, XXREAL_0:1;
p `1 <= a `1 by A4, A76, TOPREAL1:3;
then a `1 = p `1 by A67, XXREAL_0:1;
hence contradiction by A8, A77, TOPREAL3:6; :: thesis: verum

end;

suppose A78: ( b `1 < a `1 & b `2 < a `2 ) ; :: thesis: contradiction

then b `2 <= p `2 by A4, TOPREAL1:4;
then A79: b `2 = p `2 by A66, XXREAL_0:1;
A80: p `1 <= a `1 by A4, A78, TOPREAL1:3;
then A81: a `1 = p `1 by A67, XXREAL_0:1;
then a `2 <> p `2 by A8, TOPREAL3:6;
then LSeg (a,b) is vertical by A4, A6, A67, A80, SPPOL_1:18, XXREAL_0:1;
then a `1 = b `1 by SPPOL_1:16;
hence contradiction by A9, A81, A79, TOPREAL3:6; :: thesis: verum

end;

end;

end;

hence contradiction ; :: thesis: verum

end;

end;

end;

hence p is_extremal_in cell (G,i,j) by A3, SPPOL_1:def 1; :: thesis: verum