let R be Relation; :: thesis: for a, b being set st R is antisymmetric holds
( [a,b] in R \~ iff ( [a,b] in R & a <> b ) )
let a, b be set ; :: thesis: ( R is antisymmetric implies ( [a,b] in R \~ iff ( [a,b] in R & a <> b ) ) )
assume R is antisymmetric ; :: thesis: ( [a,b] in R \~ iff ( [a,b] in R & a <> b ) )
then A1: R is_antisymmetric_in field R ;
A2: R \~ is_asymmetric_in field (R \~) by RELAT_2:def 13;
hereby :: thesis: ( [a,b] in R & a <> b implies [a,b] in R \~ )
assume A3: [a,b] in R \~ ; :: thesis: ( [a,b] in R & a <> b )
hence [a,b] in R ; :: thesis: a <> b
now :: thesis: not a = b
assume A4: a = b ; :: thesis: contradiction
a in field (R \~) by A3, RELAT_1:15;
hence contradiction by A2, A3, A4; :: thesis: verum
end;
hence a <> b ; :: thesis: verum
end;
assume that
A5: [a,b] in R and
A6: a <> b ; :: thesis: [a,b] in R \~
A7: a in field R by A5, RELAT_1:15;
b in field R by A5, RELAT_1:15;
then not [b,a] in R by A1, A5, A6, A7;
then not [a,b] in R ~ by RELAT_1:def 7;
hence [a,b] in R \~ by A5, XBOOLE_0:def 5; :: thesis: verum