defpred S1[ object , object ] means ( [\$1,\$2] in the InternalRel of A & [\$2,\$1] in the InternalRel of A );
consider eq being Relation of the carrier of A such that
A1: for x, y being object holds
( [x,y] in eq iff ( x in the carrier of A & y in the carrier of A & S1[x,y] ) ) from A2: eq is total
proof
for x being object st x in the carrier of A holds
x in dom eq
proof
let x be object ; :: thesis: ( x in the carrier of A implies x in dom eq )
assume A3: x in the carrier of A ; :: thesis: x in dom eq
then reconsider a = x as Element of A ;
not A is empty by A3;
then [a,a] in the InternalRel of A by ;
then [a,a] in eq by A3, A1;
hence x in dom eq by XTUPLE_0:def 12; :: thesis: verum
end;
then the carrier of A c= dom eq ;
then dom eq = the carrier of A ;
hence eq is total by PARTFUN1:def 2; :: thesis: verum
end;
A4: field eq = the carrier of A by ;
A5: eq is symmetric
proof
for x, y being object st x in the carrier of A & y in the carrier of A & [x,y] in eq holds
[y,x] in eq
proof
let x, y be object ; :: thesis: ( x in the carrier of A & y in the carrier of A & [x,y] in eq implies [y,x] in eq )
assume that
A6: ( x in the carrier of A & y in the carrier of A ) and
A7: [x,y] in eq ; :: thesis: [y,x] in eq
( [x,y] in the InternalRel of A & [y,x] in the InternalRel of A ) by A7, A1;
hence [y,x] in eq by A6, A1; :: thesis: verum
end;
hence eq is symmetric by ; :: thesis: verum
end;
A8: eq is transitive
proof
for x, y, z being object st x in the carrier of A & y in the carrier of A & z in the carrier of A & [x,y] in eq & [y,z] in eq holds
[x,z] in eq
proof
let x, y, z be object ; :: thesis: ( x in the carrier of A & y in the carrier of A & z in the carrier of A & [x,y] in eq & [y,z] in eq implies [x,z] in eq )
assume that
A9: x in the carrier of A and
A10: y in the carrier of A and
A11: z in the carrier of A and
A12: [x,y] in eq and
A13: [y,z] in eq ; :: thesis: [x,z] in eq
A14: ( [x,y] in the InternalRel of A & [y,x] in the InternalRel of A ) by ;
A15: ( [y,z] in the InternalRel of A & [z,y] in the InternalRel of A ) by ;
A16: [x,z] in the InternalRel of A by ;
[z,x] in the InternalRel of A by ;
hence [x,z] in eq by A9, A11, A16, A1; :: thesis: verum
end;
hence eq is transitive by ; :: thesis: verum
end;
reconsider eq = eq as Equivalence_Relation of the carrier of A by A2, A5, A8;
take eq ; :: thesis: for x, y being Element of A holds
( [x,y] in eq iff ( x <= y & y <= x ) )

for x, y being Element of A holds
( [x,y] in eq iff ( x <= y & y <= x ) )
proof
let x, y be Element of A; :: thesis: ( [x,y] in eq iff ( x <= y & y <= x ) )
thus ( [x,y] in eq implies ( x <= y & y <= x ) ) :: thesis: ( x <= y & y <= x implies [x,y] in eq )
proof
assume [x,y] in eq ; :: thesis: ( x <= y & y <= x )
then ( [x,y] in the InternalRel of A & [y,x] in the InternalRel of A ) by A1;
hence ( x <= y & y <= x ) by ORDERS_2:def 5; :: thesis: verum
end;
assume ( x <= y & y <= x ) ; :: thesis: [x,y] in eq
then A17: ( [x,y] in the InternalRel of A & [y,x] in the InternalRel of A ) by ORDERS_2:def 5;
field the InternalRel of A = the carrier of A by ORDERS_1:12;
then ( x in the carrier of A & y in the carrier of A ) by ;
hence [x,y] in eq by ; :: thesis: verum
end;
hence for x, y being Element of A holds
( [x,y] in eq iff ( x <= y & y <= x ) ) ; :: thesis: verum