let A be Order; :: thesis: EqRelOf A = id the carrier of A

per cases
( A is empty or not A is empty )
;

end;

suppose
not A is empty
; :: thesis: EqRelOf A = id the carrier of A

then reconsider B = A as non empty Order ;

defpred S_{1}[ set , set ] means $1 = $2;

A1: for x, y being Element of B holds

( [x,y] in EqRelOf B iff S_{1}[x,y] )

( [x,y] in id the carrier of B iff S_{1}[x,y] )
by RELAT_1:def 10;

thus EqRelOf A = EqRelOf B

.= id the carrier of B from RELSET_1:sch 4(A1, A2)

.= id the carrier of A ; :: thesis: verum

end;defpred S

A1: for x, y being Element of B holds

( [x,y] in EqRelOf B iff S

proof

A2:
for x, y being Element of B holds
let x, y be Element of B; :: thesis: ( [x,y] in EqRelOf B iff S_{1}[x,y] )

_{1}[x,y]
; :: thesis: [x,y] in EqRelOf B

then ( x <= y & y <= x ) ;

hence [x,y] in EqRelOf B by Def6; :: thesis: verum

end;hereby :: thesis: ( S_{1}[x,y] implies [x,y] in EqRelOf B )

assume
Sassume
[x,y] in EqRelOf B
; :: thesis: S_{1}[x,y]

then ( x <= y & y <= x ) by Def6;

hence S_{1}[x,y]
by ORDERS_2:2; :: thesis: verum

end;then ( x <= y & y <= x ) by Def6;

hence S

then ( x <= y & y <= x ) ;

hence [x,y] in EqRelOf B by Def6; :: thesis: verum

( [x,y] in id the carrier of B iff S

thus EqRelOf A = EqRelOf B

.= id the carrier of B from RELSET_1:sch 4(A1, A2)

.= id the carrier of A ; :: thesis: verum