let I be non empty set ; :: thesis: for A being 1-sorted-yielding non-Empty ManySortedSet of I
for B being Element of Carrier A holds {B} is ManySortedSubset of Carrier A
let A be 1-sorted-yielding non-Empty ManySortedSet of I; :: thesis: for B being Element of Carrier A holds {B} is ManySortedSubset of Carrier A
let B be Element of Carrier A; :: thesis: {B} is ManySortedSubset of Carrier A
{B} c= Carrier A

proof

let i be object ; :: according to PBOOLE:def 2 :: thesis: ( not i in I or {B} . i c= (Carrier A) . i )
assume A1: i in I ; :: thesis: {B} . i c= (Carrier A) . i
then reconsider j = i as Element of I ;
j in dom A by A1, PARTFUN1:def 2;
then A . j in rng A by FUNCT_1:def 3;
then A2: not A . j is empty by YELLOW_6:def 2;
B . j is Element of (Carrier A) . j by PBOOLE:def 14;
then B . j is Element of (A . j) by YELLOW_6:2;
then {(B . j)} c= the carrier of (A . j) by A2, ZFMISC_1:31;
then {B} . j c= the carrier of (A . j) by PZFMISC1:def 1;
hence {B} . i c= (Carrier A) . i by YELLOW_6:2; :: thesis: verum

end;

hence {B} is ManySortedSubset of Carrier A by PBOOLE:def 18; :: thesis: verum