set car = Class ();
defpred S1[ object , object ] means ex x, y being Element of A st
( \$1 = Class ((),x) & \$2 = Class ((),y) & x <= y );
consider rel being Relation of (Class ()) such that
A1: for X, Y being object holds
( [X,Y] in rel iff ( X in Class () & Y in Class () & S1[X,Y] ) ) from set order = RelStr(# (Class ()),rel #);
take RelStr(# (Class ()),rel #) ; :: thesis: ( the carrier of RelStr(# (Class ()),rel #) = Class () & ( for X, Y being Element of Class () holds
( [X,Y] in the InternalRel of RelStr(# (Class ()),rel #) iff ex x, y being Element of A st
( X = Class ((),x) & Y = Class ((),y) & x <= y ) ) ) )

thus the carrier of RelStr(# (Class ()),rel #) = Class () ; :: thesis: for X, Y being Element of Class () holds
( [X,Y] in the InternalRel of RelStr(# (Class ()),rel #) iff ex x, y being Element of A st
( X = Class ((),x) & Y = Class ((),y) & x <= y ) )

let X, Y be Element of Class (); :: thesis: ( [X,Y] in the InternalRel of RelStr(# (Class ()),rel #) iff ex x, y being Element of A st
( X = Class ((),x) & Y = Class ((),y) & x <= y ) )

thus ( [X,Y] in the InternalRel of RelStr(# (Class ()),rel #) implies ex x, y being Element of A st
( X = Class ((),x) & Y = Class ((),y) & x <= y ) ) by A1; :: thesis: ( ex x, y being Element of A st
( X = Class ((),x) & Y = Class ((),y) & x <= y ) implies [X,Y] in the InternalRel of RelStr(# (Class ()),rel #) )

given x, y being Element of A such that A2: ( X = Class ((),x) & Y = Class ((),y) ) and
A3: x <= y ; :: thesis: [X,Y] in the InternalRel of RelStr(# (Class ()),rel #)
the carrier of A \/ the carrier of A = the carrier of A ;
then A4: field the InternalRel of A c= the carrier of A by RELSET_1:8;
[x,y] in the InternalRel of A by ;
then ( x in field the InternalRel of A & y in field the InternalRel of A ) by RELAT_1:15;
then ( X in Class () & Y in Class () ) by ;
hence [X,Y] in the InternalRel of RelStr(# (Class ()),rel #) by A1, A2, A3; :: thesis: verum