theorem Th47: :: GEOMTRAP:47

for OTS being OrdTrapSpace
for x being set holds
( x is Element of OTS iff x is Element of (Lambda OTS) )