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