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 A1: ( p <> q & 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
per cases ( p `1 <> q `1 or p `2 <> q `2 ) by A1, TOPREAL3:11;
suppose A2: 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
per cases ( p `2 = q `2 or p `2 <> q `2 ) ;
suppose A3: 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 A1, A2, A3, Th8; :: thesis: verum
end;
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 )
A5: ( p = |[(p `1 ),(p `2 )]| & q = |[(q `1 ),(q `2 )]| ) by EUCLID:57;
now
per cases ( |[(p `1 ),(q `2 )]| in Ball u,r or |[(q `1 ),(p `2 )]| in Ball u,r ) by A1, A5, TOPREAL3:32;
suppose A6: |[(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 A1, A2, A4, A6, Th9; :: thesis: verum
end;
suppose A7: |[(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 A1, A2, A4, A7, Th10; :: 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 A8: 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
per cases ( p `1 = q `1 or p `1 <> q `1 ) ;
suppose A9: 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 A1, A8, A9, Th7; :: thesis: verum
end;
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 )
A11: ( p = |[(p `1 ),(p `2 )]| & q = |[(q `1 ),(q `2 )]| ) by EUCLID:57;
now
per cases ( |[(p `1 ),(q `2 )]| in Ball u,r or |[(q `1 ),(p `2 )]| in Ball u,r ) by A1, A11, TOPREAL3:32;
suppose A12: |[(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 A1, A8, A10, A12, Th9; :: thesis: verum
end;
suppose A13: |[(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 A1, A8, A10, A13, Th10; :: 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