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:41;

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;

( 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:41;

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;

end;

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:60;

then A6: (NE-corner D) `2 = N-bound (L~ f) by A2, EUCLID:52;

(NW-corner D) `2 = N-bound (L~ f) by A2, A5, EUCLID:52;

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;then A6: (NE-corner D) `2 = N-bound (L~ f) by A2, EUCLID:52;

(NW-corner D) `2 = N-bound (L~ f) by A2, A5, EUCLID:52;

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

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:61;

then A9: (SE-corner D) `1 = E-bound (L~ f) by A2, EUCLID:52;

(NE-corner D) `1 = E-bound (L~ f) by A2, A8, EUCLID:52;

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;then A9: (SE-corner D) `1 = E-bound (L~ f) by A2, EUCLID:52;

(NE-corner D) `1 = E-bound (L~ f) by A2, A8, EUCLID:52;

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

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:59;

then A12: (SW-corner D) `2 = S-bound (L~ f) by A2, EUCLID:52;

(SE-corner D) `2 = S-bound (L~ f) by A2, A11, EUCLID:52;

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;then A12: (SW-corner D) `2 = S-bound (L~ f) by A2, EUCLID:52;

(SE-corner D) `2 = S-bound (L~ f) by A2, A11, EUCLID:52;

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

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:58;

then A15: (NW-corner D) `1 = W-bound (L~ f) by A2, EUCLID:52;

(SW-corner D) `1 = W-bound (L~ f) by A2, A14, EUCLID:52;

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;then A15: (NW-corner D) `1 = W-bound (L~ f) by A2, EUCLID:52;

(SW-corner D) `1 = W-bound (L~ f) by A2, A14, EUCLID:52;

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