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