let OTS be OrdTrapSpace; :: thesis: for a9, b9, c9, d9 being Element of (Lambda OTS) st a9,b9 // c9,d9 holds
c9,d9 // a9,b9
let a9, b9, c9, d9 be Element of (Lambda OTS); :: thesis: ( a9,b9 // c9,d9 implies c9,d9 // a9,b9 )
reconsider a = a9, b = b9, c = c9, d = d9 as Element of the carrier of OTS by Th47;
assume A1: a9,b9 // c9,d9 ; :: thesis: c9,d9 // a9,b9
per cases ( a,b // c,d or a,b // d,c ) by A1, Th48;
suppose a,b // c,d ; :: thesis: c9,d9 // a9,b9
then c,d // a,b by Def12;
hence c9,d9 // a9,b9 by Th48; :: thesis: verum
end;
suppose a,b // d,c ; :: thesis: c9,d9 // a9,b9
then b,a // c,d by Def12;
then c,d // b,a by Def12;
hence c9,d9 // a9,b9 by Th48; :: thesis: verum
end;
end;