:: deftheorem defines is_minimum_of WAYBEL_1:def 6 :
for S being non empty RelStr
for s being Element of S
for X being set holds
( s is_minimum_of X iff ( ex_inf_of X,S & s = "/\" (X,S) & "/\" (X,S) in X ) );