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 & 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 R' = R as non empty RelStr ;
set IT = { [(Class (EqRel R),a),(Class (EqRel R),b)] where a, b is Element of R' : a <= b } ;
set Y = Class (EqRel R);
{ [(Class (EqRel R),a),(Class (EqRel R),b)] where a, b is Element of R' : 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 R' : 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 R' : a <= b } ; :: thesis: x in [:(Class (EqRel R)),(Class (EqRel R)):]
then consider a, b being Element of R' such that
A3: x = [(Class (EqRel R),a),(Class (EqRel R),b)] and
a <= b ;
( Class (EqRel R),a in Class (EqRel R) & Class (EqRel R),b in Class (EqRel R) ) by EQREL_1:def 5;
hence x in [:(Class (EqRel R)),(Class (EqRel R)):] by A3, ZFMISC_1:def 2; :: thesis: verum

end;

then reconsider IT = { [(Class (EqRel R),a),(Class (EqRel R),b)] where a, b is Element of R' : 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 a', b' being Element of R st
( A = Class (EqRel R),a' & B = Class (EqRel R),b' & a' <= b' )
then consider a, b being Element of R such that
A4: [A,B] = [(Class (EqRel R),a),(Class (EqRel R),b)] and
A5: a <= b ;
reconsider a' = a, b' = b as Element of R ;
take a' = a'; :: thesis: ex b' being Element of R st
( A = Class (EqRel R),a' & B = Class (EqRel R),b' & a' <= b' )
take b' = b'; :: thesis: ( A = Class (EqRel R),a' & B = Class (EqRel R),b' & a' <= b' )
thus ( A = Class (EqRel R),a' & B = Class (EqRel R),b' & a' <= b' ) by A4, A5, ZFMISC_1:33; :: thesis: verum

end;

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

end;

end;