let L be antisymmetric RelStr ; :: thesis: for R being auxiliary(i) Relation of L
for x, y being Element of L st [x,y] in R & [y,x] in R holds
x = y
let R be auxiliary(i) Relation of L; :: thesis: for x, y being Element of L st [x,y] in R & [y,x] in R holds
x = y
let x, y be Element of L; :: thesis: ( [x,y] in R & [y,x] in R implies x = y )
assume ( [x,y] in R & [y,x] in R ) ; :: thesis: x = y
then ( x <= y & y <= x ) by WAYBEL_4:def 4;
hence x = y by ORDERS_2:25; :: thesis: verum