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