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)

proof

let n be Nat; :: according to GOBOARD4:def 2 :: thesis: ( not n in dom (X_axis h) or ( (X_axis g) . 1 <= (X_axis h) . n & (X_axis h) . n <= (X_axis g) . (len g) ) )
set F = X_axis g;
set r = (X_axis g) . 1;
set s = (X_axis g) . (len g);
set H = X_axis h;
assume n in dom (X_axis h) ; :: thesis: ( (X_axis g) . 1 <= (X_axis h) . n & (X_axis h) . n <= (X_axis g) . (len g) )
then A9: ( n in dom h & (X_axis h) . n = (h /. n) `1 ) by Th15, GOBOARD1:def 1;
1 in dom (X_axis g) by FINSEQ_5:6;
then (X_axis g) . 1 = W-bound (L~ f) by A3, GOBOARD1:def 1;
hence (X_axis g) . 1 <= (X_axis h) . n by A5, A9; :: thesis: (X_axis h) . n <= (X_axis g) . (len g)
( len (X_axis g) = len g & len (X_axis g) in dom (X_axis g) ) by FINSEQ_5:6, GOBOARD1:def 1;
then (X_axis g) . (len g) = E-bound (L~ f) by A4, GOBOARD1:def 1;
hence (X_axis h) . n <= (X_axis g) . (len g) by A5, A9; :: thesis: verum

end;

A10: Y_axis h lies_between (Y_axis h) . 1,(Y_axis h) . (len h)

proof

let n be Nat; :: according to GOBOARD4:def 2 :: thesis: ( not n in dom (Y_axis h) or ( (Y_axis h) . 1 <= (Y_axis h) . n & (Y_axis h) . n <= (Y_axis h) . (len h) ) )
set F = Y_axis h;
set r = (Y_axis h) . 1;
set s = (Y_axis h) . (len h);
assume n in dom (Y_axis h) ; :: thesis: ( (Y_axis h) . 1 <= (Y_axis h) . n & (Y_axis h) . n <= (Y_axis h) . (len h) )
then A11: ( n in dom h & (Y_axis h) . n = (h /. n) `2 ) by Th16, GOBOARD1:def 2;
1 in dom (Y_axis h) by FINSEQ_5:6;
then (Y_axis h) . 1 = S-bound (L~ f) by A6, GOBOARD1:def 2;
hence (Y_axis h) . 1 <= (Y_axis h) . n by A5, A11; :: thesis: (Y_axis h) . n <= (Y_axis h) . (len h)
( len (Y_axis h) = len h & len (Y_axis h) in dom (Y_axis h) ) by FINSEQ_5:6, GOBOARD1:def 2;
then (Y_axis h) . (len h) = N-bound (L~ f) by A7, GOBOARD1:def 2;
hence (Y_axis h) . n <= (Y_axis h) . (len h) by A5, A11; :: thesis: verum

end;

A12: Y_axis g lies_between (Y_axis h) . 1,(Y_axis h) . (len h)

proof

let n be Nat; :: according to GOBOARD4:def 2 :: thesis: ( not n in dom (Y_axis g) or ( (Y_axis h) . 1 <= (Y_axis g) . n & (Y_axis g) . n <= (Y_axis h) . (len h) ) )
set F = Y_axis h;
set r = (Y_axis h) . 1;
set s = (Y_axis h) . (len h);
set G = Y_axis g;
assume n in dom (Y_axis g) ; :: thesis: ( (Y_axis h) . 1 <= (Y_axis g) . n & (Y_axis g) . n <= (Y_axis h) . (len h) )
then A13: ( n in dom g & (Y_axis g) . n = (g /. n) `2 ) by Th16, GOBOARD1:def 2;
1 in dom (Y_axis h) by FINSEQ_5:6;
then (Y_axis h) . 1 = S-bound (L~ f) by A6, GOBOARD1:def 2;
hence (Y_axis h) . 1 <= (Y_axis g) . n by A2, A13; :: thesis: (Y_axis g) . n <= (Y_axis h) . (len h)
( len (Y_axis h) = len h & len (Y_axis h) in dom (Y_axis h) ) by FINSEQ_5:6, GOBOARD1:def 2;
then (Y_axis h) . (len h) = N-bound (L~ f) by A7, GOBOARD1:def 2;
hence (Y_axis g) . n <= (Y_axis h) . (len h) by A2, A13; :: thesis: verum

end;

X_axis g lies_between (X_axis g) . 1,(X_axis g) . (len g)

proof

let n be Nat; :: according to GOBOARD4:def 2 :: thesis: ( not n in dom (X_axis g) or ( (X_axis g) . 1 <= (X_axis g) . n & (X_axis g) . n <= (X_axis g) . (len g) ) )
set F = X_axis g;
set r = (X_axis g) . 1;
set s = (X_axis g) . (len g);
assume n in dom (X_axis g) ; :: thesis: ( (X_axis g) . 1 <= (X_axis g) . n & (X_axis g) . n <= (X_axis g) . (len g) )
then A14: ( n in dom g & (X_axis g) . n = (g /. n) `1 ) by Th15, GOBOARD1:def 1;
1 in dom (X_axis g) by FINSEQ_5:6;
then (X_axis g) . 1 = W-bound (L~ f) by A3, GOBOARD1:def 1;
hence (X_axis g) . 1 <= (X_axis g) . n by A2, A14; :: thesis: (X_axis g) . n <= (X_axis g) . (len g)
( len (X_axis g) = len g & len (X_axis g) in dom (X_axis g) ) by FINSEQ_5:6, GOBOARD1:def 1;
then (X_axis g) . (len g) = E-bound (L~ f) by A4, GOBOARD1:def 1;
hence (X_axis g) . n <= (X_axis g) . (len g) by A2, A14; :: thesis: verum

end;

hence L~ g meets L~ h by A1, A8, A12, A10, GOBOARD4:5; :: thesis: verum