let OTS be OrdTrapSpace; :: thesis: for a, b being Element of OTS holds a,b // a,b
let a, b be Element of OTS; :: thesis: a,b // a,b
consider c being Element of OTS such that
A1: ( a,b // a,c or a,b // c,a ) by Def14;

A2: now

assume A3: a,b // c,a ; :: thesis: a,b // a,b
then c,a // a,b by Def14;
then ( c = a & a = b ) by Def14;
hence a,b // a,b by A3; :: thesis: verum

end;

now

assume A4: a,b // a,c ; :: thesis: a,b // a,b

A5: now

assume A6: a <> c ; :: thesis: a,b // a,b
a,c // a,b by A4, Def14;
hence a,b // a,b by A6, Def14; :: thesis: verum

end;

now

assume a = c ; :: thesis: a,b // a,b
then a,a // a,b by A4, Def14;
hence a,b // a,b by Def14; :: thesis: verum

end;

hence a,b // a,b by A5; :: thesis: verum

end;

hence a,b // a,b by A1, A2; :: thesis: verum