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:23;
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:24;
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: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:25;
A5: L~ f = L~ (SpStSeq (L~ f)) by Th34;
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 object ; :: 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:41;
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 object ; :: 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:41; :: thesis: verum