let A be Preorder; the InternalRel of (QuotientOrder A) = <=E A
per cases
( A is empty or not A is empty )
;
suppose
not
A is
empty
;
the InternalRel of (QuotientOrder A) = <=E Athen reconsider B =
A as non
empty Preorder ;
set qa =
QuotientOrder B;
set int = the
InternalRel of
(QuotientOrder B);
A1:
for
x being
Element of
B holds
Class (
(EqRelOf B),
x)
= Class (
(EqRel B),
x)
by Th41;
for
X,
Y being
Element of
(QuotientOrder B) st
[X,Y] in the
InternalRel of
(QuotientOrder B) holds
[X,Y] in <=E B
proof
let X,
Y be
Element of
(QuotientOrder B);
( [X,Y] in the InternalRel of (QuotientOrder B) implies [X,Y] in <=E B )
(
X in the
carrier of
(QuotientOrder B) &
Y in the
carrier of
(QuotientOrder B) )
;
then A2:
(
X in Class (EqRelOf B) &
Y in Class (EqRelOf B) )
by Def7;
assume
[X,Y] in the
InternalRel of
(QuotientOrder B)
;
[X,Y] in <=E B
then consider x,
y being
Element of
B such that A3:
(
X = Class (
(EqRelOf B),
x) &
Y = Class (
(EqRelOf B),
y) &
x <= y )
by A2, Def7;
(
X = Class (
(EqRel B),
x) &
Y = Class (
(EqRel B),
y) &
x <= y )
by A1, A3;
hence
[X,Y] in <=E B
by DICKSON:def 5;
verum
end; then A4:
the
InternalRel of
(QuotientOrder B) c= <=E B
by RELSET_1:def 1;
for
X,
Y being
Element of
Class (EqRel B) st
[X,Y] in <=E B holds
[X,Y] in the
InternalRel of
(QuotientOrder B)
proof
let X,
Y be
Element of
Class (EqRel B);
( [X,Y] in <=E B implies [X,Y] in the InternalRel of (QuotientOrder B) )
(
X in Class (EqRel B) &
Y in Class (EqRel B) )
;
then A5:
(
X in Class (EqRelOf B) &
Y in Class (EqRelOf B) )
by Th41;
assume
[X,Y] in <=E B
;
[X,Y] in the InternalRel of (QuotientOrder B)
then consider x,
y being
Element of
B such that A6:
(
X = Class (
(EqRel B),
x) &
Y = Class (
(EqRel B),
y) &
x <= y )
by DICKSON:def 5;
(
X = Class (
(EqRelOf B),
x) &
Y = Class (
(EqRelOf B),
y) &
x <= y )
by A1, A6;
hence
[X,Y] in the
InternalRel of
(QuotientOrder B)
by A5, Def7;
verum
end; hence
the
InternalRel of
(QuotientOrder A) = <=E A
by A4, RELSET_1:def 1;
verum end;