let PM be MetrStruct ; :: thesis: for r, p being Real
for x, y, 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 x, y, 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 x, y, 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, Th27;
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, Th27;
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; :: 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; :: thesis: verum