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

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

hence RelIncl X is_antisymmetric_in X ; :: thesis: verum

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

hence RelIncl X is_antisymmetric_in X ; :: thesis: verum