theorem Th48: :: GEOMTRAP:48

for OTS being OrdTrapSpace
for a, b, c, d being Element of OTS
for a9, b9, c9, d9 being Element of (Lambda OTS) st a = a9 & b = b9 & c = c9 & d = d9 holds
( a9,b9 // c9,d9 iff ( a,b // c,d or a,b // d,c ) )