theorem Th26: :: TOPREAL4:26
for p being Point of (TOP-REAL 2)
for P, R being Subset of (TOP-REAL 2) st 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
P c= R