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 that
A1: S is discrete and
A2: w1 <= w2 ; :: thesis: w1 = w2
reconsider S1 = S as non empty discrete Poset by A1;
len w1 = len w2 by A2;
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;
reconsider s5 = s3, s6 = s4 as Element of S1 ;
s3 <= s4 by A2, A4;
then s5 = s6 by ORDERS_3:1;
hence w1 . i = w2 . i ; :: thesis: verum
end;
hence w1 = w2 by A3, FUNCT_1:2; :: thesis: verum