thus ( R is antisymmetric implies for x, y being set st x,y in R & y,x in R holds
x = y ) :: thesis: ( ( for x, y being set st x,y in R & y,x in R holds
x = y ) implies R is antisymmetric )
proof
assume A2: 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 ; :: according to RELAT_2:def 4,RELAT_2:def 12 :: thesis: for x, y being set st x,y in R & y,x in R holds
x = y
let x, y be set ; :: thesis: ( x,y in R & y,x in R implies x = y )
assume A3: ( [x,y] in R & [y,x] in R ) ; :: according to MMLQUERY:def 1 :: thesis: x = y
then ( x in field R & y in field R ) by RELAT_1:15;
hence x = y by A2, A3; :: thesis: verum
end;
assume A4: for x, y being set st x,y in R & y,x in R holds
x = y ; :: thesis: R is antisymmetric
let x, y be object ; :: 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 )
reconsider xx = x, yy = y as set by TARSKI:1;
assume ( x in field R & y in field R & [x,y] in R & [y,x] in R ) ; :: thesis: x = y
then ( xx,yy in R & yy,xx in R ) ;
hence x = y by A4; :: thesis: verum