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

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

end;

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;hence the InternalRel of (QuotientOrder A) = <=E A ; :: thesis: verum

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

for X, Y being Element of Class (EqRel B) st [X,Y] in <=E B holds

[X,Y] in the InternalRel of (QuotientOrder B)

end;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

then A4:
the InternalRel of (QuotientOrder B) c= <=E B
by RELSET_1:def 1;
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;( 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

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

hence
the InternalRel of (QuotientOrder A) = <=E A
by A4, RELSET_1:def 1; :: thesis: verum
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;( 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