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 Element of 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 Element of 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 one-to-one non empty special FinSequence of (TOP-REAL 2) by A1, CARD_1:47;
A8: X_axis g lies_between (X_axis g) . 1,(X_axis g) . (len g)

proof

set F = X_axis g;
set r = (X_axis g) . 1;
set s = (X_axis g) . (len g);
let n be Element of 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) ) )
assume A9: 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 A10: n in dom g by Th19;
A11: (X_axis g) . n = (g /. n) `1 by A9, GOBOARD1:def 3;
1 in dom (X_axis g) by FINSEQ_5:6;
then (X_axis g) . 1 = W-bound (L~ f) by A3, GOBOARD1:def 3;
hence (X_axis g) . 1 <= (X_axis g) . n by A2, A10, A11; :: thesis: (X_axis g) . n <= (X_axis g) . (len g)
A12: len (X_axis g) = len g by GOBOARD1:def 3;
len (X_axis g) in dom (X_axis g) by FINSEQ_5:6;
then (X_axis g) . (len g) = E-bound (L~ f) by A4, A12, GOBOARD1:def 3;
hence (X_axis g) . n <= (X_axis g) . (len g) by A2, A10, A11; :: thesis: verum

end;

A13: X_axis h lies_between (X_axis g) . 1,(X_axis g) . (len g)

proof

set F = X_axis g;
set r = (X_axis g) . 1;
set s = (X_axis g) . (len g);
set H = X_axis h;
let n be Element of 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) ) )
assume A14: 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 A15: n in dom h by Th19;
A16: (X_axis h) . n = (h /. n) `1 by A14, GOBOARD1:def 3;
1 in dom (X_axis g) by FINSEQ_5:6;
then (X_axis g) . 1 = W-bound (L~ f) by A3, GOBOARD1:def 3;
hence (X_axis g) . 1 <= (X_axis h) . n by A5, A15, A16; :: thesis: (X_axis h) . n <= (X_axis g) . (len g)
A17: len (X_axis g) = len g by GOBOARD1:def 3;
len (X_axis g) in dom (X_axis g) by FINSEQ_5:6;
then (X_axis g) . (len g) = E-bound (L~ f) by A4, A17, GOBOARD1:def 3;
hence (X_axis h) . n <= (X_axis g) . (len g) by A5, A15, A16; :: thesis: verum

end;

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

proof

set F = Y_axis h;
set r = (Y_axis h) . 1;
set s = (Y_axis h) . (len h);
set G = Y_axis g;
let n be Element of 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) ) )
assume A19: 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 A20: n in dom g by Th20;
A21: (Y_axis g) . n = (g /. n) `2 by A19, GOBOARD1:def 4;
1 in dom (Y_axis h) by FINSEQ_5:6;
then (Y_axis h) . 1 = S-bound (L~ f) by A6, GOBOARD1:def 4;
hence (Y_axis h) . 1 <= (Y_axis g) . n by A2, A20, A21; :: thesis: (Y_axis g) . n <= (Y_axis h) . (len h)
A22: len (Y_axis h) = len h by GOBOARD1:def 4;
len (Y_axis h) in dom (Y_axis h) by FINSEQ_5:6;
then (Y_axis h) . (len h) = N-bound (L~ f) by A7, A22, GOBOARD1:def 4;
hence (Y_axis g) . n <= (Y_axis h) . (len h) by A2, A20, A21; :: thesis: verum

end;

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

proof

set F = Y_axis h;
set r = (Y_axis h) . 1;
set s = (Y_axis h) . (len h);
let n be Element of 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) ) )
assume A23: 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 A24: n in dom h by Th20;
A25: (Y_axis h) . n = (h /. n) `2 by A23, GOBOARD1:def 4;
1 in dom (Y_axis h) by FINSEQ_5:6;
then (Y_axis h) . 1 = S-bound (L~ f) by A6, GOBOARD1:def 4;
hence (Y_axis h) . 1 <= (Y_axis h) . n by A5, A24, A25; :: thesis: (Y_axis h) . n <= (Y_axis h) . (len h)
A26: len (Y_axis h) = len h by GOBOARD1:def 4;
len (Y_axis h) in dom (Y_axis h) by FINSEQ_5:6;
then (Y_axis h) . (len h) = N-bound (L~ f) by A7, A26, GOBOARD1:def 4;
hence (Y_axis h) . n <= (Y_axis h) . (len h) by A5, A24, A25; :: thesis: verum

end;

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