let R be RelStr ; ( R is quasi_ordered implies <=E R partially_orders Class (EqRel R) )
set CR = the carrier of R;
set IR = the InternalRel of R;
assume A1:
R is quasi_ordered
; <=E R partially_orders Class (EqRel R)
then
R is transitive
;
then A2:
the InternalRel of R is_transitive_in the carrier of R
;
thus
<=E R is_reflexive_in Class (EqRel R)
ORDERS_1:def 8 ( <=E R is_transitive_in Class (EqRel R) & <=E R is_antisymmetric_in Class (EqRel R) )
thus
<=E R is_transitive_in Class (EqRel R)
<=E R is_antisymmetric_in Class (EqRel R)proof
let x,
y,
z be
object ;
RELAT_2:def 8 ( not x in Class (EqRel R) or not y in Class (EqRel R) or not z in Class (EqRel R) or not [x,y] in <=E R or not [y,z] in <=E R or [x,z] in <=E R )
assume that A6:
x in Class (EqRel R)
and
y in Class (EqRel R)
and
z in Class (EqRel R)
and A7:
[x,y] in <=E R
and A8:
[y,z] in <=E R
;
[x,z] in <=E R
consider a,
b being
Element of
R such that A9:
x = Class (
(EqRel R),
a)
and A10:
y = Class (
(EqRel R),
b)
and A11:
a <= b
by A7, Def5;
consider c,
d being
Element of
R such that A12:
y = Class (
(EqRel R),
c)
and A13:
z = Class (
(EqRel R),
d)
and A14:
c <= d
by A8, Def5;
A15:
[a,b] in the
InternalRel of
R
by A11;
A16:
[c,d] in the
InternalRel of
R
by A14;
A17:
ex
x1 being
object st
(
x1 in the
carrier of
R &
x = Class (
(EqRel R),
x1) )
by A6, EQREL_1:def 3;
then
b in Class (
(EqRel R),
c)
by A10, A12, EQREL_1:23;
then
[b,c] in EqRel R
by EQREL_1:19;
then
[b,c] in the
InternalRel of
R /\ ( the InternalRel of R ~)
by A1, Def4;
then
[b,c] in the
InternalRel of
R
by XBOOLE_0:def 4;
then
[a,c] in the
InternalRel of
R
by A2, A15, A17;
then
[a,d] in the
InternalRel of
R
by A2, A16, A17;
then
a <= d
;
hence
[x,z] in <=E R
by A9, A13, Def5;
verum
end;
thus
<=E R is_antisymmetric_in Class (EqRel R)
verumproof
let x,
y be
object ;
RELAT_2:def 4 ( not x in Class (EqRel R) or not y in Class (EqRel R) or not [x,y] in <=E R or not [y,x] in <=E R or x = y )
assume that A18:
x in Class (EqRel R)
and
y in Class (EqRel R)
and A19:
[x,y] in <=E R
and A20:
[y,x] in <=E R
;
x = y
consider a,
b being
Element of
R such that A21:
x = Class (
(EqRel R),
a)
and A22:
y = Class (
(EqRel R),
b)
and A23:
a <= b
by A19, Def5;
consider c,
d being
Element of
R such that A24:
y = Class (
(EqRel R),
c)
and A25:
x = Class (
(EqRel R),
d)
and A26:
c <= d
by A20, Def5;
A27:
[a,b] in the
InternalRel of
R
by A23;
A28:
[c,d] in the
InternalRel of
R
by A26;
A29:
ex
x1 being
object st
(
x1 in the
carrier of
R &
x = Class (
(EqRel R),
x1) )
by A18, EQREL_1:def 3;
then A30:
d in Class (
(EqRel R),
a)
by A21, A25, EQREL_1:23;
a in Class (
(EqRel R),
a)
by A29, EQREL_1:20;
then A31:
[a,d] in EqRel R
by A30, EQREL_1:22;
A32:
c in Class (
(EqRel R),
b)
by A22, A24, A29, EQREL_1:23;
b in Class (
(EqRel R),
b)
by A29, EQREL_1:20;
then A33:
[b,c] in EqRel R
by A32, EQREL_1:22;
[a,d] in the
InternalRel of
R /\ ( the InternalRel of R ~)
by A1, A31, Def4;
then
[a,d] in the
InternalRel of
R ~
by XBOOLE_0:def 4;
then A34:
[d,a] in the
InternalRel of
R
by RELAT_1:def 7;
[b,c] in the
InternalRel of
R /\ ( the InternalRel of R ~)
by A1, A33, Def4;
then
[b,c] in the
InternalRel of
R
by XBOOLE_0:def 4;
then
[b,d] in the
InternalRel of
R
by A2, A28, A29;
then A35:
[b,a] in the
InternalRel of
R
by A2, A29, A34;
[b,a] in the
InternalRel of
R ~
by A27, RELAT_1:def 7;
then
[b,a] in the
InternalRel of
R /\ ( the InternalRel of R ~)
by A35, XBOOLE_0:def 4;
then
[b,a] in EqRel R
by A1, Def4;
then
b in Class (
(EqRel R),
a)
by EQREL_1:19;
hence
x = y
by A21, A22, EQREL_1:23;
verum
end;