let f be rectangular special_circular_sequence; :: thesis: L~ f = { p where p is Point of (TOP-REAL 2) : ( ( p `1 = W-bound (L~ f) & p `2 <= N-bound (L~ f) & p `2 >= S-bound (L~ f) ) or ( p `1 <= E-bound (L~ f) & p `1 >= W-bound (L~ f) & p `2 = N-bound (L~ f) ) or ( p `1 <= E-bound (L~ f) & p `1 >= W-bound (L~ f) & p `2 = S-bound (L~ f) ) or ( p `1 = E-bound (L~ f) & p `2 <= N-bound (L~ f) & p `2 >= S-bound (L~ f) ) ) }
set C = L~ f;
set E = { p where p is Point of (TOP-REAL 2) : ( p `1 = E-bound (L~ f) & p `2 <= N-bound (L~ f) & p `2 >= S-bound (L~ f) ) } ;
set S = { p where p is Point of (TOP-REAL 2) : ( p `1 <= E-bound (L~ f) & p `1 >= W-bound (L~ f) & p `2 = S-bound (L~ f) ) } ;
set N = { p where p is Point of (TOP-REAL 2) : ( p `1 <= E-bound (L~ f) & p `1 >= W-bound (L~ f) & p `2 = N-bound (L~ f) ) } ;
set W = { p where p is Point of (TOP-REAL 2) : ( p `1 = W-bound (L~ f) & p `2 <= N-bound (L~ f) & p `2 >= S-bound (L~ f) ) } ;
A1:
L~ f = L~ (SpStSeq (L~ f))
by Th51;
A2:
LSeg (SE-corner (L~ f)),(NE-corner (L~ f)) = { p where p is Point of (TOP-REAL 2) : ( p `1 = E-bound (L~ f) & p `2 <= N-bound (L~ f) & p `2 >= S-bound (L~ f) ) }
by SPRECT_1:25;
A3:
LSeg (SW-corner (L~ f)),(SE-corner (L~ f)) = { p where p is Point of (TOP-REAL 2) : ( p `1 <= E-bound (L~ f) & p `1 >= W-bound (L~ f) & p `2 = S-bound (L~ f) ) }
by SPRECT_1:26;
A4:
LSeg (NW-corner (L~ f)),(NE-corner (L~ f)) = { p where p is Point of (TOP-REAL 2) : ( p `1 <= E-bound (L~ f) & p `1 >= W-bound (L~ f) & p `2 = N-bound (L~ f) ) }
by SPRECT_1:27;
A5:
LSeg (SW-corner (L~ f)),(NW-corner (L~ f)) = { p where p is Point of (TOP-REAL 2) : ( p `1 = W-bound (L~ f) & p `2 <= N-bound (L~ f) & p `2 >= S-bound (L~ f) ) }
by SPRECT_1:28;
thus
L~ f c= { p where p is Point of (TOP-REAL 2) : ( ( p `1 = W-bound (L~ f) & p `2 <= N-bound (L~ f) & p `2 >= S-bound (L~ f) ) or ( p `1 <= E-bound (L~ f) & p `1 >= W-bound (L~ f) & p `2 = N-bound (L~ f) ) or ( p `1 <= E-bound (L~ f) & p `1 >= W-bound (L~ f) & p `2 = S-bound (L~ f) ) or ( p `1 = E-bound (L~ f) & p `2 <= N-bound (L~ f) & p `2 >= S-bound (L~ f) ) ) }
:: according to XBOOLE_0:def 10 :: thesis: { p where p is Point of (TOP-REAL 2) : ( ( p `1 = W-bound (L~ f) & p `2 <= N-bound (L~ f) & p `2 >= S-bound (L~ f) ) or ( p `1 <= E-bound (L~ f) & p `1 >= W-bound (L~ f) & p `2 = N-bound (L~ f) ) or ( p `1 <= E-bound (L~ f) & p `1 >= W-bound (L~ f) & p `2 = S-bound (L~ f) ) or ( p `1 = E-bound (L~ f) & p `2 <= N-bound (L~ f) & p `2 >= S-bound (L~ f) ) ) } c= L~ fproof
let x be
set ;
:: according to TARSKI:def 3 :: thesis: ( not x in L~ f or x in { p where p is Point of (TOP-REAL 2) : ( ( p `1 = W-bound (L~ f) & p `2 <= N-bound (L~ f) & p `2 >= S-bound (L~ f) ) or ( p `1 <= E-bound (L~ f) & p `1 >= W-bound (L~ f) & p `2 = N-bound (L~ f) ) or ( p `1 <= E-bound (L~ f) & p `1 >= W-bound (L~ f) & p `2 = S-bound (L~ f) ) or ( p `1 = E-bound (L~ f) & p `2 <= N-bound (L~ f) & p `2 >= S-bound (L~ f) ) ) } )
assume A6:
x in L~ f
;
:: thesis: x in { p where p is Point of (TOP-REAL 2) : ( ( p `1 = W-bound (L~ f) & p `2 <= N-bound (L~ f) & p `2 >= S-bound (L~ f) ) or ( p `1 <= E-bound (L~ f) & p `1 >= W-bound (L~ f) & p `2 = N-bound (L~ f) ) or ( p `1 <= E-bound (L~ f) & p `1 >= W-bound (L~ f) & p `2 = S-bound (L~ f) ) or ( p `1 = E-bound (L~ f) & p `2 <= N-bound (L~ f) & p `2 >= S-bound (L~ f) ) ) }
then reconsider q =
x as
Point of
(TOP-REAL 2) ;
q in ((LSeg (NW-corner (L~ f)),(NE-corner (L~ f))) \/ (LSeg (NE-corner (L~ f)),(SE-corner (L~ f)))) \/ ((LSeg (SE-corner (L~ f)),(SW-corner (L~ f))) \/ (LSeg (SW-corner (L~ f)),(NW-corner (L~ f))))
by A1, A6, SPRECT_1:43;
then
(
q in (LSeg (NW-corner (L~ f)),(NE-corner (L~ f))) \/ (LSeg (NE-corner (L~ f)),(SE-corner (L~ f))) or
q in (LSeg (SE-corner (L~ f)),(SW-corner (L~ f))) \/ (LSeg (SW-corner (L~ f)),(NW-corner (L~ f))) )
by XBOOLE_0:def 3;
then
(
q in LSeg (NW-corner (L~ f)),
(NE-corner (L~ f)) or
q in LSeg (NE-corner (L~ f)),
(SE-corner (L~ f)) or
q in LSeg (SE-corner (L~ f)),
(SW-corner (L~ f)) or
q in LSeg (SW-corner (L~ f)),
(NW-corner (L~ f)) )
by XBOOLE_0:def 3;
then
( ex
p being
Point of
(TOP-REAL 2) st
(
x = p &
p `1 = E-bound (L~ f) &
p `2 <= N-bound (L~ f) &
p `2 >= S-bound (L~ f) ) or ex
p being
Point of
(TOP-REAL 2) st
(
x = p &
p `1 <= E-bound (L~ f) &
p `1 >= W-bound (L~ f) &
p `2 = S-bound (L~ f) ) or ex
p being
Point of
(TOP-REAL 2) st
(
x = p &
p `1 <= E-bound (L~ f) &
p `1 >= W-bound (L~ f) &
p `2 = N-bound (L~ f) ) or ex
p being
Point of
(TOP-REAL 2) st
(
x = p &
p `1 = W-bound (L~ f) &
p `2 <= N-bound (L~ f) &
p `2 >= S-bound (L~ f) ) )
by A2, A3, A4, A5;
hence
x in { p where p is Point of (TOP-REAL 2) : ( ( p `1 = W-bound (L~ f) & p `2 <= N-bound (L~ f) & p `2 >= S-bound (L~ f) ) or ( p `1 <= E-bound (L~ f) & p `1 >= W-bound (L~ f) & p `2 = N-bound (L~ f) ) or ( p `1 <= E-bound (L~ f) & p `1 >= W-bound (L~ f) & p `2 = S-bound (L~ f) ) or ( p `1 = E-bound (L~ f) & p `2 <= N-bound (L~ f) & p `2 >= S-bound (L~ f) ) ) }
;
:: thesis: verum
end;
let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in { p where p is Point of (TOP-REAL 2) : ( ( p `1 = W-bound (L~ f) & p `2 <= N-bound (L~ f) & p `2 >= S-bound (L~ f) ) or ( p `1 <= E-bound (L~ f) & p `1 >= W-bound (L~ f) & p `2 = N-bound (L~ f) ) or ( p `1 <= E-bound (L~ f) & p `1 >= W-bound (L~ f) & p `2 = S-bound (L~ f) ) or ( p `1 = E-bound (L~ f) & p `2 <= N-bound (L~ f) & p `2 >= S-bound (L~ f) ) ) } or x in L~ f )
assume
x in { p where p is Point of (TOP-REAL 2) : ( ( p `1 = W-bound (L~ f) & p `2 <= N-bound (L~ f) & p `2 >= S-bound (L~ f) ) or ( p `1 <= E-bound (L~ f) & p `1 >= W-bound (L~ f) & p `2 = N-bound (L~ f) ) or ( p `1 <= E-bound (L~ f) & p `1 >= W-bound (L~ f) & p `2 = S-bound (L~ f) ) or ( p `1 = E-bound (L~ f) & p `2 <= N-bound (L~ f) & p `2 >= S-bound (L~ f) ) ) }
; :: thesis: x in L~ f
then
ex p being Point of (TOP-REAL 2) st
( x = p & ( ( p `1 = W-bound (L~ f) & p `2 <= N-bound (L~ f) & p `2 >= S-bound (L~ f) ) or ( p `1 <= E-bound (L~ f) & p `1 >= W-bound (L~ f) & p `2 = N-bound (L~ f) ) or ( p `1 <= E-bound (L~ f) & p `1 >= W-bound (L~ f) & p `2 = S-bound (L~ f) ) or ( p `1 = E-bound (L~ f) & p `2 <= N-bound (L~ f) & p `2 >= S-bound (L~ f) ) ) )
;
then
( x in LSeg (NW-corner (L~ f)),(NE-corner (L~ f)) or x in LSeg (NE-corner (L~ f)),(SE-corner (L~ f)) or x in LSeg (SE-corner (L~ f)),(SW-corner (L~ f)) or x in LSeg (SW-corner (L~ f)),(NW-corner (L~ f)) )
by A2, A3, A4, A5;
then
( x in (LSeg (NW-corner (L~ f)),(NE-corner (L~ f))) \/ (LSeg (NE-corner (L~ f)),(SE-corner (L~ f))) or x in (LSeg (SE-corner (L~ f)),(SW-corner (L~ f))) \/ (LSeg (SW-corner (L~ f)),(NW-corner (L~ f))) )
by XBOOLE_0:def 3;
then
x in ((LSeg (NW-corner (L~ f)),(NE-corner (L~ f))) \/ (LSeg (NE-corner (L~ f)),(SE-corner (L~ f)))) \/ ((LSeg (SE-corner (L~ f)),(SW-corner (L~ f))) \/ (LSeg (SW-corner (L~ f)),(NW-corner (L~ f))))
by XBOOLE_0:def 3;
hence
x in L~ f
by A1, SPRECT_1:43; :: thesis: verum