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 that
A2: x in X and
A3: y in X and
A4: [x,y] in R ~ and
A5: [y,x] in R ~ ; :: thesis: x = y
A6: [y,x] in R by A4, RELAT_1:def 7;
[x,y] in R by A5, RELAT_1:def 7;
hence x = y by A1, A2, A3, A6; :: thesis: verum