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 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 A2: ( y in Ball x,r & y in Ball z,p ) by XBOOLE_0:def 4;
then consider s being Real such that
A3: ( s > 0 & Ball y,s c= Ball x,r ) by A1, Th30;
consider t being Real such that
A4: ( t > 0 & Ball y,t c= Ball z,p ) by A1, A2, Th30;
take q = min s,t; :: thesis: ( Ball y,q c= Ball x,r & Ball y,q c= Ball z,p )
( q <= s & q > 0 ) by A3, A4, XXREAL_0:15, XXREAL_0:17;
then Ball y,q c= Ball y,s by Th1;
hence Ball y,q c= Ball x,r by A3, XBOOLE_1:1; :: thesis: Ball y,q c= Ball z,p
( q <= t & q > 0 ) by A3, A4, XXREAL_0:15, XXREAL_0:17;
then Ball y,q c= Ball y,t by Th1;
hence Ball y,q c= Ball z,p by A4, XBOOLE_1:1; :: thesis: verum