let D1 be non empty set ; :: thesis: for D2 being set
for k being Element of D1 holds [:{k},D2:] c= [:D1,D2:]
let D2 be set ; :: thesis: for k being Element of D1 holds [:{k},D2:] c= [:D1,D2:]
let k be Element of D1; :: thesis: [:{k},D2:] c= [:D1,D2:]
{k} is Subset of D1 by SUBSET_1:41;
hence [:{k},D2:] c= [:D1,D2:] by ZFMISC_1:95; :: thesis: verum