let L be non empty up-complete Poset; :: thesis: for S being non empty full SubRelStr of L holds supMap S = () * ()
let S be non empty full SubRelStr of L; :: thesis: supMap S = () * ()
A1: now :: thesis: for x being object holds
( ( x in dom () implies ( x in dom () & () . x in dom () ) ) & ( x in dom () & () . x in dom () implies x in dom () ) )
let x be object ; :: thesis: ( ( x in dom () implies ( x in dom () & () . x in dom () ) ) & ( x in dom () & () . x in dom () implies x in dom () ) )
thus ( x in dom () implies ( x in dom () & () . x in dom () ) ) :: thesis: ( x in dom () & () . x in dom () implies x in dom () )
proof
assume x in dom () ; :: thesis: ( x in dom () & () . x in dom () )
then x is Ideal of S by Th52;
hence x in dom () by Th54; :: thesis: () . x in dom ()
then (idsMap S) . x in rng () by FUNCT_1:def 3;
then (idsMap S) . x is Ideal of L by Th55;
hence (idsMap S) . x in dom () by YELLOW_2:50; :: thesis: verum
end;
thus ( x in dom () & () . x in dom () implies x in dom () ) :: thesis: verum
proof
assume that
A2: x in dom () and
(idsMap S) . x in dom () ; :: thesis: x in dom ()
x is Ideal of S by ;
hence x in dom () by Th52; :: thesis: verum
end;
end;
now :: thesis: for x being object st x in dom () holds
() . x = () . (() . x)
let x be object ; :: thesis: ( x in dom () implies () . x = () . (() . x) )
assume x in dom () ; :: thesis: () . x = () . (() . 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 ;
A5: ex_sup_of J,L by WAYBEL_0:75;
thus () . x = "\/" (I,L) by Def10
.= sup () by
.= () . (() . x) by ; :: thesis: verum
end;
hence supMap S = () * () by ; :: thesis: verum