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

A1: now :: thesis: ( R is antisymmetric implies R /\ (R ~) c= id (dom R) )

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

then A2: R is_antisymmetric_in field R ;

end;then A2: R is_antisymmetric_in field R ;

now :: thesis: for a, b being object st [a,b] in R /\ (R ~) holds

[a,b] in id (dom R)

hence
R /\ (R ~) c= id (dom R)
; :: thesis: verum[a,b] in id (dom R)

let a, b be object ; :: 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 XTUPLE_0:def 12;

A6: [a,b] in R by A3, XBOOLE_0:def 4;

then ( a in field R & b in field R ) by RELAT_1:15;

then a = b by A2, A6, A4;

hence [a,b] in id (dom R) by A5, RELAT_1:def 10; :: thesis: verum

end;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 XTUPLE_0:def 12;

A6: [a,b] in R by A3, XBOOLE_0:def 4;

then ( a in field R & b in field R ) by RELAT_1:15;

then a = b by A2, A6, A4;

hence [a,b] in id (dom R) by A5, RELAT_1:def 10; :: thesis: verum

now :: thesis: ( R /\ (R ~) c= id (dom R) implies R is antisymmetric )

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

end;now :: thesis: for a, b being object st a in field R & b in field R & [a,b] in R & [b,a] in R holds

a = b

hence
R is antisymmetric
by Def4; :: thesis: veruma = b

let a, b be object ; :: 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;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