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 A1: ( mp is approximating & mp in the carrier of (MonSet L) ) ; :: thesis: ex AR being auxiliary approximating Relation of L st AR = (Map2Rel L) . mp
then consider AR being auxiliary Relation of L such that
A2: ( AR = (Map2Rel L) . mp & ( for x, y being set holds
( [x,y] in AR iff ex x', y' being Element of L ex s' being Function of L,(InclPoset (Ids L)) st
( x' = x & y' = y & s' = mp & x' in s' . y' ) ) ) ) by Def16;

now

let x be Element of L; :: thesis: x = sup (AR -below x)
consider ii being Subset of L such that
A3: ( ii = mp . x & x = sup ii ) by A1, Def19;
AR -below x = mp . x

proof

thus AR -below x c= mp . x :: according to XBOOLE_0:def 10 :: thesis: mp . x c= AR -below x

proof

let a be set ; :: 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 consider x', y' being Element of L, s' being Function of L,(InclPoset (Ids L)) such that
A4: ( x' = a & y' = x & s' = mp & x' in s' . y' ) by A2;
thus a in mp . x by A4; :: thesis: verum

end;

thus mp . x c= AR -below x :: thesis: verum

proof

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

end;

end;

hence x = sup (AR -below x) by A3; :: thesis: verum

end;

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