let f be rectangular FinSequence of (); :: thesis: for p being Point of () 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 (); :: 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 ;
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 () such that
A8: f = SpStSeq D by SPRECT_1:def 2;
A9: E-bound (L~ ()) = E-bound D by SPRECT_1:61;
A10: N-bound (L~ ()) = N-bound D by SPRECT_1:60;
A11: S-bound (L~ ()) = S-bound D by SPRECT_1:59;
A12: W-bound (L~ ()) = W-bound D by SPRECT_1:58;
A13: L~ f = ((LSeg ((),())) \/ (LSeg ((),()))) \/ ((LSeg ((),())) \/ (LSeg ((),()))) by ;
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
end;
suppose A19: p `1 = E-bound (L~ f) ; :: thesis: p in L~ f
end;
suppose A23: p `2 = S-bound (L~ f) ; :: thesis: p in L~ f
end;
suppose A27: p `2 = N-bound (L~ f) ; :: thesis: p in L~ f
end;
end;