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