set IR = the InternalRel of R;
set CR = the carrier of R;

per cases ( the carrier of R = {} or not the carrier of R is empty ) ;

suppose A1: the carrier of R = {} ; :: thesis: ex b₁ being Relation of (Class (EqRel R)) st
for A, B being set holds
( [A,B] in b₁ iff ex a, b being Element of R st
( A = Class (EqRel R),a & B = Class (EqRel R),b & a <= b ) )

reconsider IT = {} as Relation of (Class (EqRel R)) by RELSET_1:25;
take IT ; :: thesis: for A, B being set holds
( [A,B] in IT iff ex a, b being Element of R st
( A = Class (EqRel R),a & B = Class (EqRel R),b & a <= b ) )
let A, B be set ; :: thesis: ( [A,B] in IT iff ex a, b being Element of R st
( A = Class (EqRel R),a & B = Class (EqRel R),b & a <= b ) )
thus ( [A,B] in IT implies ex a, b being Element of R st
( A = Class (EqRel R),a & B = Class (EqRel R),b & a <= b ) ) ; :: thesis: ( ex a, b being Element of R st
( A = Class (EqRel R),a & B = Class (EqRel R),b & a <= b ) implies [A,B] in IT )
given a, b being Element of R such that A = Class (EqRel R),a and
B = Class (EqRel R),b and
A2: a <= b ; :: thesis: [A,B] in IT
the InternalRel of R = {} by A1;
hence [A,B] in IT by A2, ORDERS_2:def 9; :: thesis: verum

end;

suppose not the carrier of R is empty ; :: thesis: ex b₁ being Relation of (Class (EqRel R)) st
for A, B being set holds
( [A,B] in b₁ iff ex a, b being Element of R st
( A = Class (EqRel R),a & B = Class (EqRel R),b & a <= b ) )

then reconsider R9 = R as non empty RelStr ;
set IT = { [(Class (EqRel R),a),(Class (EqRel R),b)] where a, b is Element of R9 : a <= b } ;
set Y = Class (EqRel R);
{ [(Class (EqRel R),a),(Class (EqRel R),b)] where a, b is Element of R9 : a <= b } c= [:(Class (EqRel R)),(Class (EqRel R)):]

proof

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in { [(Class (EqRel R),a),(Class (EqRel R),b)] where a, b is Element of R9 : a <= b } or x in [:(Class (EqRel R)),(Class (EqRel R)):] )
assume x in { [(Class (EqRel R),a),(Class (EqRel R),b)] where a, b is Element of R9 : a <= b } ; :: thesis: x in [:(Class (EqRel R)),(Class (EqRel R)):]
then consider a, b being Element of R9 such that
A3: x = [(Class (EqRel R),a),(Class (EqRel R),b)] and
a <= b ;
A4: Class (EqRel R),a in Class (EqRel R) by EQREL_1:def 5;
Class (EqRel R),b in Class (EqRel R) by EQREL_1:def 5;
hence x in [:(Class (EqRel R)),(Class (EqRel R)):] by A3, A4, ZFMISC_1:def 2; :: thesis: verum

end;

then reconsider IT = { [(Class (EqRel R),a),(Class (EqRel R),b)] where a, b is Element of R9 : a <= b } as Relation of (Class (EqRel R)) ;
take IT ; :: thesis: for A, B being set holds
( [A,B] in IT iff ex a, b being Element of R st
( A = Class (EqRel R),a & B = Class (EqRel R),b & a <= b ) )
let A, B be set ; :: thesis: ( [A,B] in IT iff ex a, b being Element of R st
( A = Class (EqRel R),a & B = Class (EqRel R),b & a <= b ) )

hereby :: thesis: ( ex a, b being Element of R st
( A = Class (EqRel R),a & B = Class (EqRel R),b & a <= b ) implies [A,B] in IT )

assume [A,B] in IT ; :: thesis: ex a9, b9 being Element of R st
( A = Class (EqRel R),a9 & B = Class (EqRel R),b9 & a9 <= b9 )
then consider a, b being Element of R such that
A5: [A,B] = [(Class (EqRel R),a),(Class (EqRel R),b)] and
A6: a <= b ;
reconsider a9 = a, b9 = b as Element of R ;
take a9 = a9; :: thesis: ex b9 being Element of R st
( A = Class (EqRel R),a9 & B = Class (EqRel R),b9 & a9 <= b9 )
take b9 = b9; :: thesis: ( A = Class (EqRel R),a9 & B = Class (EqRel R),b9 & a9 <= b9 )
thus ( A = Class (EqRel R),a9 & B = Class (EqRel R),b9 & a9 <= b9 ) by A5, A6, ZFMISC_1:33; :: thesis: verum

end;

given a, b being Element of R such that A7: A = Class (EqRel R),a and
A8: B = Class (EqRel R),b and
A9: a <= b ; :: thesis: [A,B] in IT
thus [A,B] in IT by A7, A8, A9; :: thesis: verum

end;

end;