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