theorem :: WELLORD2:23

for X being set holds RelIncl X c= [:X,X:]