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 )

x = y ; :: thesis: R is antisymmetric

then 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 ;

then R is_antisymmetric_in field R by RELAT_2:def 4;

hence R is antisymmetric by RELAT_2:def 12; :: thesis: verum

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
for x, y being object st [x,y] in R & [y,x] in R holds
assume
R is antisymmetric
; :: thesis: for x, y being object st [x,y] in R & [y,x] in R holds

x = y

then A1: R is_antisymmetric_in field R by RELAT_2:def 12;

let x, y be object ; :: thesis: ( [x,y] in R & [y,x] in R implies x = y )

assume that

A2: [x,y] in R and

A3: [y,x] in R ; :: thesis: x = y

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

hence x = y by A1, A2, A3, RELAT_2:def 4; :: thesis: verum

end;x = y

then A1: R is_antisymmetric_in field R by RELAT_2:def 12;

let x, y be object ; :: thesis: ( [x,y] in R & [y,x] in R implies x = y )

assume that

A2: [x,y] in R and

A3: [y,x] in R ; :: thesis: x = y

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

hence x = y by A1, A2, A3, RELAT_2:def 4; :: thesis: verum

x = y ; :: thesis: R is antisymmetric

then 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 ;

then R is_antisymmetric_in field R by RELAT_2:def 4;

hence R is antisymmetric by RELAT_2:def 12; :: thesis: verum