theorem :: WAYBEL16:4

for L being non empty RelStr
for x, y being Element of L st x is_minimal_in the carrier of L \ (downarrow y) holds
(downarrow x) \ {x} = (downarrow x) /\ (downarrow y)