let p be Point of (); :: thesis: for P, R being Subset of () st p in R & P = { q where q is Point of () : ( q = p or ex P1 being Subset of () st
( P1 is_S-P_arc_joining p,q & P1 c= R ) )
}
holds
P c= R

let P, R be Subset of (); :: thesis: ( p in R & P = { q where q is Point of () : ( q = p or ex P1 being Subset of () 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 () : ( q = p or ex P1 being Subset of () 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 () such that
A3: q = x and
A4: ( q = p or ex P1 being Subset of () 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 () 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 () st
( P1 is_S-P_arc_joining p,q & P1 c= R ) ; :: thesis: x in R
then consider P1 being Subset of () such that
A5: P1 is_S-P_arc_joining p,q and
A6: P1 c= R ;
q in P1 by ;
hence x in R by A3, A6; :: thesis: verum
end;
end;
end;
hence x in R ; :: thesis: verum