theorem :: QC_LANG1:1

for D1 being non empty set
for D2 being set
for k being Element of D1 holds [:{k},D2:] c= [:D1,D2:]