let OTS be OrdTrapSpace; :: thesis: for a', b' being Element of holds a',b' // b',a'
let a', b' be Element of ; :: thesis: a',b' // b',a'
reconsider a = a', b = b' as Element of by Th50;
a,b // a,b by Lm41;
hence a',b' // b',a' by Th51; :: thesis: verum