let OTS be OrdTrapSpace; :: thesis: for a9, b9 being Element of (Lambda OTS) holds a9,b9 // b9,a9
let a9, b9 be Element of (Lambda OTS); :: thesis: a9,b9 // b9,a9
reconsider a = a9, b = b9 as Element of OTS by Th47;
a,b // a,b by Lm41;
hence a9,b9 // b9,a9 by Th48; :: thesis: verum