let D1 be non empty set ; for D2 being set
for k1, k2, k3 being Element of D1 holds [:{k1,k2,k3},D2:] c= [:D1,D2:]
let D2 be set ; for k1, k2, k3 being Element of D1 holds [:{k1,k2,k3},D2:] c= [:D1,D2:]
let k1, k2, k3 be Element of D1; [:{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; verum