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 A1: ( w1 <= w2 & w2 <= w1 ) ; :: thesis: w1 = w2
then len w1 = len w2 by Def7;
then A2: dom w1 = dom w2 by FINSEQ_3:31;
for i being set st i in dom w1 holds
w1 . i = w2 . i

proof

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

end;

hence w1 = w2 by A2, FUNCT_1:9; :: thesis: verum