let X be non empty set ; :: thesis: for R being Relation of X st R is_asymmetric_in X holds
R is asymmetric
let R be Relation of X; :: thesis: ( R is_asymmetric_in X implies R is asymmetric )
assume A1: R is_asymmetric_in X ; :: thesis: R is asymmetric
let x, y be object ; :: according to RELAT_2:def 5,RELAT_2:def 13 :: thesis: ( not x in field R or not y in field R or not [x,y] in R or not [y,x] in R )
field R c= X \/ X by RELSET_1:8;
hence ( not x in field R or not y in field R or not [x,y] in R or not [y,x] in R ) by A1; :: thesis: verum