let S be non empty Poset; :: thesis: for w1, w2 being Element of the carrier of S * st S is discrete & w1 <= w2 holds
w1 = w2
let w1, w2 be Element of the carrier of S * ; :: thesis: ( S is discrete & w1 <= w2 implies w1 = w2 )
assume A1: ( S is discrete & w1 <= w2 ) ; :: thesis: w1 = w2
then reconsider S1 = S as non empty discrete Poset ;
len w1 = len w2 by A1, 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;
A4: s3 <= s4 by A1, A3, Def7;
reconsider s5 = s3, s6 = s4 as Element of S1 ;
s5 = s6 by A4, ORDERS_3:1;
hence w1 . i = w2 . i ; :: thesis: verum

end;

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