theorem Th02: :: ANPROJ10:5

for X being non empty set holds 4 -tuples_on X = { <*d1,d2,d3,d4*> where d1, d2, d3, d4 is Element of X : verum }