let f be FinSequence of (TOP-REAL 2); :: thesis: 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); :: thesis: ( 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) ; :: according to SPRECT_2:def 1,SPRECT_2:def 2,SPRECT_2:def 3 :: thesis: 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; :: thesis: verum