let OTS be OrdTrapSpace; for a9, b9, c9 being Element of (Lambda OTS) ex d9 being Element of (Lambda OTS) st a9,b9 // c9,d9
let a9, b9, c9 be Element of (Lambda OTS); ex d9 being Element of (Lambda OTS) st a9,b9 // c9,d9
reconsider a = a9, b = b9, c = c9 as Element of OTS by Th47;
consider d being Element of OTS such that
A1:
( a,b // c,d or a,b // d,c )
by Def12;
reconsider d9 = d as Element of (Lambda OTS) by Th47;
take
d9
; a9,b9 // c9,d9
thus
a9,b9 // c9,d9
by A1, Th48; verum