let f be rectangular FinSequence of (TOP-REAL 2); :: thesis: for p being Point of (TOP-REAL 2) 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 (TOP-REAL 2); :: 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 (TOP-REAL 2) such that
A2: f = SpStSeq D by SPRECT_1:def 2;
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 A2, SPRECT_1:43;
then A3: ( p in (LSeg (NW-corner D),(NE-corner D)) \/ (LSeg (NE-corner D),(SE-corner D)) or p in (LSeg (SE-corner D),(SW-corner D)) \/ (LSeg (SW-corner D),(NW-corner D)) ) by A1, XBOOLE_0:def 3;

per cases ( p in LSeg (NW-corner D),(NE-corner D) or p in LSeg (NE-corner D),(SE-corner D) or p in LSeg (SE-corner D),(SW-corner D) or p in LSeg (SW-corner D),(NW-corner D) ) by A3, XBOOLE_0:def 3;

suppose A4: p in LSeg (NW-corner D),(NE-corner D) ; :: 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~ (SpStSeq D)) = N-bound D by SPRECT_1:68;
then A6: (NE-corner D) `2 = N-bound (L~ f) by A2, EUCLID:56;
(NW-corner D) `2 = N-bound (L~ f) by A2, A5, EUCLID:56;
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 A4, A6, GOBOARD7:6; :: thesis: verum

end;

suppose A7: p in LSeg (NE-corner D),(SE-corner D) ; :: 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~ (SpStSeq D)) = E-bound D by SPRECT_1:69;
then A9: (SE-corner D) `1 = E-bound (L~ f) by A2, EUCLID:56;
(NE-corner D) `1 = E-bound (L~ f) by A2, A8, EUCLID:56;
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 A7, A9, GOBOARD7:5; :: thesis: verum

end;

suppose A10: p in LSeg (SE-corner D),(SW-corner D) ; :: 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~ (SpStSeq D)) = S-bound D by SPRECT_1:67;
then A12: (SW-corner D) `2 = S-bound (L~ f) by A2, EUCLID:56;
(SE-corner D) `2 = S-bound (L~ f) by A2, A11, EUCLID:56;
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 A10, A12, GOBOARD7:6; :: thesis: verum

end;

suppose A13: p in LSeg (SW-corner D),(NW-corner D) ; :: 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~ (SpStSeq D)) = W-bound D by SPRECT_1:66;
then A15: (NW-corner D) `1 = W-bound (L~ f) by A2, EUCLID:56;
(SW-corner D) `1 = W-bound (L~ f) by A2, A14, EUCLID:56;
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 A13, A15, GOBOARD7:5; :: thesis: verum

end;

end;