let X be set ; :: thesis: RelIncl X is_transitive_in X
( RelIncl X is transitive & field (RelIncl X) = X ) by Def1, Th3;
hence RelIncl X is_transitive_in X by RELAT_2:def 16; :: thesis: verum