let x be set ; :: thesis: for L being non empty Poset holds
( x in dom (SupMap L) iff x is Ideal of L )
let L be non empty Poset; :: thesis: ( x in dom (SupMap L) iff x is Ideal of L )

hereby :: thesis: ( x is Ideal of L implies x in dom (SupMap L) )

assume x in dom (SupMap L) ; :: thesis: x is Ideal of L
then x in Ids L by Th51;
then ex I being Ideal of L st x = I ;
hence x is Ideal of L ; :: thesis: verum

end;

assume x is Ideal of L ; :: thesis: x in dom (SupMap L)
then x in { X where X is Ideal of L : verum } ;
hence x in dom (SupMap L) by Th51; :: thesis: verum