let p be Point of (TOP-REAL 2); :: thesis: 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
let P, R be Subset of (TOP-REAL 2); :: thesis: ( 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 P c= R )
assume that
A1: p in R and
A2: 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: P c= R
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in P or x in R )
assume x in P ; :: thesis: x in R
then consider q being Point of (TOP-REAL 2) such that
A3: q = x and
A4: ( q = p or ex P1 being Subset of (TOP-REAL 2) st
( P1 is_S-P_arc_joining p,q & P1 c= R ) ) by A2;
now :: thesis: x in R
per cases ( q = p or ex P1 being Subset of (TOP-REAL 2) st
( P1 is_S-P_arc_joining p,q & P1 c= R ) ) by A4;
suppose q = p ; :: thesis: x in R
hence x in R by A1, A3; :: thesis: verum
end;
suppose ex P1 being Subset of (TOP-REAL 2) st
( P1 is_S-P_arc_joining p,q & P1 c= R ) ; :: thesis: x in R
then consider P1 being Subset of (TOP-REAL 2) such that
A5: P1 is_S-P_arc_joining p,q and
A6: P1 c= R ;
q in P1 by A5, Th3;
hence x in R by A3, A6; :: thesis: verum
end;
end;
end;
hence x in R ; :: thesis: verum