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 that
A1: [x,y] in R and
A2: [y,x] in R ; :: thesis: x = y
A3: y <= x by A2, WAYBEL_4:def 3;
x <= y by A1, WAYBEL_4:def 3;
hence x = y by A3, ORDERS_2:2; :: thesis: verum