theorem Th28: :: WAYBEL19:28

for R being non empty reflexive antisymmetric RelStr
for x being Element of R holds (uparrow x) /\ (downarrow x) = {x}