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 per cases
( p `1 <> q `1 or p `2 <> q `2 )
by A1, TOPREAL3:11;
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 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, Th8;
:: 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:57;
now per cases
( |[(p `1 ),(q `2 )]| in Ball u,r or |[(q `1 ),(p `2 )]| in Ball u,r )
by A2, A6, TOPREAL3:32;
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, Th9;
:: 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, Th10;
:: thesis: verum 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; 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 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 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, Th7;
:: 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:57;
now per cases
( |[(p `1 ),(q `2 )]| in Ball u,r or |[(q `1 ),(p `2 )]| in Ball u,r )
by A2, A12, TOPREAL3:32;
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, Th9;
:: 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, Th10;
:: thesis: verum 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; 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
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