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 Def12;

per cases ( a,b // c,a or a,b // a,c ) by A1;

suppose a,b // c,a ; :: thesis: a,b // a,b

then A2: c,a // a,b by Def12;
then c = a by Def12;
hence a,b // a,b by A2, Def12; :: thesis: verum

end;

suppose A3: a,b // a,c ; :: thesis: a,b // a,b

per cases ( a <> c or a = c ) ;

suppose A4: a <> c ; :: thesis: a,b // a,b

a,c // a,b by A3, Def12;
hence a,b // a,b by A4, Def12; :: thesis: verum

end;

suppose a = c ; :: thesis: a,b // a,b

then a,a // a,b by A3, Def12;
hence a,b // a,b by Def12; :: thesis: verum

end;

end;

end;

end;