let R be Relation; :: thesis: for X being set st R is_antisymmetric_in X holds
R ~ is_antisymmetric_in X
let X be set ; :: thesis: ( R is_antisymmetric_in X implies R ~ is_antisymmetric_in X )
assume A1: for x, y being set st x in X & y in X & [x,y] in R & [y,x] in R holds
x = y ; :: according to RELAT_2:def 4 :: thesis: R ~ is_antisymmetric_in X
let x be set ; :: according to RELAT_2:def 4 :: thesis: for b₁ being set holds
( not x in X or not b₁ in X or not [x,b₁] in R ~ or not [b₁,x] in R ~ or x = b₁ )
let y be set ; :: thesis: ( not x in X or not y in X or not [x,y] in R ~ or not [y,x] in R ~ or x = y )
assume A2: ( x in X & y in X & [x,y] in R ~ & [y,x] in R ~ ) ; :: thesis: x = y
then ( [x,y] in R & [y,x] in R ) by RELAT_1:def 7;
hence x = y by A1, A2; :: thesis: verum