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

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;

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;

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;

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;

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;

end;