let A be Preorder; :: thesis: EqRelOf A = EqRel A
for x, y being Element of A st [x,y] in EqRelOf A holds
[x,y] in EqRel A
proof
let x, y be Element of A; :: thesis: ( [x,y] in EqRelOf A implies [x,y] in EqRel A )
assume [x,y] in EqRelOf A ; :: thesis: [x,y] in EqRel A
then ( x <= y & y <= x ) by Def6;
then ( [x,y] in the InternalRel of A & [y,x] in the InternalRel of A ) by ORDERS_2:def 5;
then ( [x,y] in the InternalRel of A & [x,y] in the InternalRel of A ~ ) by RELAT_1:def 7;
then [x,y] in the InternalRel of A /\ ( the InternalRel of A ~) by XBOOLE_0:def 4;
hence [x,y] in EqRel A by DICKSON:def 4; :: thesis: verum
end;
hence EqRelOf A c= EqRel A by RELSET_1:def 1; :: according to XBOOLE_0:def 10 :: thesis: EqRel A c= EqRelOf A
for x, y being Element of A st [x,y] in EqRel A holds
[x,y] in EqRelOf A
proof
let x, y be Element of A; :: thesis: ( [x,y] in EqRel A implies [x,y] in EqRelOf A )
assume [x,y] in EqRel A ; :: thesis: [x,y] in EqRelOf A
then [x,y] in the InternalRel of A /\ ( the InternalRel of A ~) by DICKSON:def 4;
then ( [x,y] in the InternalRel of A & [x,y] in the InternalRel of A ~ ) by XBOOLE_0:def 4;
then ( [x,y] in the InternalRel of A & [y,x] in the InternalRel of A ) by RELAT_1:def 7;
then ( x <= y & y <= x ) by ORDERS_2:def 5;
hence [x,y] in EqRelOf A by Def6; :: thesis: verum
end;
hence EqRel A c= EqRelOf A by RELSET_1:def 1; :: thesis: verum