let f be rectangular FinSequence of (TOP-REAL 2); :: thesis: for p being Point of (TOP-REAL 2) 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 (TOP-REAL 2); :: 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 )
assume A1:
<*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 )
dom <*p*> = {1}
by FINSEQ_1:4, FINSEQ_1:55;
then
( 1 in dom <*p*> & <*p*> /. 1 = p )
by FINSEQ_4:25, TARSKI:def 1;
then A2:
( W-bound (L~ f) <= p `1 & p `1 <= E-bound (L~ f) & S-bound (L~ f) <= p `2 & p `2 <= N-bound (L~ f) )
by A1, SPRECT_2:def 1;
consider D being non empty compact non horizontal non vertical Subset of (TOP-REAL 2) such that
A3:
f = SpStSeq D
by SPRECT_1:def 2;
A4:
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 A3, SPRECT_1:43;
A5:
W-bound (L~ (SpStSeq D)) = W-bound D
by SPRECT_1:66;
A6:
S-bound (L~ (SpStSeq D)) = S-bound D
by SPRECT_1:67;
A7:
N-bound (L~ (SpStSeq D)) = N-bound D
by SPRECT_1:68;
A8:
E-bound (L~ (SpStSeq D)) = E-bound D
by SPRECT_1:69;
assume A9:
( 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 A9;
suppose A10:
p `1 = W-bound (L~ f)
;
:: thesis: p in L~ fA11:
(
(SW-corner D) `1 = W-bound D &
(NW-corner D) `1 = W-bound D )
by EUCLID:56;
(
(SW-corner D) `2 = S-bound D &
(NW-corner D) `2 = N-bound D )
by EUCLID:56;
then
p in LSeg (SW-corner D),
(NW-corner D)
by A2, A3, A5, A6, A7, A10, A11, GOBOARD7:8;
then
p in (LSeg (SE-corner D),(SW-corner D)) \/ (LSeg (SW-corner D),(NW-corner D))
by XBOOLE_0:def 3;
hence
p in L~ f
by A4, XBOOLE_0:def 3;
:: thesis: verum end; suppose A12:
p `1 = E-bound (L~ f)
;
:: thesis: p in L~ fA13:
(
(NE-corner D) `1 = E-bound D &
(SE-corner D) `1 = E-bound D )
by EUCLID:56;
(
(NE-corner D) `2 = N-bound D &
(SE-corner D) `2 = S-bound D )
by EUCLID:56;
then
p in LSeg (NE-corner D),
(SE-corner D)
by A2, A3, A6, A7, A8, A12, A13, GOBOARD7:8;
then
p in (LSeg (NW-corner D),(NE-corner D)) \/ (LSeg (NE-corner D),(SE-corner D))
by XBOOLE_0:def 3;
hence
p in L~ f
by A4, XBOOLE_0:def 3;
:: thesis: verum end; suppose A14:
p `2 = S-bound (L~ f)
;
:: thesis: p in L~ fA15:
(
(SE-corner D) `1 = E-bound D &
(SW-corner D) `1 = W-bound D )
by EUCLID:56;
(
(SE-corner D) `2 = S-bound D &
(SW-corner D) `2 = S-bound D )
by EUCLID:56;
then
p in LSeg (SE-corner D),
(SW-corner D)
by A2, A3, A5, A6, A8, A14, A15, GOBOARD7:9;
then
p in (LSeg (SE-corner D),(SW-corner D)) \/ (LSeg (SW-corner D),(NW-corner D))
by XBOOLE_0:def 3;
hence
p in L~ f
by A4, XBOOLE_0:def 3;
:: thesis: verum end; suppose A16:
p `2 = N-bound (L~ f)
;
:: thesis: p in L~ fA17:
(
(NW-corner D) `1 = W-bound D &
(NE-corner D) `1 = E-bound D )
by EUCLID:56;
(
(NW-corner D) `2 = N-bound D &
(NE-corner D) `2 = N-bound D )
by EUCLID:56;
then
p in LSeg (NW-corner D),
(NE-corner D)
by A2, A3, A5, A7, A8, A16, A17, GOBOARD7:9;
then
p in (LSeg (NW-corner D),(NE-corner D)) \/ (LSeg (NE-corner D),(SE-corner D))
by XBOOLE_0:def 3;
hence
p in L~ f
by A4, XBOOLE_0:def 3;
:: thesis: verum end;