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:25;
dom <*p*> = {1} by FINSEQ_1:4, FINSEQ_1:55;
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, SPRECT_2:def 1;
A5: p `2 <= N-bound (L~ f) by A3, A2, A1, SPRECT_2:def 1;
A6: S-bound (L~ f) <= p `2 by A3, A2, A1, SPRECT_2:def 1;
A7: p `1 <= E-bound (L~ f) by A3, A2, A1, SPRECT_2:def 1;
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:69;
A10: N-bound (L~ (SpStSeq D)) = N-bound D by SPRECT_1:68;
A11: S-bound (L~ (SpStSeq D)) = S-bound D by SPRECT_1:67;
A12: W-bound (L~ (SpStSeq D)) = W-bound D by SPRECT_1:66;
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:43;
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:56;
A17: (NW-corner D) `2 = N-bound D by EUCLID:56;
A18: (SW-corner D) `2 = S-bound D by EUCLID:56;
(SW-corner D) `1 = W-bound D by EUCLID:56;
then p in LSeg (SW-corner D),(NW-corner D) by A6, A5, A8, A12, A11, A10, A15, A16, A18, A17, 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 A19: p `1 = E-bound (L~ f) ; :: thesis: p in L~ f

A20: (SE-corner D) `1 = E-bound D by EUCLID:56;
A21: (SE-corner D) `2 = S-bound D by EUCLID:56;
A22: (NE-corner D) `2 = N-bound D by EUCLID:56;
(NE-corner D) `1 = E-bound D by EUCLID:56;
then p in LSeg (NE-corner D),(SE-corner D) by A6, A5, A8, A11, A10, A9, A19, A20, A22, A21, 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;

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

A24: (SW-corner D) `1 = W-bound D by EUCLID:56;
A25: (SW-corner D) `2 = S-bound D by EUCLID:56;
A26: (SE-corner D) `2 = S-bound D by EUCLID:56;
(SE-corner D) `1 = E-bound D by EUCLID:56;
then p in LSeg (SE-corner D),(SW-corner D) by A4, A7, A8, A12, A11, A9, A23, A24, A26, A25, GOBOARD7:9;
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:56;
A29: (NE-corner D) `2 = N-bound D by EUCLID:56;
A30: (NW-corner D) `2 = N-bound D by EUCLID:56;
(NW-corner D) `1 = W-bound D by EUCLID:56;
then p in LSeg (NW-corner D),(NE-corner D) by A4, A7, A8, A12, A10, A9, A27, A28, A30, A29, GOBOARD7:9;
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;