:: Go-Board Theorem
:: by Jaros{\l}aw Kotowicz and Yatsuka Nakamura
::
:: Received August 24, 1992
:: Copyright (c) 1992-2012 Association of Mizar Users


begin

theorem Th1: :: GOBOARD4:1
for G being Go-board
for f1, f2 being FinSequence of (TOP-REAL 2) st 1 <= len f1 &amp; 1 <= len f2 &amp; f1 is_sequence_on G &amp; f2 is_sequence_on G &amp; f1 /. 1 in rng (Line (G,1)) &amp; f1 /. (len f1) in rng (Line (G,(len G))) &amp; f2 /. 1 in rng (Col (G,1)) &amp; f2 /. (len f2) in rng (Col (G,(width G))) holds
rng f1 meets rng f2
proofend;

theorem Th2: :: GOBOARD4:2
for G being Go-board
for f1, f2 being FinSequence of (TOP-REAL 2) st 2 <= len f1 &amp; 2 <= len f2 &amp; f1 is_sequence_on G &amp; f2 is_sequence_on G &amp; f1 /. 1 in rng (Line (G,1)) &amp; f1 /. (len f1) in rng (Line (G,(len G))) &amp; f2 /. 1 in rng (Col (G,1)) &amp; f2 /. (len f2) in rng (Col (G,(width G))) holds
L~ f1 meets L~ f2
proofend;

theorem :: GOBOARD4:3
for G being Go-board
for f1, f2 being FinSequence of (TOP-REAL 2) st 2 <= len f1 &amp; 2 <= len f2 &amp; f1 is_sequence_on G &amp; f2 is_sequence_on G &amp; f1 /. 1 in rng (Line (G,1)) &amp; f1 /. (len f1) in rng (Line (G,(len G))) &amp; f2 /. 1 in rng (Col (G,1)) &amp; f2 /. (len f2) in rng (Col (G,(width G))) holds
L~ f1 meets L~ f2 by Th2;

definition
let f be Relation;
let r, s be Real;
predf lies_between r,s means :Def1: :: GOBOARD4:def 1
 rng f c= [.r,s.];
end;

:: deftheorem Def1 defines lies_between GOBOARD4:def_1_:_
 for f being Relation
for r, s being Real holds
( f lies_between r,s iff rng f c= [.r,s.] );

definition
let f be FinSequence of REAL ;
let r, s be Real;
redefine pred f lies_between r,s means :Def2: :: GOBOARD4:def 2
 for n being Element of NAT st n in dom f holds
( r <= f . n &amp; f . n <= s );
compatibility
 ( f lies_between r,s iff for n being Element of NAT st n in dom f holds
( r <= f . n &amp; f . n <= s ) )
proofend;
end;

:: deftheorem Def2 defines lies_between GOBOARD4:def_2_:_
 for f being FinSequence of REAL
for r, s being Real holds
( f lies_between r,s iff for n being Element of NAT st n in dom f holds
( r <= f . n &amp; f . n <= s ) );

theorem Th4: :: GOBOARD4:4
for f1, f2 being FinSequence of (TOP-REAL 2) st 2 <= len f1 &amp; 2 <= len f2 &amp; f1 is special &amp; f2 is special &amp; ( for n being Element of NAT st n in dom f1 &amp; n + 1 in dom f1 holds
f1 /. n <> f1 /. (n + 1) ) &amp; ( for n being Element of NAT st n in dom f2 &amp; n + 1 in dom f2 holds
f2 /. n <> f2 /. (n + 1) ) &amp; X_axis f1 lies_between (X_axis f1) . 1,(X_axis f1) . (len f1) &amp; X_axis f2 lies_between (X_axis f1) . 1,(X_axis f1) . (len f1) &amp; Y_axis f1 lies_between (Y_axis f2) . 1,(Y_axis f2) . (len f2) &amp; Y_axis f2 lies_between (Y_axis f2) . 1,(Y_axis f2) . (len f2) holds
L~ f1 meets L~ f2
proofend;

theorem Th5: :: GOBOARD4:5
for f1, f2 being FinSequence of (TOP-REAL 2) st f1 is one-to-one &amp; f1 is special &amp; 2 <= len f1 &amp; f2 is one-to-one &amp; f2 is special &amp; 2 <= len f2 &amp; X_axis f1 lies_between (X_axis f1) . 1,(X_axis f1) . (len f1) &amp; X_axis f2 lies_between (X_axis f1) . 1,(X_axis f1) . (len f1) &amp; Y_axis f1 lies_between (Y_axis f2) . 1,(Y_axis f2) . (len f2) &amp; Y_axis f2 lies_between (Y_axis f2) . 1,(Y_axis f2) . (len f2) holds
L~ f1 meets L~ f2
proofend;

theorem :: GOBOARD4:6
for P1, P2 being Subset of (TOP-REAL 2)
for p1, p2, q1, q2 being Point of (TOP-REAL 2) st P1 is_S-P_arc_joining p1,q1 &amp; P2 is_S-P_arc_joining p2,q2 &amp; ( for p being Point of (TOP-REAL 2) st p in P1 \/ P2 holds
( p1 `1 <= p `1 &amp; p `1 <= q1 `1 ) ) &amp; ( for p being Point of (TOP-REAL 2) st p in P1 \/ P2 holds
( p2 `2 <= p `2 &amp; p `2 <= q2 `2 ) ) holds
P1 meets P2
proofend;