theorem Th2: :: FUNCT_5:8

( proj1 {} = {} & proj2 {} = {} ) ;