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

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