defpred S₁[ 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 & S₁[x,y] ) ) from RELSET_1:sch 1();
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 ORDERS_2:1, ORDERS_2:def 5;
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 A2, ORDERS_1:12;
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 A4, RELAT_2:def 3, RELAT_2:def 11; :: 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 A12, A1;
A15: ( [y,z] in the InternalRel of A & [z,y] in the InternalRel of A ) by A13, A1;
A16: [x,z] in the InternalRel of A by A9, A10, A11, A14, A15, RELAT_2:def 8, ORDERS_2:def 3;
[z,x] in the InternalRel of A by A9, A10, A11, A14, A15, RELAT_2:def 8, ORDERS_2:def 3;
hence [x,z] in eq by A9, A11, A16, A1; :: thesis: verum

end;

hence eq is transitive by A4, RELAT_2:def 8, RELAT_2:def 16; :: 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 A17, RELAT_1:15;
hence [x,y] in eq by A17, A1; :: thesis: verum

end;

hence for x, y being Element of A holds
( [x,y] in eq iff ( x <= y & y <= x ) ) ; :: thesis: verum