let f be rectangular FinSequence of (TOP-REAL 2); 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); ( <*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 )
A1:
<*p*> /. 1 = p
by FINSEQ_4:16;
dom <*p*> = {1}
by FINSEQ_1:2, FINSEQ_1:38;
then A2:
1 in dom <*p*>
by TARSKI:def 1;
assume A3:
<*p*> is_in_the_area_of f
; ( ( 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 )
then A4:
W-bound (L~ f) <= p `1
by A2, A1;
A5:
p `2 <= N-bound (L~ f)
by A3, A2, A1;
A6:
S-bound (L~ f) <= p `2
by A3, A2, A1;
A7:
p `1 <= E-bound (L~ f)
by A3, A2, A1;
consider D being non empty compact non horizontal non vertical Subset of (TOP-REAL 2) such that
A8:
f = SpStSeq D
by SPRECT_1:def 2;
A9:
E-bound (L~ (SpStSeq D)) = E-bound D
by SPRECT_1:61;
A10:
N-bound (L~ (SpStSeq D)) = N-bound D
by SPRECT_1:60;
A11:
S-bound (L~ (SpStSeq D)) = S-bound D
by SPRECT_1:59;
A12:
W-bound (L~ (SpStSeq D)) = W-bound D
by SPRECT_1:58;
A13:
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 A8, SPRECT_1:41;
assume A14:
( 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) )
; 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 A14;
suppose A15:
p `1 = W-bound (L~ f)
;
p in L~ fA16:
(NW-corner D) `1 = W-bound D
by EUCLID:52;
A17:
(NW-corner D) `2 = N-bound D
by EUCLID:52;
A18:
(SW-corner D) `2 = S-bound D
by EUCLID:52;
(SW-corner D) `1 = W-bound D
by EUCLID:52;
then
p in LSeg (
(SW-corner D),
(NW-corner D))
by A6, A5, A8, A12, A11, A10, A15, A16, A18, A17, GOBOARD7:7;
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 A13, XBOOLE_0:def 3;
verum end; suppose A19:
p `1 = E-bound (L~ f)
;
p in L~ fA20:
(SE-corner D) `1 = E-bound D
by EUCLID:52;
A21:
(SE-corner D) `2 = S-bound D
by EUCLID:52;
A22:
(NE-corner D) `2 = N-bound D
by EUCLID:52;
(NE-corner D) `1 = E-bound D
by EUCLID:52;
then
p in LSeg (
(NE-corner D),
(SE-corner D))
by A6, A5, A8, A11, A10, A9, A19, A20, A22, A21, GOBOARD7:7;
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 A13, XBOOLE_0:def 3;
verum end; suppose A23:
p `2 = S-bound (L~ f)
;
p in L~ fA24:
(SW-corner D) `1 = W-bound D
by EUCLID:52;
A25:
(SW-corner D) `2 = S-bound D
by EUCLID:52;
A26:
(SE-corner D) `2 = S-bound D
by EUCLID:52;
(SE-corner D) `1 = E-bound D
by EUCLID:52;
then
p in LSeg (
(SE-corner D),
(SW-corner D))
by A4, A7, A8, A12, A11, A9, A23, A24, A26, A25, 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 A13, XBOOLE_0:def 3;
verum end; suppose A27:
p `2 = N-bound (L~ f)
;
p in L~ fA28:
(NE-corner D) `1 = E-bound D
by EUCLID:52;
A29:
(NE-corner D) `2 = N-bound D
by EUCLID:52;
A30:
(NW-corner D) `2 = N-bound D
by EUCLID:52;
(NW-corner D) `1 = W-bound D
by EUCLID:52;
then
p in LSeg (
(NW-corner D),
(NE-corner D))
by A4, A7, A8, A12, A10, A9, A27, A28, A30, A29, 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 A13, XBOOLE_0:def 3;
verum end;