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