let L be non empty Poset; :: thesis: ( dom (SupMap L) = Ids L & rng (SupMap L) is Subset of L )
set P = InclPoset (Ids L);
thus dom (SupMap L) = the carrier of (InclPoset (Ids L)) by FUNCT_2:def 1
.= the carrier of RelStr(# (Ids L),(RelIncl (Ids L)) #) by YELLOW_1:def 1
.= Ids L ; :: thesis: rng (SupMap L) is Subset of L
thus rng (SupMap L) is Subset of L ; :: thesis: verum