let L be non empty reflexive transitive RelStr ; :: thesis: for S being non empty full SubRelStr of L holds

( dom (idsMap S) = Ids S & rng (idsMap S) is Subset of (Ids L) )

let S be non empty full SubRelStr of L; :: thesis: ( dom (idsMap S) = Ids S & rng (idsMap S) is Subset of (Ids L) )

set P = InclPoset (Ids S);

thus dom (idsMap 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 (idsMap S) is Subset of (Ids L)

thus rng (idsMap S) is Subset of (Ids L) by YELLOW_1:1; :: thesis: verum

( dom (idsMap S) = Ids S & rng (idsMap S) is Subset of (Ids L) )

let S be non empty full SubRelStr of L; :: thesis: ( dom (idsMap S) = Ids S & rng (idsMap S) is Subset of (Ids L) )

set P = InclPoset (Ids S);

thus dom (idsMap 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 (idsMap S) is Subset of (Ids L)

thus rng (idsMap S) is Subset of (Ids L) by YELLOW_1:1; :: thesis: verum