let L be non empty reflexive transitive RelStr ; :: thesis: for S being non empty full SubRelStr of L holds
( dom (supMap S) = Ids S & rng (supMap S) is Subset of L )
let S be non empty full SubRelStr of L; :: thesis: ( dom (supMap S) = Ids S & rng (supMap S) is Subset of L )
set P = InclPoset (Ids S);
thus dom (supMap S) = the carrier of (InclPoset (Ids S)) by FUNCT_2:def 1
.= the carrier of RelStr(# (Ids S),(RelIncl (Ids S)) #) by YELLOW_1:def 1
.= Ids S ; :: thesis: rng (supMap S) is Subset of L
thus rng (supMap S) is Subset of L ; :: thesis: verum