let OTS be OrdTrapSpace; :: thesis: Lambda OTS is TrapSpace-like
set TS = Lambda OTS;
let a9, b9, c9, d9, p9, q9 be Element of (Lambda OTS); :: according to GEOMTRAP:def 14 :: thesis: ( a9,b9 // b9,a9 & ( a9,b9 // c9,d9 & a9,b9 // c9,q9 & not a9 = b9 implies d9 = q9 ) & ( p9 <> q9 & p9,q9 // a9,b9 & p9,q9 // c9,d9 implies a9,b9 // c9,d9 ) & ( a9,b9 // c9,d9 implies c9,d9 // a9,b9 ) & ex x9 being Element of (Lambda OTS) st a9,b9 // c9,x9 )
thus a9,b9 // b9,a9 by Lm42; :: thesis: ( ( a9,b9 // c9,d9 & a9,b9 // c9,q9 & not a9 = b9 implies d9 = q9 ) & ( p9 <> q9 & p9,q9 // a9,b9 & p9,q9 // c9,d9 implies a9,b9 // c9,d9 ) & ( a9,b9 // c9,d9 implies c9,d9 // a9,b9 ) & ex x9 being Element of (Lambda OTS) st a9,b9 // c9,x9 )
thus ( a9,b9 // c9,d9 & a9,b9 // c9,q9 & not a9 = b9 implies d9 = q9 ) by Lm40; :: thesis: ( ( p9 <> q9 & p9,q9 // a9,b9 & p9,q9 // c9,d9 implies a9,b9 // c9,d9 ) & ( a9,b9 // c9,d9 implies c9,d9 // a9,b9 ) & ex x9 being Element of (Lambda OTS) st a9,b9 // c9,x9 )
thus ( p9 <> q9 & p9,q9 // a9,b9 & p9,q9 // c9,d9 implies a9,b9 // c9,d9 ) by Lm39; :: thesis: ( ( a9,b9 // c9,d9 implies c9,d9 // a9,b9 ) & ex x9 being Element of (Lambda OTS) st a9,b9 // c9,x9 )
thus ( a9,b9 // c9,d9 implies c9,d9 // a9,b9 ) by Lm38; :: thesis: ex x9 being Element of (Lambda OTS) st a9,b9 // c9,x9
thus ex x9 being Element of (Lambda OTS) st a9,b9 // c9,x9 by Lm37; :: thesis: verum