let OTS be OrdTrapSpace; :: thesis: 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); :: thesis: 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 ; :: thesis: a9,b9 // c9,d9
thus a9,b9 // c9,d9 by A1, Th48; :: thesis: verum