let G be Go-board; :: thesis: for f1, f2 being FinSequence of (TOP-REAL 2) st 2 <= len f1 & 2 <= len f2 & f1 is_sequence_on G & f2 is_sequence_on G & f1 /. 1 in rng (Line G,1) & f1 /. (len f1) in rng (Line G,(len G)) & f2 /. 1 in rng (Col G,1) & f2 /. (len f2) in rng (Col G,(width G)) holds
L~ f1 meets L~ f2
let f1, f2 be FinSequence of (TOP-REAL 2); :: thesis: ( 2 <= len f1 & 2 <= len f2 & f1 is_sequence_on G & f2 is_sequence_on G & f1 /. 1 in rng (Line G,1) & f1 /. (len f1) in rng (Line G,(len G)) & f2 /. 1 in rng (Col G,1) & f2 /. (len f2) in rng (Col G,(width G)) implies L~ f1 meets L~ f2 )
assume A1: ( 2 <= len f1 & 2 <= len f2 & f1 is_sequence_on G & f2 is_sequence_on G & f1 /. 1 in rng (Line G,1) & f1 /. (len f1) in rng (Line G,(len G)) & f2 /. 1 in rng (Col G,1) & f2 /. (len f2) in rng (Col G,(width G)) ) ; :: thesis: L~ f1 meets L~ f2
then ( 1 <= len f1 & 1 <= len f2 ) by XXREAL_0:2;
then rng f1 meets rng f2 by A1, Th1;
then consider x being set such that
A2: ( x in rng f1 & x in rng f2 ) by XBOOLE_0:3;
A3: ex n being Element of NAT st
( n in dom f1 & f1 /. n = x ) by A2, PARTFUN2:4;
ex m being Element of NAT st
( m in dom f2 & f2 /. m = x ) by A2, PARTFUN2:4;
then ( x in L~ f1 & x in L~ f2 ) by A1, A3, GOBOARD1:16;
hence L~ f1 meets L~ f2 by XBOOLE_0:3; :: thesis: verum