let f be rectangular FinSequence of (TOP-REAL 2); :: thesis: for p being Point of (TOP-REAL 2) st <*p*> is_in_the_area_of f & ( p `1 = W-bound (L~ f) or p `1 = E-bound (L~ f) or p `2 = S-bound (L~ f) or p `2 = N-bound (L~ f) ) holds

p in L~ f

let p be Point of (TOP-REAL 2); :: thesis: ( <*p*> is_in_the_area_of f & ( p `1 = W-bound (L~ f) or p `1 = E-bound (L~ f) or p `2 = S-bound (L~ f) or p `2 = N-bound (L~ f) ) implies p in L~ f )

A1: <*p*> /. 1 = p by FINSEQ_4:16;

dom <*p*> = {1} by FINSEQ_1:2, FINSEQ_1:38;

then A2: 1 in dom <*p*> by TARSKI:def 1;

assume A3: <*p*> is_in_the_area_of f ; :: thesis: ( ( not p `1 = W-bound (L~ f) & not p `1 = E-bound (L~ f) & not p `2 = S-bound (L~ f) & not p `2 = N-bound (L~ f) ) or p in L~ f )

then A4: W-bound (L~ f) <= p `1 by A2, A1;

A5: p `2 <= N-bound (L~ f) by A3, A2, A1;

A6: S-bound (L~ f) <= p `2 by A3, A2, A1;

A7: p `1 <= E-bound (L~ f) by A3, A2, A1;

consider D being non empty compact non horizontal non vertical Subset of (TOP-REAL 2) such that

A8: f = SpStSeq D by SPRECT_1:def 2;

A9: E-bound (L~ (SpStSeq D)) = E-bound D by SPRECT_1:61;

A10: N-bound (L~ (SpStSeq D)) = N-bound D by SPRECT_1:60;

A11: S-bound (L~ (SpStSeq D)) = S-bound D by SPRECT_1:59;

A12: W-bound (L~ (SpStSeq D)) = W-bound D by SPRECT_1:58;

A13: L~ f = ((LSeg ((NW-corner D),(NE-corner D))) \/ (LSeg ((NE-corner D),(SE-corner D)))) \/ ((LSeg ((SE-corner D),(SW-corner D))) \/ (LSeg ((SW-corner D),(NW-corner D)))) by A8, SPRECT_1:41;

assume A14: ( p `1 = W-bound (L~ f) or p `1 = E-bound (L~ f) or p `2 = S-bound (L~ f) or p `2 = N-bound (L~ f) ) ; :: thesis: p in L~ f

p in L~ f

let p be Point of (TOP-REAL 2); :: thesis: ( <*p*> is_in_the_area_of f & ( p `1 = W-bound (L~ f) or p `1 = E-bound (L~ f) or p `2 = S-bound (L~ f) or p `2 = N-bound (L~ f) ) implies p in L~ f )

A1: <*p*> /. 1 = p by FINSEQ_4:16;

dom <*p*> = {1} by FINSEQ_1:2, FINSEQ_1:38;

then A2: 1 in dom <*p*> by TARSKI:def 1;

assume A3: <*p*> is_in_the_area_of f ; :: thesis: ( ( not p `1 = W-bound (L~ f) & not p `1 = E-bound (L~ f) & not p `2 = S-bound (L~ f) & not p `2 = N-bound (L~ f) ) or p in L~ f )

then A4: W-bound (L~ f) <= p `1 by A2, A1;

A5: p `2 <= N-bound (L~ f) by A3, A2, A1;

A6: S-bound (L~ f) <= p `2 by A3, A2, A1;

A7: p `1 <= E-bound (L~ f) by A3, A2, A1;

consider D being non empty compact non horizontal non vertical Subset of (TOP-REAL 2) such that

A8: f = SpStSeq D by SPRECT_1:def 2;

A9: E-bound (L~ (SpStSeq D)) = E-bound D by SPRECT_1:61;

A10: N-bound (L~ (SpStSeq D)) = N-bound D by SPRECT_1:60;

A11: S-bound (L~ (SpStSeq D)) = S-bound D by SPRECT_1:59;

A12: W-bound (L~ (SpStSeq D)) = W-bound D by SPRECT_1:58;

A13: L~ f = ((LSeg ((NW-corner D),(NE-corner D))) \/ (LSeg ((NE-corner D),(SE-corner D)))) \/ ((LSeg ((SE-corner D),(SW-corner D))) \/ (LSeg ((SW-corner D),(NW-corner D)))) by A8, SPRECT_1:41;

assume A14: ( p `1 = W-bound (L~ f) or p `1 = E-bound (L~ f) or p `2 = S-bound (L~ f) or p `2 = N-bound (L~ f) ) ; :: thesis: p in L~ f

per cases
( p `1 = W-bound (L~ f) or p `1 = E-bound (L~ f) or p `2 = S-bound (L~ f) or p `2 = N-bound (L~ f) )
by A14;

end;

suppose A15:
p `1 = W-bound (L~ f)
; :: thesis: p in L~ f

A16:
(NW-corner D) `1 = W-bound D
by EUCLID:52;

A17: (NW-corner D) `2 = N-bound D by EUCLID:52;

A18: (SW-corner D) `2 = S-bound D by EUCLID:52;

