let OTS be OrdTrapSpace; :: thesis: Lambda OTS is TrapSpace-like
set TS = Lambda OTS;
let a', b', c', d', p', q' be Element of ; :: 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 st a',b' // c',x' )
thus a',b' // b',a' by Lm42; :: thesis: ( ( 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 st a',b' // c',x' )
thus ( a',b' // c',d' & a',b' // c',q' & not a' = b' implies d' = q' ) by Lm40; :: thesis: ( ( 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 st a',b' // c',x' )
thus ( p' <> q' & p',q' // a',b' & p',q' // c',d' implies a',b' // c',d' ) by Lm39; :: thesis: ( ( a',b' // c',d' implies c',d' // a',b' ) & ex x' being Element of st a',b' // c',x' )
thus ( a',b' // c',d' implies c',d' // a',b' ) by Lm38; :: thesis: ex x' being Element of st a',b' // c',x'
thus ex x' being Element of st a',b' // c',x' by Lm37; :: thesis: verum