set car = Class (EqRelOf A);
defpred S₁[ object , object ] means ex x, y being Element of A st
( $1 = Class ((EqRelOf A),x) & $2 = Class ((EqRelOf A),y) & x <= y );
consider rel being Relation of (Class (EqRelOf A)) such that
A1: for X, Y being object holds
( [X,Y] in rel iff ( X in Class (EqRelOf A) & Y in Class (EqRelOf A) & S₁[X,Y] ) ) from RELSET_1:sch 1();
set order = RelStr(# (Class (EqRelOf A)),rel #);
take RelStr(# (Class (EqRelOf A)),rel #) ; :: thesis: ( the carrier of RelStr(# (Class (EqRelOf A)),rel #) = Class (EqRelOf A) & ( for X, Y being Element of Class (EqRelOf A) holds
( [X,Y] in the InternalRel of RelStr(# (Class (EqRelOf A)),rel #) iff ex x, y being Element of A st
( X = Class ((EqRelOf A),x) & Y = Class ((EqRelOf A),y) & x <= y ) ) ) )
thus the carrier of RelStr(# (Class (EqRelOf A)),rel #) = Class (EqRelOf A) ; :: thesis: for X, Y being Element of Class (EqRelOf A) holds
( [X,Y] in the InternalRel of RelStr(# (Class (EqRelOf A)),rel #) iff ex x, y being Element of A st
( X = Class ((EqRelOf A),x) & Y = Class ((EqRelOf A),y) & x <= y ) )
let X, Y be Element of Class (EqRelOf A); :: thesis: ( [X,Y] in the InternalRel of RelStr(# (Class (EqRelOf A)),rel #) iff ex x, y being Element of A st
( X = Class ((EqRelOf A),x) & Y = Class ((EqRelOf A),y) & x <= y ) )
thus ( [X,Y] in the InternalRel of RelStr(# (Class (EqRelOf A)),rel #) implies ex x, y being Element of A st
( X = Class ((EqRelOf A),x) & Y = Class ((EqRelOf A),y) & x <= y ) ) by A1; :: thesis: ( ex x, y being Element of A st
( X = Class ((EqRelOf A),x) & Y = Class ((EqRelOf A),y) & x <= y ) implies [X,Y] in the InternalRel of RelStr(# (Class (EqRelOf A)),rel #) )
given x, y being Element of A such that A2: ( X = Class ((EqRelOf A),x) & Y = Class ((EqRelOf A),y) ) and
A3: x <= y ; :: thesis: [X,Y] in the InternalRel of RelStr(# (Class (EqRelOf A)),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 A3, ORDERS_2:def 5;
then ( x in field the InternalRel of A & y in field the InternalRel of A ) by RELAT_1:15;
then ( X in Class (EqRelOf A) & Y in Class (EqRelOf A) ) by A2, A4, EQREL_1:def 3;
hence [X,Y] in the InternalRel of RelStr(# (Class (EqRelOf A)),rel #) by A1, A2, A3; :: thesis: verum