:: deftheorem defines is_minimal_in WAYBEL_4:def 26 :
for L being RelStr
for X being set
for x being Element of L holds
( x is_minimal_in X iff x is_minimal_wrt X, the InternalRel of L );