theorem :: WELLORD2:19

for X being set holds RelIncl X is_reflexive_in X by Def1;