for f1, f2 being FinSequence of (TOP-REAL 2) st 2 <= len f1 & 2 <= len f2 & f1 is special & f2 is special & ( for n being Nat st n in dom f1 & n + 1 in dom f1 holds
f1 /. n <> f1 /. (n + 1) ) & ( for n being Nat st n in dom f2 & n + 1 in dom f2 holds
f2 /. n <> f2 /. (n + 1) ) & X_axis f1 lies_between (X_axis f1) . 1,(X_axis f1) . (len f1) & X_axis f2 lies_between (X_axis f1) . 1,(X_axis f1) . (len f1) & Y_axis f1 lies_between (Y_axis f2) . 1,(Y_axis f2) . (len f2) & Y_axis f2 lies_between (Y_axis f2) . 1,(Y_axis f2) . (len f2) holds
L~ f1 meets L~ f2