theorem Th3: :: WAYBEL16:3

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