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 S1[ set , set ] means $1 = $2;
A1: for x, y being Element of B holds
( [x,y] in EqRelOf B iff S1[x,y] )
proof
let x, y be Element of B; :: thesis: ( [x,y] in EqRelOf B iff S1[x,y] )
hereby :: thesis: ( S1[x,y] implies [x,y] in EqRelOf B )
assume [x,y] in EqRelOf B ; :: thesis: S1[x,y]
then ( x <= y & y <= x ) by Def6;
hence S1[x,y] by ORDERS_2:2; :: thesis: verum
end;
assume S1[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 S1[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;