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;

( 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 Rend;

hence
x in R
; :: thesis: verumper 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;

end;

( P1 is_S-P_arc_joining p,q & P1 c= R ) ) by A4;

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

( 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;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