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

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

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

hence EqRelOf A = id the carrier of A ; :: thesis: verum

end;

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

then reconsider B = A as non empty Order ;
defpred S₁[ set , set ] means $1 = $2;
A1: for x, y being Element of B holds
( [x,y] in EqRelOf B iff S₁[x,y] )

proof

let x, y be Element of B; :: thesis: ( [x,y] in EqRelOf B iff S₁[x,y] )

hereby :: thesis: ( S₁[x,y] implies [x,y] in EqRelOf B )

assume [x,y] in EqRelOf B ; :: thesis: S₁[x,y]
then ( x <= y & y <= x ) by Def6;
hence S₁[x,y] by ORDERS_2:2; :: thesis: verum

end;

assume S₁[x,y] ; :: thesis: [x,y] in EqRelOf B
then ( x <= y & y <= x ) ;
hence [x,y] in EqRelOf B by Def6; :: thesis: verum

end;

A2: for x, y being Element of B holds
( [x,y] in id the carrier of B iff S₁[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;

end;