let L be complete LATTICE; :: thesis: for mp being Function of L,(InclPoset (Ids L)) st mp is approximating & mp in the carrier of (MonSet L) holds
ex AR being auxiliary approximating Relation of L st AR = (Map2Rel L) . mp
let mp be Function of L,(InclPoset (Ids L)); :: thesis: ( mp is approximating & mp in the carrier of (MonSet L) implies ex AR being auxiliary approximating Relation of L st AR = (Map2Rel L) . mp )
assume that
A1: mp is approximating and
A2: mp in the carrier of (MonSet L) ; :: thesis: ex AR being auxiliary approximating Relation of L st AR = (Map2Rel L) . mp
consider AR being auxiliary Relation of L such that
A3: AR = (Map2Rel L) . mp and
A4: for x, y being object holds
( [x,y] in AR iff ex x9, y9 being Element of L ex s9 being Function of L,(InclPoset (Ids L)) st
( x9 = x & y9 = y & s9 = mp & x9 in s9 . y9 ) ) by A2, Def15;

now :: thesis: for x being Element of L holds x = sup (AR -below x)

let x be Element of L; :: thesis: x = sup (AR -below x)
A5: ex ii being Subset of L st
( ii = mp . x & x = sup ii ) by A1;
A6: AR -below x c= mp . x

proof

let a be object ; :: according to TARSKI:def 3 :: thesis: ( not a in AR -below x or a in mp . x )
assume a in AR -below x ; :: thesis: a in mp . x
then [a,x] in AR by Th13;
then ex x9, y9 being Element of L ex s9 being Function of L,(InclPoset (Ids L)) st
( x9 = a & y9 = x & s9 = mp & x9 in s9 . y9 ) by A4;
hence a in mp . x ; :: thesis: verum

end;

mp . x c= AR -below x

proof

let a be object ; :: according to TARSKI:def 3 :: thesis: ( not a in mp . x or a in AR -below x )
assume A7: a in mp . x ; :: thesis: a in AR -below x
then reconsider a9 = a as Element of L by A5;
[a9,x] in AR by A4, A7;
hence a in AR -below x ; :: thesis: verum

end;

hence x = sup (AR -below x) by A5, A6, XBOOLE_0:def 10; :: thesis: verum

end;

then reconsider AR = AR as auxiliary approximating Relation of L by Def17;
take AR ; :: thesis: AR = (Map2Rel L) . mp
thus AR = (Map2Rel L) . mp by A3; :: thesis: verum