let r be Real; :: thesis: for P being Subset of (TOP-REAL 2) st P = { p where p is Point of (TOP-REAL 2) : p `1 = r } holds

P is closed

let P be Subset of (TOP-REAL 2); :: thesis: ( P = { p where p is Point of (TOP-REAL 2) : p `1 = r } implies P is closed )

assume A1: P = { p where p is Point of (TOP-REAL 2) : p `1 = r } ; :: thesis: P is closed

defpred S_{1}[ Point of (TOP-REAL 2)] means $1 `1 >= r;

{ p where p is Element of (TOP-REAL 2) : S_{1}[p] } is Subset of (TOP-REAL 2)
from DOMAIN_1:sch 7();

then reconsider P1 = { p where p is Point of (TOP-REAL 2) : p `1 >= r } as Subset of (TOP-REAL 2) ;

A2: P1 is closed by Th4;

defpred S_{2}[ Point of (TOP-REAL 2)] means $1 `1 <= r;

{ p where p is Element of (TOP-REAL 2) : S_{2}[p] } is Subset of (TOP-REAL 2)
from DOMAIN_1:sch 7();

then reconsider P2 = { p where p is Point of (TOP-REAL 2) : p `1 <= r } as Subset of (TOP-REAL 2) ;

A3: P2 is closed by Th5;

A4: P c= P1 /\ P2

hence P is closed by A2, A3, TOPS_1:8; :: thesis: verum

P is closed

let P be Subset of (TOP-REAL 2); :: thesis: ( P = { p where p is Point of (TOP-REAL 2) : p `1 = r } implies P is closed )

assume A1: P = { p where p is Point of (TOP-REAL 2) : p `1 = r } ; :: thesis: P is closed

defpred S

{ p where p is Element of (TOP-REAL 2) : S

then reconsider P1 = { p where p is Point of (TOP-REAL 2) : p `1 >= r } as Subset of (TOP-REAL 2) ;

A2: P1 is closed by Th4;

defpred S

{ p where p is Element of (TOP-REAL 2) : S

then reconsider P2 = { p where p is Point of (TOP-REAL 2) : p `1 <= r } as Subset of (TOP-REAL 2) ;

A3: P2 is closed by Th5;

A4: P c= P1 /\ P2

proof

P1 /\ P2 c= P
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in P or x in P1 /\ P2 )

assume x in P ; :: thesis: x in P1 /\ P2

then A5: ex p being Point of (TOP-REAL 2) st

( p = x & p `1 = r ) by A1;

then A6: x in P1 ;

x in P2 by A5;

hence x in P1 /\ P2 by A6, XBOOLE_0:def 4; :: thesis: verum

end;assume x in P ; :: thesis: x in P1 /\ P2

then A5: ex p being Point of (TOP-REAL 2) st

( p = x & p `1 = r ) by A1;

then A6: x in P1 ;

x in P2 by A5;

hence x in P1 /\ P2 by A6, XBOOLE_0:def 4; :: thesis: verum

proof

then
P = P1 /\ P2
by A4;
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in P1 /\ P2 or x in P )

assume A7: x in P1 /\ P2 ; :: thesis: x in P

then A8: x in P1 by XBOOLE_0:def 4;

A9: x in P2 by A7, XBOOLE_0:def 4;

consider q1 being Point of (TOP-REAL 2) such that

A10: q1 = x and

A11: q1 `1 >= r by A8;

ex q2 being Point of (TOP-REAL 2) st

( q2 = x & q2 `1 <= r ) by A9;

then q1 `1 = r by A10, A11, XXREAL_0:1;

hence x in P by A1, A10; :: thesis: verum

end;assume A7: x in P1 /\ P2 ; :: thesis: x in P

then A8: x in P1 by XBOOLE_0:def 4;

A9: x in P2 by A7, XBOOLE_0:def 4;

consider q1 being Point of (TOP-REAL 2) such that

A10: q1 = x and

A11: q1 `1 >= r by A8;

ex q2 being Point of (TOP-REAL 2) st

( q2 = x & q2 `1 <= r ) by A9;

then q1 `1 = r by A10, A11, XXREAL_0:1;

hence x in P by A1, A10; :: thesis: verum

hence P is closed by A2, A3, TOPS_1:8; :: thesis: verum