defpred S_{1}[ 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_{1}[x,y] ) )
from RELSET_1:sch 1();

A2: eq is total

A5: eq is symmetric

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 ) )

( [x,y] in eq iff ( x <= y & y <= x ) ) ; :: thesis: verum

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

A2: eq is total

proof

A4:
field eq = the carrier of A
by A2, ORDERS_1:12;
for x being object st x in the carrier of A holds

x in dom eq

then dom eq = the carrier of A ;

hence eq is total by PARTFUN1:def 2; :: thesis: verum

end;x in dom eq

proof

then
the carrier of A c= dom eq
;
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;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

then dom eq = the carrier of A ;

hence eq is total by PARTFUN1:def 2; :: thesis: verum

A5: eq is symmetric

proof

A8:
eq is transitive
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

end;[y,x] in eq

proof

hence
eq is symmetric
by A4, RELAT_2:def 3, RELAT_2:def 11; :: thesis: verum
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;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

proof

reconsider eq = eq as Equivalence_Relation of the carrier of A by A2, A5, A8;
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

end;[x,z] in eq

proof

hence
eq is transitive
by A4, RELAT_2:def 8, RELAT_2:def 16; :: thesis: verum
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;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

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

hence
for x, y being Element of A holds
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 )

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;thus ( [x,y] in eq implies ( x <= y & y <= x ) ) :: thesis: ( x <= y & y <= x implies [x,y] in eq )

proof

assume
( x <= y & y <= x )
; :: thesis: [x,y] in eq
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;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

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

( [x,y] in eq iff ( x <= y & y <= x ) ) ; :: thesis: verum