let X be set ; :: thesis: RelIncl X is_antisymmetric_in X
( RelIncl X is antisymmetric & field (RelIncl X) = X ) by Def1, Th5;
hence RelIncl X is_antisymmetric_in X by RELAT_2:def 12; :: thesis: verum