let A be Preorder; :: thesis: the InternalRel of (QuotientOrder A) = <=E A

per cases ( A is empty or not A is empty ) ;

suppose A is empty ; :: thesis: the InternalRel of (QuotientOrder A) = <=E A

then ( the InternalRel of (QuotientOrder A) is empty & <=E A is empty ) ;
hence the InternalRel of (QuotientOrder A) = <=E A ; :: thesis: verum

end;

suppose not A is empty ; :: thesis: the InternalRel of (QuotientOrder A) = <=E A

then 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); :: thesis: ( [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) ; :: thesis: [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; :: thesis: 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); :: thesis: ( [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 ; :: thesis: [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; :: thesis: verum

end;

hence the InternalRel of (QuotientOrder A) = <=E A by A4, RELSET_1:def 1; :: thesis: verum

end;

end;