let p, q be Point of (TOP-REAL 2); :: thesis: for r being Real
for u being Point of (Euclid 2) st p <> q & p in Ball (u,r) & q in Ball (u,r) holds
ex P being Subset of (TOP-REAL 2) st
( P is_S-P_arc_joining p,q & P c= Ball (u,r) )
let r be Real; :: thesis: for u being Point of (Euclid 2) st p <> q & p in Ball (u,r) & q in Ball (u,r) holds
ex P being Subset of (TOP-REAL 2) st
( P is_S-P_arc_joining p,q & P c= Ball (u,r) )
let u be Point of (Euclid 2); :: thesis: ( p <> q & p in Ball (u,r) & q in Ball (u,r) implies ex P being Subset of (TOP-REAL 2) st
( P is_S-P_arc_joining p,q & P c= Ball (u,r) ) )
assume that
A1: p <> q and
A2: ( p in Ball (u,r) & q in Ball (u,r) ) ; :: thesis: ex P being Subset of (TOP-REAL 2) st
( P is_S-P_arc_joining p,q & P c= Ball (u,r) )
now :: thesis: ex P being Subset of (TOP-REAL 2) st
( P is_S-P_arc_joining p,q & P c= Ball (u,r) )
per cases ( p `1 <> q `1 or p `2 <> q `2 ) by A1, TOPREAL3:6;
suppose A3: p `1 <> q `1 ; :: thesis: ex P being Subset of (TOP-REAL 2) st
( P is_S-P_arc_joining p,q & P c= Ball (u,r) )
now :: thesis: ex P being Subset of (TOP-REAL 2) st
( P is_S-P_arc_joining p,q & P c= Ball (u,r) )
per cases ( p `2 = q `2 or p `2 <> q `2 ) ;
suppose A4: p `2 = q `2 ; :: thesis: ex P being Subset of (TOP-REAL 2) st
( P is_S-P_arc_joining p,q & P c= Ball (u,r) )
reconsider P = L~ <*p,|[(((p `1) + (q `1)) / 2),(p `2)]|,q*> as Subset of (TOP-REAL 2) ;
take P = P; :: thesis: ( P is_S-P_arc_joining p,q & P c= Ball (u,r) )
thus ( P is_S-P_arc_joining p,q & P c= Ball (u,r) ) by A2, A3, A4, Th7; :: thesis: verum
end;
suppose A5: p `2 <> q `2 ; :: thesis: ex P being Subset of (TOP-REAL 2) st
( P is_S-P_arc_joining p,q & P c= Ball (u,r) )
A6: ( p = |[(p `1),(p `2)]| & q = |[(q `1),(q `2)]| ) by EUCLID:53;
now :: thesis: ex P being Subset of (TOP-REAL 2) st
( P is_S-P_arc_joining p,q & P c= Ball (u,r) )
per cases ( |[(p `1),(q `2)]| in Ball (u,r) or |[(q `1),(p `2)]| in Ball (u,r) ) by A2, A6, TOPREAL3:25;
suppose A7: |[(p `1),(q `2)]| in Ball (u,r) ; :: thesis: ex P being Subset of (TOP-REAL 2) st
( P is_S-P_arc_joining p,q & P c= Ball (u,r) )
reconsider P = L~ <*p,|[(p `1),(q `2)]|,q*> as Subset of (TOP-REAL 2) ;
take P = P; :: thesis: ( P is_S-P_arc_joining p,q & P c= Ball (u,r) )
thus ( P is_S-P_arc_joining p,q & P c= Ball (u,r) ) by A2, A3, A5, A7, Th8; :: thesis: verum
end;
suppose A8: |[(q `1),(p `2)]| in Ball (u,r) ; :: thesis: ex P being Subset of (TOP-REAL 2) st
( P is_S-P_arc_joining p,q & P c= Ball (u,r) )
reconsider P = L~ <*p,|[(q `1),(p `2)]|,q*> as Subset of (TOP-REAL 2) ;
take P = P; :: thesis: ( P is_S-P_arc_joining p,q & P c= Ball (u,r) )
thus ( P is_S-P_arc_joining p,q & P c= Ball (u,r) ) by A2, A3, A5, A8, Th9; :: thesis: verum
end;
end;
end;
hence ex P being Subset of (TOP-REAL 2) st
( P is_S-P_arc_joining p,q & P c= Ball (u,r) ) ; :: thesis: verum
end;
end;
end;
hence ex P being Subset of (TOP-REAL 2) st
( P is_S-P_arc_joining p,q & P c= Ball (u,r) ) ; :: thesis: verum
end;
suppose A9: p `2 <> q `2 ; :: thesis: ex P being Subset of (TOP-REAL 2) st
( P is_S-P_arc_joining p,q & P c= Ball (u,r) )
now :: thesis: ex P being Subset of (TOP-REAL 2) st
( P is_S-P_arc_joining p,q & P c= Ball (u,r) )
per cases ( p `1 = q `1 or p `1 <> q `1 ) ;
suppose A10: p `1 = q `1 ; :: thesis: ex P being Subset of (TOP-REAL 2) st
( P is_S-P_arc_joining p,q & P c= Ball (u,r) )
reconsider P = L~ <*p,|[(p `1),(((p `2) + (q `2)) / 2)]|,q*> as Subset of (TOP-REAL 2) ;
take P = P; :: thesis: ( P is_S-P_arc_joining p,q & P c= Ball (u,r) )
thus ( P is_S-P_arc_joining p,q & P c= Ball (u,r) ) by A2, A9, A10, Th6; :: thesis: verum
end;
suppose A11: p `1 <> q `1 ; :: thesis: ex P being Subset of (TOP-REAL 2) st
( P is_S-P_arc_joining p,q & P c= Ball (u,r) )
A12: ( p = |[(p `1),(p `2)]| & q = |[(q `1),(q `2)]| ) by EUCLID:53;
now :: thesis: ex P being Subset of (TOP-REAL 2) st
( P is_S-P_arc_joining p,q & P c= Ball (u,r) )
per cases ( |[(p `1),(q `2)]| in Ball (u,r) or |[(q `1),(p `2)]| in Ball (u,r) ) by A2, A12, TOPREAL3:25;
suppose A13: |[(p `1),(q `2)]| in Ball (u,r) ; :: thesis: ex P being Subset of (TOP-REAL 2) st
( P is_S-P_arc_joining p,q & P c= Ball (u,r) )
reconsider P = L~ <*p,|[(p `1),(q `2)]|,q*> as Subset of (TOP-REAL 2) ;
take P = P; :: thesis: ( P is_S-P_arc_joining p,q & P c= Ball (u,r) )
thus ( P is_S-P_arc_joining p,q & P c= Ball (u,r) ) by A2, A9, A11, A13, Th8; :: thesis: verum
end;
suppose A14: |[(q `1),(p `2)]| in Ball (u,r) ; :: thesis: ex P being Subset of (TOP-REAL 2) st
( P is_S-P_arc_joining p,q & P c= Ball (u,r) )
reconsider P = L~ <*p,|[(q `1),(p `2)]|,q*> as Subset of (TOP-REAL 2) ;
take P = P; :: thesis: ( P is_S-P_arc_joining p,q & P c= Ball (u,r) )
thus ( P is_S-P_arc_joining p,q & P c= Ball (u,r) ) by A2, A9, A11, A14, Th9; :: thesis: verum
end;
end;
end;
hence ex P being Subset of (TOP-REAL 2) st
( P is_S-P_arc_joining p,q & P c= Ball (u,r) ) ; :: thesis: verum
end;
end;
end;
hence ex P being Subset of (TOP-REAL 2) st
( P is_S-P_arc_joining p,q & P c= Ball (u,r) ) ; :: thesis: verum
end;
end;
end;
hence ex P being Subset of (TOP-REAL 2) st
( P is_S-P_arc_joining p,q & P c= Ball (u,r) ) ; :: thesis: verum