theorem :: WAYBEL_4:55

for L being RelStr
for X being set
for x being Element of L holds
( x is_maximal_in X iff ( x in X & ( for y being Element of L holds
( not y in X or not x < y ) ) ) )