let f be FinSequence of (TOP-REAL 2); for g, h being one-to-one special FinSequence of (TOP-REAL 2) st 2 <= len g & 2 <= len h & g is_a_h.c._for f & h is_a_v.c._for f holds
L~ g meets L~ h
let g, h be one-to-one special FinSequence of (TOP-REAL 2); ( 2 <= len g & 2 <= len h & g is_a_h.c._for f & h is_a_v.c._for f implies L~ g meets L~ h )
assume that
A1:
( 2 <= len g & 2 <= len h )
and
A2:
for n being Nat st n in dom g holds
( W-bound (L~ f) <= (g /. n) `1 & (g /. n) `1 <= E-bound (L~ f) & S-bound (L~ f) <= (g /. n) `2 & (g /. n) `2 <= N-bound (L~ f) )
and
A3:
(g /. 1) `1 = W-bound (L~ f)
and
A4:
(g /. (len g)) `1 = E-bound (L~ f)
and
A5:
for n being Nat st n in dom h holds
( W-bound (L~ f) <= (h /. n) `1 & (h /. n) `1 <= E-bound (L~ f) & S-bound (L~ f) <= (h /. n) `2 & (h /. n) `2 <= N-bound (L~ f) )
and
A6:
(h /. 1) `2 = S-bound (L~ f)
and
A7:
(h /. (len h)) `2 = N-bound (L~ f)
; SPRECT_2:def 1,SPRECT_2:def 2,SPRECT_2:def 3 L~ g meets L~ h
reconsider g = g, h = h as non empty one-to-one special FinSequence of (TOP-REAL 2) by A1, CARD_1:27;
A8:
X_axis h lies_between (X_axis g) . 1,(X_axis g) . (len g)
A10:
Y_axis h lies_between (Y_axis h) . 1,(Y_axis h) . (len h)
A12:
Y_axis g lies_between (Y_axis h) . 1,(Y_axis h) . (len h)
X_axis g lies_between (X_axis g) . 1,(X_axis g) . (len g)
hence
L~ g meets L~ h
by A1, A8, A12, A10, GOBOARD4:5; verum