let p be Point of (TOP-REAL 2); :: thesis: for R, P being Subset of (TOP-REAL 2) st R is being_Region & p in R & P = { q where q is Point of (TOP-REAL 2) : ( q = p or ex P1 being Subset of (TOP-REAL 2) st
( P1 is_S-P_arc_joining p,q & P1 c= R ) ) } holds
R = P
let R, P be Subset of (TOP-REAL 2); :: thesis: ( R is being_Region & p in R & P = { q where q is Point of (TOP-REAL 2) : ( q = p or ex P1 being Subset of (TOP-REAL 2) st
( P1 is_S-P_arc_joining p,q & P1 c= R ) ) } implies R = P )
assume A1: ( R is being_Region & p in R & P = { q where q is Point of (TOP-REAL 2) : ( q = p or ex P1 being Subset of (TOP-REAL 2) st
( P1 is_S-P_arc_joining p,q & P1 c= R ) ) } ) ; :: thesis: R = P
hence R c= P by Th28; :: according to XBOOLE_0:def 10 :: thesis: P c= R
thus P c= R by A1, Th27; :: thesis: verum