Lambda OTS is TrapSpace-like

proof

let a', b', c', d', p', q' be Element of (Lambda OTS); :: according to GEOMTRAP:def 15 :: thesis: ( a',b' // b',a' & ( a',b' // c',d' & a',b' // c',q' & not a' = b' implies d' = q' ) & ( p' <> q' & p',q' // a',b' & p',q' // c',d' implies a',b' // c',d' ) & ( a',b' // c',d' implies c',d' // a',b' ) & ex x' being Element of (Lambda OTS) st a',b' // c',x' )
thus ( a',b' // b',a' & ( a',b' // c',d' & a',b' // c',q' & not a' = b' implies d' = q' ) & ( p' <> q' & p',q' // a',b' & p',q' // c',d' implies a',b' // c',d' ) & ( a',b' // c',d' implies c',d' // a',b' ) & ex x' being Element of (Lambda OTS) st a',b' // c',x' ) by Lm36, Lm37, Lm38, Lm39, Lm41; :: thesis: verum

end;

hence Lambda OTS is TrapSpace-like ; :: thesis: verum