let S, X be non empty set ; :: thesis: for R being Relation of X st R is antisymmetric holds

R is_antisymmetric_in S

let R be Relation of X; :: thesis: ( R is antisymmetric implies R is_antisymmetric_in S )

assume R is antisymmetric ; :: thesis: R is_antisymmetric_in S

then A1: R is_antisymmetric_in field R ;

let x, y be object ; :: according to RELAT_2:def 4 :: thesis: ( not x in S or not y in S or not [x,y] in R or not [y,x] in R or x = y )

assume ( x in S & y in S ) ; :: thesis: ( not [x,y] in R or not [y,x] in R or x = y )

assume A2: [x,y] in R ; :: thesis: ( not [y,x] in R or x = y )

then ( x in field R & y in field R ) by RELAT_1:15;

hence ( not [y,x] in R or x = y ) by A1, A2; :: thesis: verum

R is_antisymmetric_in S

let R be Relation of X; :: thesis: ( R is antisymmetric implies R is_antisymmetric_in S )

assume R is antisymmetric ; :: thesis: R is_antisymmetric_in S

then A1: R is_antisymmetric_in field R ;

let x, y be object ; :: according to RELAT_2:def 4 :: thesis: ( not x in S or not y in S or not [x,y] in R or not [y,x] in R or x = y )

assume ( x in S & y in S ) ; :: thesis: ( not [x,y] in R or not [y,x] in R or x = y )

assume A2: [x,y] in R ; :: thesis: ( not [y,x] in R or x = y )

then ( x in field R & y in field R ) by RELAT_1:15;

hence ( not [y,x] in R or x = y ) by A1, A2; :: thesis: verum