let X be object ; :: thesis: for R being Relation holds
( R is antisymmetric iff for x, y being object st [x,y] in R & [y,x] in R holds
x = y )
let R be Relation; :: thesis: ( R is antisymmetric iff for x, y being object st [x,y] in R & [y,x] in R holds
x = y )
thus ( R is antisymmetric implies for x, y being object st [x,y] in R & [y,x] in R holds
x = y ) :: thesis: ( ( for x, y being object st [x,y] in R & [y,x] in R holds
x = y ) implies R is antisymmetric )
proof
assume A0: R is antisymmetric ; :: thesis: for x, y being object st [x,y] in R & [y,x] in R holds
x = y
let x, y be object ; :: thesis: ( [x,y] in R & [y,x] in R implies x = y )
assume A1: ( [x,y] in R & [y,x] in R ) ; :: thesis: x = y
then ( x in field R & y in field R ) by RELAT_1:15;
hence x = y by A0, A1, RELAT_2:def 4, RELAT_2:def 12; :: thesis: verum
end;
assume A1: for x, y being object st [x,y] in R & [y,x] in R holds
x = y ; :: thesis: R is antisymmetric
set X = field R;
for x, y being object st x in field R & y in field R & [x,y] in R & [y,x] in R holds
x = y by A1;
hence R is antisymmetric by RELAT_2:def 12, RELAT_2:def 4; :: thesis: verum