:: deftheorem defines is_maximal_in WAYBEL_4:def 24 :
for L being RelStr
for X being set
for x being Element of L holds
( x is_maximal_in X iff x is_maximal_wrt X, the InternalRel of L );