let S be non empty Poset; :: thesis: for w1, w2 being Element of the carrier of S * st w1 <= w2 & w2 <= w1 holds
w1 = w2
let w1, w2 be Element of the carrier of S * ; :: thesis: ( w1 <= w2 & w2 <= w1 implies w1 = w2 )
assume that
A1: w1 <= w2 and
A2: w2 <= w1 ; :: thesis: w1 = w2
len w1 = len w2 by A1;
then A3: dom w1 = dom w2 by FINSEQ_3:29;
for i being object st i in dom w1 holds
w1 . i = w2 . i

proof

let i be object ; :: thesis: ( i in dom w1 implies w1 . i = w2 . i )
assume A4: i in dom w1 ; :: thesis: w1 . i = w2 . i
reconsider s3 = w1 . i, s4 = w2 . i as Element of S by A3, A4, PARTFUN1:4;
( s3 <= s4 & s4 <= s3 ) by A1, A2, A3, A4;
hence w1 . i = w2 . i by ORDERS_2:2; :: thesis: verum

end;

hence w1 = w2 by A3, FUNCT_1:2; :: thesis: verum