set P = InclPoset (Ids L);
let f, g be Function of (InclPoset (Ids L)),L; :: thesis: ( ( for I being Ideal of L holds f . I = sup I ) & ( for I being Ideal of L holds g . I = sup I ) implies f = g )
assume that
A3: for I being Ideal of L holds f . I = sup I and
A4: for I being Ideal of L holds g . I = sup I ; :: thesis: f = g
A5: the carrier of (InclPoset (Ids L)) = the carrier of RelStr(# (Ids L),(RelIncl (Ids L)) #) by YELLOW_1:def 1
.= Ids L ;

A6: now :: thesis: for x being object st x in the carrier of (InclPoset (Ids L)) holds
f . x = g . x

let x be object ; :: thesis: ( x in the carrier of (InclPoset (Ids L)) implies f . x = g . x )
assume x in the carrier of (InclPoset (Ids L)) ; :: thesis: f . x = g . x
then ex I being Ideal of L st x = I by A5;
then reconsider I = x as Ideal of L ;
f . I = sup I by A3;
hence f . x = g . x by A4; :: thesis: verum

end;

( dom f = the carrier of (InclPoset (Ids L)) & dom g = the carrier of (InclPoset (Ids L)) ) by FUNCT_2:def 1;
hence f = g by A6, FUNCT_1:2; :: thesis: verum