let p, q be Point of (TOP-REAL 2); :: thesis: for R being Subset of (TOP-REAL 2) st R is being_Region & p in R & q in R & p <> q holds

ex P being Subset of (TOP-REAL 2) st

( P is_S-P_arc_joining p,q & P c= R )

let R be Subset of (TOP-REAL 2); :: thesis: ( R is being_Region & p in R & q in R & p <> q implies ex P being Subset of (TOP-REAL 2) st

( P is_S-P_arc_joining p,q & P c= R ) )

set RR = { q2 where q2 is Point of (TOP-REAL 2) : ( q2 = p or ex P1 being Subset of (TOP-REAL 2) st

( P1 is_S-P_arc_joining p,q2 & P1 c= R ) ) } ;

{ q2 where q2 is Point of (TOP-REAL 2) : ( q2 = p or ex P1 being Subset of (TOP-REAL 2) st

( P1 is_S-P_arc_joining p,q2 & P1 c= R ) ) } c= the carrier of (TOP-REAL 2)

( P1 is_S-P_arc_joining p,q2 & P1 c= R ) ) } as Subset of (TOP-REAL 2) ;

assume that

A1: ( R is being_Region & p in R ) and

A2: q in R and

A3: p <> q ; :: thesis: ex P being Subset of (TOP-REAL 2) st

( P is_S-P_arc_joining p,q & P c= R )

R c= RR by A1, Th27;

then q in RR by A2;

then ex q1 being Point of (TOP-REAL 2) st

( q1 = q & ( q1 = p or ex P1 being Subset of (TOP-REAL 2) st

( P1 is_S-P_arc_joining p,q1 & P1 c= R ) ) ) ;

hence ex P being Subset of (TOP-REAL 2) st

( P is_S-P_arc_joining p,q & P c= R ) by A3; :: thesis: verum

ex P being Subset of (TOP-REAL 2) st

( P is_S-P_arc_joining p,q & P c= R )

let R be Subset of (TOP-REAL 2); :: thesis: ( R is being_Region & p in R & q in R & p <> q implies ex P being Subset of (TOP-REAL 2) st

( P is_S-P_arc_joining p,q & P c= R ) )

set RR = { q2 where q2 is Point of (TOP-REAL 2) : ( q2 = p or ex P1 being Subset of (TOP-REAL 2) st

( P1 is_S-P_arc_joining p,q2 & P1 c= R ) ) } ;

{ q2 where q2 is Point of (TOP-REAL 2) : ( q2 = p or ex P1 being Subset of (TOP-REAL 2) st

( P1 is_S-P_arc_joining p,q2 & P1 c= R ) ) } c= the carrier of (TOP-REAL 2)

proof

then reconsider RR = { q2 where q2 is Point of (TOP-REAL 2) : ( q2 = p or ex P1 being Subset of (TOP-REAL 2) st
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in { q2 where q2 is Point of (TOP-REAL 2) : ( q2 = p or ex P1 being Subset of (TOP-REAL 2) st

( P1 is_S-P_arc_joining p,q2 & P1 c= R ) ) } or x in the carrier of (TOP-REAL 2) )

assume x in { q2 where q2 is Point of (TOP-REAL 2) : ( q2 = p or ex P1 being Subset of (TOP-REAL 2) st

( P1 is_S-P_arc_joining p,q2 & P1 c= R ) ) } ; :: thesis: x in the carrier of (TOP-REAL 2)

then ex q2 being Point of (TOP-REAL 2) st

( q2 = x & ( q2 = p or ex P1 being Subset of (TOP-REAL 2) st

( P1 is_S-P_arc_joining p,q2 & P1 c= R ) ) ) ;

hence x in the carrier of (TOP-REAL 2) ; :: thesis: verum

end;( P1 is_S-P_arc_joining p,q2 & P1 c= R ) ) } or x in the carrier of (TOP-REAL 2) )

assume x in { q2 where q2 is Point of (TOP-REAL 2) : ( q2 = p or ex P1 being Subset of (TOP-REAL 2) st

( P1 is_S-P_arc_joining p,q2 & P1 c= R ) ) } ; :: thesis: x in the carrier of (TOP-REAL 2)

then ex q2 being Point of (TOP-REAL 2) st

( q2 = x & ( q2 = p or ex P1 being Subset of (TOP-REAL 2) st

( P1 is_S-P_arc_joining p,q2 & P1 c= R ) ) ) ;

hence x in the carrier of (TOP-REAL 2) ; :: thesis: verum

( P1 is_S-P_arc_joining p,q2 & P1 c= R ) ) } as Subset of (TOP-REAL 2) ;

assume that

A1: ( R is being_Region & p in R ) and

A2: q in R and

A3: p <> q ; :: thesis: ex P being Subset of (TOP-REAL 2) st

( P is_S-P_arc_joining p,q & P c= R )

R c= RR by A1, Th27;

then q in RR by A2;

then ex q1 being Point of (TOP-REAL 2) st

( q1 = q & ( q1 = p or ex P1 being Subset of (TOP-REAL 2) st

( P1 is_S-P_arc_joining p,q1 & P1 c= R ) ) ) ;

hence ex P being Subset of (TOP-REAL 2) st

( P is_S-P_arc_joining p,q & P c= R ) by A3; :: thesis: verum