let X be non empty set ; :: thesis: for R being antisymmetric Relation of X
for x, y being Element of X st x <=_ R,y & y <=_ R,x holds
x = y
let R be antisymmetric Relation of X; :: thesis: for x, y being Element of X st x <=_ R,y & y <=_ R,x holds
x = y
let x, y be Element of X; :: thesis: ( x <=_ R,y & y <=_ R,x implies x = y )
assume A: ( x <=_ R,y & y <=_ R,x ) ; :: thesis: x = y
then ( x in field R & y in field R ) by RELAT_1:15;
hence x = y by A, RELAT_2:def 4, RELAT_2:def 12; :: thesis: verum