let X be set ; :: thesis: RelIncl X is_transitive_in X

( RelIncl X is transitive & field (RelIncl X) = X ) by Def1;

hence RelIncl X is_transitive_in X ; :: thesis: verum

( RelIncl X is transitive & field (RelIncl X) = X ) by Def1;

hence RelIncl X is_transitive_in X ; :: thesis: verum