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: 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;
A2: 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;
A3: 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;
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: L~ f = L~ (SpStSeq (L~ f)) by Th51;
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~ f

proof

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 A5, 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 A1, A2, A4, A3;
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 A1, A2, A4, A3;
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 A5, SPRECT_1:43; :: thesis: verum