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;