let R be Relation; :: thesis: ( R is antisymmetric iff R /\ (R ~ ) c= id (dom R) )

A1: now

assume R is antisymmetric ; :: thesis: R /\ (R ~ ) c= id (dom R)
then A2: R is_antisymmetric_in field R by Def12;

now

let a, b be set ; :: thesis: ( [a,b] in R /\ (R ~ ) implies [a,b] in id (dom R) )
assume A3: [a,b] in R /\ (R ~ ) ; :: thesis: [a,b] in id (dom R)
then [a,b] in R ~ by XBOOLE_0:def 4;
then A4: [b,a] in R by RELAT_1:def 7;
then A5: b in dom R by RELAT_1:def 4;
A6: [a,b] in R by A3, XBOOLE_0:def 4;
then ( a in field R & b in field R ) by RELAT_1:30;
then a = b by A2, A6, A4, Def4;
hence [a,b] in id (dom R) by A5, RELAT_1:def 10; :: thesis: verum

end;

hence R /\ (R ~ ) c= id (dom R) by RELAT_1:def 3; :: thesis: verum

end;

now

assume A7: R /\ (R ~ ) c= id (dom R) ; :: thesis: R is antisymmetric

now

let a, b be set ; :: thesis: ( a in field R & b in field R & [a,b] in R & [b,a] in R implies a = b )
assume that
a in field R and
b in field R and
A8: [a,b] in R and
A9: [b,a] in R ; :: thesis: a = b
[a,b] in R ~ by A9, RELAT_1:def 7;
then [a,b] in R /\ (R ~ ) by A8, XBOOLE_0:def 4;
hence a = b by A7, RELAT_1:def 10; :: thesis: verum

end;

then R is_antisymmetric_in field R by Def4;
hence R is antisymmetric by Def12; :: thesis: verum

end;

hence ( R is antisymmetric iff R /\ (R ~ ) c= id (dom R) ) by A1; :: thesis: verum