theorem Th1: :: TOPREAL3:1

for x, y, z being object holds
( 1 in dom <*x,y,z*> & 2 in dom <*x,y,z*> & 3 in dom <*x,y,z*> )