let L be non empty up-complete Poset; :: thesis: for S being non empty full SubRelStr of L holds supMap S = (SupMap L) * (idsMap S)
let S be non empty full SubRelStr of L; :: thesis: supMap S = (SupMap L) * (idsMap S)

A1: now :: thesis: for x being object holds
( ( x in dom (supMap S) implies ( x in dom (idsMap S) & (idsMap S) . x in dom (SupMap L) ) ) & ( x in dom (idsMap S) & (idsMap S) . x in dom (SupMap L) implies x in dom (supMap S) ) )

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

proof

assume x in dom (supMap S) ; :: thesis: ( x in dom (idsMap S) & (idsMap S) . x in dom (SupMap L) )
then x is Ideal of S by Th52;
hence x in dom (idsMap S) by Th54; :: thesis: (idsMap S) . x in dom (SupMap L)
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: verum

end;

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

proof

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

end;

end;

now :: thesis: for x being object st x in dom (supMap S) holds
(supMap S) . x = (SupMap L) . ((idsMap S) . x)

let x be object ; :: thesis: ( x in dom (supMap S) implies (supMap S) . x = (SupMap L) . ((idsMap S) . x) )
assume x in dom (supMap S) ; :: thesis: (supMap S) . x = (SupMap L) . ((idsMap S) . x)
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: verum

end;

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