let L be non empty up-complete Poset; :: thesis:
let S be non empty full SubRelStr of L; :: thesis:

A1: now :: thesis:

let x be object ; :: thesis:
thus ( x in dom (supMap S) implies ( x in dom (idsMap S) & (idsMap S) . x in dom (SupMap L) ) ) :: thesis:

assume x in dom (supMap S) ; :: thesis:
then x is Ideal of S by Th52;
hence x in dom (idsMap S) by Th54; :: thesis:
then (idsMap S) . x in rng (idsMap S) by FUNCT_1:def 3;
then (idsMap S) . x is Ideal of L by Th55;
hence (idsMap S) . x in dom (SupMap L) by YELLOW_2:50; :: thesis:

end;

thus ( x in dom (idsMap S) & (idsMap S) . x in dom (SupMap L) implies x in dom (supMap S) ) :: thesis:

assume that
A2: x in dom (idsMap S) and
(idsMap S) . x in dom (SupMap L) ; :: thesis:
x is Ideal of S by A2, Th54;
hence x in dom (supMap S) by Th52; :: thesis:

end;

end;

let x be object ; :: thesis:
assume x in dom (supMap S) ; :: thesis:
then reconsider I = x as Ideal of S by Th52;
consider J being Subset of L such that
A3: I = J and
A4: (idsMap S) . I = downarrow J by Def11;
reconsider J = J as non empty directed Subset of L by A3, YELLOW_2:7;
A5: ex_sup_of J,L by WAYBEL_0:75;
thus (supMap S) . x = "\/" (I,L) by Def10
.= sup (downarrow J) by A3, A5, WAYBEL_0:33
.= (SupMap L) . ((idsMap S) . x) by A4, YELLOW_2:def 3 ; :: thesis:

end;

hence supMap S = (SupMap L) * (idsMap S) by A1, FUNCT_1:10; :: thesis: