let R be Relation; :: thesis: ( R = R \~ iff R is asymmetric )
thus ( R = R \~ implies R is asymmetric ) ; :: thesis: ( R is asymmetric implies R = R \~ )
assume R is asymmetric ; :: thesis: R = R \~
then A1: R is_asymmetric_in field R ;
now :: thesis: for a, b being object holds
( ( [a,b] in R implies [a,b] in R \~ ) & ( [a,b] in R \~ implies [a,b] in R ) )
let a, b be object ; :: thesis: ( ( [a,b] in R implies [a,b] in R \~ ) & ( [a,b] in R \~ implies [a,b] in R ) )
hereby :: thesis: ( [a,b] in R \~ implies [a,b] in R )
assume A2: [a,b] in R ; :: thesis: [a,b] in R \~
then A3: a in field R by RELAT_1:15;
b in field R by A2, RELAT_1:15;
then not [b,a] in R by A1, A2, A3;
then not [a,b] in R ~ by RELAT_1:def 7;
hence [a,b] in R \~ by A2, XBOOLE_0:def 5; :: thesis: verum
end;
assume [a,b] in R \~ ; :: thesis: [a,b] in R
hence [a,b] in R ; :: thesis: verum
end;
hence R = R \~ by RELAT_1:def 2; :: thesis: verum