let X be non empty set ; :: thesis: for R being Relation of X st R is_antisymmetric_in X holds
R is antisymmetric
let R be Relation of X; :: thesis: ( R is_antisymmetric_in X implies R is antisymmetric )
assume A1: R is_antisymmetric_in X ; :: thesis: R is antisymmetric
A2: field R c= X \/ X by RELSET_1:19;
let x, y be set ; :: according to RELAT_2:def 4,RELAT_2:def 12 :: thesis: ( not x in field R or not y in field R or not [x,y] in R or not [y,x] in R or x = y )
assume A3: x in field R ; :: thesis: ( not y in field R or not [x,y] in R or not [y,x] in R or x = y )
assume A4: y in field R ; :: thesis: ( not [x,y] in R or not [y,x] in R or x = y )
assume ( [x,y] in R & [y,x] in R ) ; :: thesis: x = y
hence x = y by A1, A2, A3, A4, RELAT_2:def 4; :: thesis: verum