let f be rectangular FinSequence of (); :: thesis: for p being Point of () holds
( not p in L~ f or 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) )

let p be Point of (); :: thesis: ( not p in L~ f or 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) )
assume A1: p in L~ f ; :: thesis: ( 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) )
consider D being non empty compact non horizontal non vertical Subset of () such that
A2: f = SpStSeq D by SPRECT_1:def 2;
L~ f = ((LSeg ((),())) \/ (LSeg ((),()))) \/ ((LSeg ((),())) \/ (LSeg ((),()))) by ;
then A3: ( p in (LSeg ((),())) \/ (LSeg ((),())) or p in (LSeg ((),())) \/ (LSeg ((),())) ) by ;
per cases ( p in LSeg ((),()) or p in LSeg ((),()) or p in LSeg ((),()) or p in LSeg ((),()) ) by ;
suppose A4: p in LSeg ((),()) ; :: thesis: ( 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) )
A5: N-bound (L~ ()) = N-bound D by SPRECT_1:60;
then A6: (NE-corner D) `2 = N-bound (L~ f) by ;
(NW-corner D) `2 = N-bound (L~ f) by ;
hence ( 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 ; :: thesis: verum
end;
suppose A7: p in LSeg ((),()) ; :: thesis: ( 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) )
A8: E-bound (L~ ()) = E-bound D by SPRECT_1:61;
then A9: (SE-corner D) `1 = E-bound (L~ f) by ;
(NE-corner D) `1 = E-bound (L~ f) by ;
hence ( 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 ; :: thesis: verum
end;
suppose A10: p in LSeg ((),()) ; :: thesis: ( 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) )
A11: S-bound (L~ ()) = S-bound D by SPRECT_1:59;
then A12: (SW-corner D) `2 = S-bound (L~ f) by ;
(SE-corner D) `2 = S-bound (L~ f) by ;
hence ( 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 ; :: thesis: verum
end;
suppose A13: p in LSeg ((),()) ; :: thesis: ( 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) )
A14: W-bound (L~ ()) = W-bound D by SPRECT_1:58;
then A15: (NW-corner D) `1 = W-bound (L~ f) by ;
(SW-corner D) `1 = W-bound (L~ f) by ;
hence ( 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 ; :: thesis: verum
end;
end;