let i1, j1 be Nat; for G being Go-board st 1 <= i1 & i1 <= len G & 1 <= j1 & j1 + 1 <= width G holds
for i2, j2 being Nat holds
( not 1 <= i2 or not i2 + 1 <= len G or not 1 <= j2 or not j2 <= width G or not (1 / 2) * ((G * (i1,j1)) + (G * (i1,(j1 + 1)))) in LSeg ((G * (i2,j2)),(G * ((i2 + 1),j2))) )
let G be Go-board; ( 1 <= i1 & i1 <= len G & 1 <= j1 & j1 + 1 <= width G implies for i2, j2 being Nat holds
( not 1 <= i2 or not i2 + 1 <= len G or not 1 <= j2 or not j2 <= width G or not (1 / 2) * ((G * (i1,j1)) + (G * (i1,(j1 + 1)))) in LSeg ((G * (i2,j2)),(G * ((i2 + 1),j2))) ) )
assume that
A1:
( 1 <= i1 & i1 <= len G )
and
A2:
( 1 <= j1 & j1 + 1 <= width G )
; for i2, j2 being Nat holds
( not 1 <= i2 or not i2 + 1 <= len G or not 1 <= j2 or not j2 <= width G or not (1 / 2) * ((G * (i1,j1)) + (G * (i1,(j1 + 1)))) in LSeg ((G * (i2,j2)),(G * ((i2 + 1),j2))) )
A3:
j1 < j1 + 1
by XREAL_1:29;
set mi = (1 / 2) * ((G * (i1,j1)) + (G * (i1,(j1 + 1))));
given i2, j2 being Nat such that A4:
( 1 <= i2 & i2 + 1 <= len G )
and
A5:
( 1 <= j2 & j2 <= width G )
and
A6:
(1 / 2) * ((G * (i1,j1)) + (G * (i1,(j1 + 1)))) in LSeg ((G * (i2,j2)),(G * ((i2 + 1),j2)))
; contradiction
A7:
((1 / 2) * (G * (i1,j1))) + ((1 / 2) * (G * (i1,(j1 + 1)))) = (1 / 2) * ((G * (i1,j1)) + (G * (i1,(j1 + 1))))
by RLVECT_1:def 5;
then A8:
(1 / 2) * ((G * (i1,j1)) + (G * (i1,(j1 + 1)))) in LSeg ((G * (i1,j1)),(G * (i1,(j1 + 1))))
by Lm1;
then A9:
LSeg ((G * (i1,j1)),(G * (i1,(j1 + 1)))) meets LSeg ((G * (i2,j2)),(G * ((i2 + 1),j2)))
by A6, XBOOLE_0:3;
per cases
( ( i1 = i2 & j1 = j2 ) or ( i1 = i2 & j1 + 1 = j2 ) or ( i1 = i2 + 1 & j1 = j2 ) or ( i1 = i2 + 1 & j1 + 1 = j2 ) )
by A1, A2, A4, A5, A9, Th21;
suppose A10:
(
i1 = i2 &
j1 = j2 )
;
contradictionthen
(LSeg ((G * (i1,j1)),(G * (i1,(j1 + 1))))) /\ (LSeg ((G * ((i1 + 1),j1)),(G * (i1,j1)))) = {(G * (i1,j1))}
by A2, A4, Th17;
then
(1 / 2) * ((G * (i1,j1)) + (G * (i1,(j1 + 1)))) in {(G * (i1,j1))}
by A6, A8, A10, XBOOLE_0:def 4;
then ((1 / 2) * (G * (i1,j1))) + ((1 / 2) * (G * (i1,(j1 + 1)))) =
G * (
i1,
j1)
by A7, TARSKI:def 1
.=
((1 / 2) + (1 / 2)) * (G * (i1,j1))
by RLVECT_1:def 8
.=
((1 / 2) * (G * (i1,j1))) + ((1 / 2) * (G * (i1,j1)))
by RLVECT_1:def 6
;
then A11:
(1 / 2) * (G * (i1,(j1 + 1))) = (1 / 2) * (G * (i1,j1))
by Th3;
(G * (i1,(j1 + 1))) `2 > (G * (i1,j1)) `2
by A1, A2, A3, GOBOARD5:4;
hence
contradiction
by A11, RLVECT_1:36;
verum end; suppose A12:
(
i1 = i2 &
j1 + 1
= j2 )
;
contradictionthen
(LSeg ((G * (i1,j1)),(G * (i1,(j1 + 1))))) /\ (LSeg ((G * ((i1 + 1),(j1 + 1))),(G * (i1,(j1 + 1))))) = {(G * (i1,(j1 + 1)))}
by A2, A4, Th15;
then
(1 / 2) * ((G * (i1,j1)) + (G * (i1,(j1 + 1)))) in {(G * (i1,(j1 + 1)))}
by A6, A8, A12, XBOOLE_0:def 4;
then ((1 / 2) * (G * (i1,j1))) + ((1 / 2) * (G * (i1,(j1 + 1)))) =
G * (
i1,
(j1 + 1))
by A7, TARSKI:def 1
.=
((1 / 2) + (1 / 2)) * (G * (i1,(j1 + 1)))
by RLVECT_1:def 8
.=
((1 / 2) * (G * (i1,(j1 + 1)))) + ((1 / 2) * (G * (i1,(j1 + 1))))
by RLVECT_1:def 6
;
then A13:
(1 / 2) * (G * (i1,(j1 + 1))) = (1 / 2) * (G * (i1,j1))
by Th3;
(G * (i1,(j1 + 1))) `2 > (G * (i1,j1)) `2
by A1, A2, A3, GOBOARD5:4;
hence
contradiction
by A13, RLVECT_1:36;
verum end; suppose A14:
(
i1 = i2 + 1 &
j1 = j2 )
;
contradictionthen
(LSeg ((G * (i1,j1)),(G * (i1,(j1 + 1))))) /\ (LSeg ((G * (i1,j1)),(G * (i2,j1)))) = {(G * (i1,j1))}
by A2, A4, Th18;
then
(1 / 2) * ((G * (i1,j1)) + (G * (i1,(j1 + 1)))) in {(G * (i1,j1))}
by A6, A8, A14, XBOOLE_0:def 4;
then ((1 / 2) * (G * (i1,j1))) + ((1 / 2) * (G * (i1,(j1 + 1)))) =
G * (
i1,
j1)
by A7, TARSKI:def 1
.=
((1 / 2) + (1 / 2)) * (G * (i1,j1))
by RLVECT_1:def 8
.=
((1 / 2) * (G * (i1,j1))) + ((1 / 2) * (G * (i1,j1)))
by RLVECT_1:def 6
;
then A15:
(1 / 2) * (G * (i1,(j1 + 1))) = (1 / 2) * (G * (i1,j1))
by Th3;
(G * (i1,(j1 + 1))) `2 > (G * (i1,j1)) `2
by A1, A2, A3, GOBOARD5:4;
hence
contradiction
by A15, RLVECT_1:36;
verum end; suppose A16:
(
i1 = i2 + 1 &
j1 + 1
= j2 )
;
contradictionthen
(LSeg ((G * (i1,j1)),(G * (i1,(j1 + 1))))) /\ (LSeg ((G * (i1,(j1 + 1))),(G * (i2,(j1 + 1))))) = {(G * (i1,(j1 + 1)))}
by A2, A4, Th16;
then
(1 / 2) * ((G * (i1,j1)) + (G * (i1,(j1 + 1)))) in {(G * (i1,(j1 + 1)))}
by A6, A8, A16, XBOOLE_0:def 4;
then ((1 / 2) * (G * (i1,j1))) + ((1 / 2) * (G * (i1,(j1 + 1)))) =
G * (
i1,
(j1 + 1))
by A7, TARSKI:def 1
.=
((1 / 2) + (1 / 2)) * (G * (i1,(j1 + 1)))
by RLVECT_1:def 8
.=
((1 / 2) * (G * (i1,(j1 + 1)))) + ((1 / 2) * (G * (i1,(j1 + 1))))
by RLVECT_1:def 6
;
then A17:
(1 / 2) * (G * (i1,(j1 + 1))) = (1 / 2) * (G * (i1,j1))
by Th3;
(G * (i1,(j1 + 1))) `2 > (G * (i1,j1)) `2
by A1, A2, A3, GOBOARD5:4;
hence
contradiction
by A17, RLVECT_1:36;
verum end; end;