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