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 Th50;
consider d being Element of OTS such that
A1: ( a,b // c,d or a,b // d,c ) by Def14;
reconsider d9 = d as Element of (Lambda OTS) by Th50;
take d9 ; :: thesis: a9,b9 // c9,d9
thus a9,b9 // c9,d9 by A1, Th51; :: thesis: verum