(SW-corner D) `1 = W-bound D by EUCLID:52;

then p in LSeg ((SW-corner D),(NW-corner D)) by A6, A5, A8, A12, A11, A10, A15, A16, A18, A17, GOBOARD7:7;

then p in (LSeg ((SE-corner D),(SW-corner D))) \/ (LSeg ((SW-corner D),(NW-corner D))) by XBOOLE_0:def 3;

hence p in L~ f by A13, XBOOLE_0:def 3; :: thesis: verum

end;A17: (NW-corner D) `2 = N-bound D by EUCLID:52;

A18: (SW-corner D) `2 = S-bound D by EUCLID:52;

(SW-corner D) `1 = W-bound D by EUCLID:52;

then p in LSeg ((SW-corner D),(NW-corner D)) by A6, A5, A8, A12, A11, A10, A15, A16, A18, A17, GOBOARD7:7;

then p in (LSeg ((SE-corner D),(SW-corner D))) \/ (LSeg ((SW-corner D),(NW-corner D))) by XBOOLE_0:def 3;

hence p in L~ f by A13, XBOOLE_0:def 3; :: thesis: verum

suppose A19:
p `1 = E-bound (L~ f)
; :: thesis: p in L~ f

A20:
(SE-corner D) `1 = E-bound D
by EUCLID:52;

A21: (SE-corner D) `2 = S-bound D by EUCLID:52;

A22: (NE-corner D) `2 = N-bound D by EUCLID:52;

(NE-corner D) `1 = E-bound D by EUCLID:52;

then p in LSeg ((NE-corner D),(SE-corner D)) by A6, A5, A8, A11, A10, A9, A19, A20, A22, A21, GOBOARD7:7;

then p in (LSeg ((NW-corner D),(NE-corner D))) \/ (LSeg ((NE-corner D),(SE-corner D))) by XBOOLE_0:def 3;

hence p in L~ f by A13, XBOOLE_0:def 3; :: thesis: verum

end;A21: (SE-corner D) `2 = S-bound D by EUCLID:52;

A22: (NE-corner D) `2 = N-bound D by EUCLID:52;

(NE-corner D) `1 = E-bound D by EUCLID:52;

then p in LSeg ((NE-corner D),(SE-corner D)) by A6, A5, A8, A11, A10, A9, A19, A20, A22, A21, GOBOARD7:7;

then p in (LSeg ((NW-corner D),(NE-corner D))) \/ (LSeg ((NE-corner D),(SE-corner D))) by XBOOLE_0:def 3;

hence p in L~ f by A13, XBOOLE_0:def 3; :: thesis: verum

suppose A23:
p `2 = S-bound (L~ f)
; :: thesis: p in L~ f

A24:
(SW-corner D) `1 = W-bound D
by EUCLID:52;

A25: (SW-corner D) `2 = S-bound D by EUCLID:52;

A26: (SE-corner D) `2 = S-bound D by EUCLID:52;

(SE-corner D) `1 = E-bound D by EUCLID:52;

then p in LSeg ((SE-corner D),(SW-corner D)) by A4, A7, A8, A12, A11, A9, A23, A24, A26, A25, GOBOARD7:8;

then p in (LSeg ((SE-corner D),(SW-corner D))) \/ (LSeg ((SW-corner D),(NW-corner D))) by XBOOLE_0:def 3;

hence p in L~ f by A13, XBOOLE_0:def 3; :: thesis: verum

end;A25: (SW-corner D) `2 = S-bound D by EUCLID:52;

A26: (SE-corner D) `2 = S-bound D by EUCLID:52;

(SE-corner D) `1 = E-bound D by EUCLID:52;

then p in LSeg ((SE-corner D),(SW-corner D)) by A4, A7, A8, A12, A11, A9, A23, A24, A26, A25, GOBOARD7:8;

then p in (LSeg ((SE-corner D),(SW-corner D))) \/ (LSeg ((SW-corner D),(NW-corner D))) by XBOOLE_0:def 3;

hence p in L~ f by A13, XBOOLE_0:def 3; :: thesis: verum

suppose A27:
p `2 = N-bound (L~ f)
; :: thesis: p in L~ f

A28:
(NE-corner D) `1 = E-bound D
by EUCLID:52;

A29: (NE-corner D) `2 = N-bound D by EUCLID:52;

A30: (NW-corner D) `2 = N-bound D by EUCLID:52;

(NW-corner D) `1 = W-bound D by EUCLID:52;

then p in LSeg ((NW-corner D),(NE-corner D)) by A4, A7, A8, A12, A10, A9, A27, A28, A30, A29, GOBOARD7:8;

then p in (LSeg ((NW-corner D),(NE-corner D))) \/ (LSeg ((NE-corner D),(SE-corner D))) by XBOOLE_0:def 3;

hence p in L~ f by A13, XBOOLE_0:def 3; :: thesis: verum

end;A29: (NE-corner D) `2 = N-bound D by EUCLID:52;

A30: (NW-corner D) `2 = N-bound D by EUCLID:52;

(NW-corner D) `1 = W-bound D by EUCLID:52;

then p in LSeg ((NW-corner D),(NE-corner D)) by A4, A7, A8, A12, A10, A9, A27, A28, A30, A29, GOBOARD7:8;

then p in (LSeg ((NW-corner D),(NE-corner D))) \/ (LSeg ((NE-corner D),(SE-corner D))) by XBOOLE_0:def 3;

hence p in L~ f by A13, XBOOLE_0:def 3; :: thesis: verum