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

for x, y being Element of A st [x,y] in EqRel A holds

[x,y] in EqRelOf A

for x, y being Element of A st [x,y] in EqRelOf A holds

[x,y] in EqRel A

proof

hence
EqRelOf A c= EqRel A
by RELSET_1:def 1; :: according to XBOOLE_0:def 10 :: thesis: EqRel A c= EqRelOf A
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;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

for x, y being Element of A st [x,y] in EqRel A holds

[x,y] in EqRelOf A

proof

hence
EqRel A c= EqRelOf A
by RELSET_1:def 1; :: thesis: verum
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;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