let PM be MetrStruct ; :: thesis: for r, p being Real
for y, x, z being Element of PM st PM is triangle & y in (Ball x,r) /\ (Ball z,p) holds
ex q being Real st
( Ball y,q c= Ball x,r & Ball y,q c= Ball z,p )
let r, p be Real; :: thesis: for y, x, z being Element of PM st PM is triangle & y in (Ball x,r) /\ (Ball z,p) holds
ex q being Real st
( Ball y,q c= Ball x,r & Ball y,q c= Ball z,p )
let y, x, z be Element of PM; :: thesis: ( PM is triangle & y in (Ball x,r) /\ (Ball z,p) implies ex q being Real st
( Ball y,q c= Ball x,r & Ball y,q c= Ball z,p ) )
assume A1: PM is triangle ; :: thesis: ( not y in (Ball x,r) /\ (Ball z,p) or ex q being Real st
( Ball y,q c= Ball x,r & Ball y,q c= Ball z,p ) )
assume A2: y in (Ball x,r) /\ (Ball z,p) ; :: thesis: ex q being Real st
( Ball y,q c= Ball x,r & Ball y,q c= Ball z,p )
then y in Ball x,r by XBOOLE_0:def 4;
then consider s being Real such that
s > 0 and
A3: Ball y,s c= Ball x,r by A1, Th30;
y in Ball z,p by A2, XBOOLE_0:def 4;
then consider t being Real such that
t > 0 and
A4: Ball y,t c= Ball z,p by A1, Th30;
take q = min s,t; :: thesis: ( Ball y,q c= Ball x,r & Ball y,q c= Ball z,p )
Ball y,q c= Ball y,s by Th1, XXREAL_0:17;
hence Ball y,q c= Ball x,r by A3, XBOOLE_1:1; :: thesis: Ball y,q c= Ball z,p
Ball y,q c= Ball y,t by Th1, XXREAL_0:17;
hence Ball y,q c= Ball z,p by A4, XBOOLE_1:1; :: thesis: verum