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 RELSET_1:sch 1();
A2:
eq is total
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 ;
( 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
;
[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;
verum
end;
hence
eq is
symmetric
by A4, RELAT_2:def 3, RELAT_2:def 11;
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 ;
( 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
;
[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;
verum
end;
hence
eq is
transitive
by A4, RELAT_2:def 8, RELAT_2:def 16;
verum
end;
reconsider eq = eq as Equivalence_Relation of the carrier of A by A2, A5, A8;
take
eq
; 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;
( [x,y] in eq iff ( x <= y & y <= x ) )
thus
(
[x,y] in eq implies (
x <= y &
y <= x ) )
( x <= y & y <= x implies [x,y] in eq )
assume
(
x <= y &
y <= x )
;
[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;
verum
end;
hence
for x, y being Element of A holds
( [x,y] in eq iff ( x <= y & y <= x ) )
; verum