let X be set ; :: thesis: RelIncl X is_reflexive_in X
( RelIncl X is reflexive & field (RelIncl X) = X ) by Def1, Th2;
hence RelIncl X is_reflexive_in X by RELAT_2:def 9; :: thesis: verum