for G being Go-board
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 by Th2;