theorem :: WELLORD2:21

for X being set holds RelIncl X is_antisymmetric_in X