let R be RelStr ; :: thesis: ( R is quasi_ordered implies <=E R partially_orders Class (EqRel R) )
set CR = the carrier of R;
set IR = the InternalRel of R;
assume A1: R is quasi_ordered ; :: thesis: <=E R partially_orders Class (EqRel R)
then R is transitive by Def3;
then A2: the InternalRel of R is_transitive_in the carrier of R by ORDERS_2:def 5;
thus <=E R is_reflexive_in Class (EqRel R) :: according to ORDERS_1:def 7 :: thesis: ( <=E R is_transitive_in Class (EqRel R) & <=E R is_antisymmetric_in Class (EqRel R) )

proof

let x be set ; :: according to RELAT_2:def 1 :: thesis: ( not x in Class (EqRel R) or [x,x] in <=E R )
assume x in Class (EqRel R) ; :: thesis: [x,x] in <=E R
then consider a being set such that
A3: a in the carrier of R and
A4: x = Class (EqRel R),a by EQREL_1:def 5;
R is reflexive by A1, Def3;
then the InternalRel of R is_reflexive_in the carrier of R by ORDERS_2:def 4;
then A5: [a,a] in the InternalRel of R by A3, RELAT_2:def 1;
reconsider a' = a as Element of R by A3;
a' <= a' by A5, ORDERS_2:def 9;
hence [x,x] in <=E R by A4, Def5; :: thesis: verum

end;

thus <=E R is_transitive_in Class (EqRel R) :: thesis: <=E R is_antisymmetric_in Class (EqRel R)

proof

let x, y, z be set ; :: according to RELAT_2:def 8 :: thesis: ( not x in Class (EqRel R) or not y in Class (EqRel R) or not z in Class (EqRel R) or not [x,y] in <=E R or not [y,z] in <=E R or [x,z] in <=E R )
assume that
A6: ( x in Class (EqRel R) & y in Class (EqRel R) & z in Class (EqRel R) ) and
A7: [x,y] in <=E R and
A8: [y,z] in <=E R ; :: thesis: [x,z] in <=E R
consider a, b being Element of R such that
A9: ( x = Class (EqRel R),a & y = Class (EqRel R),b & a <= b ) by A7, Def5;
consider c, d being Element of R such that
A10: ( y = Class (EqRel R),c & z = Class (EqRel R),d & c <= d ) by A8, Def5;
A11: [a,b] in the InternalRel of R by A9, ORDERS_2:def 9;
A12: [c,d] in the InternalRel of R by A10, ORDERS_2:def 9;
consider x1 being set such that
A13: ( x1 in the carrier of R & x = Class (EqRel R),x1 ) by A6, EQREL_1:def 5;
b in Class (EqRel R),c by A9, A10, A13, EQREL_1:31;
then [b,c] in EqRel R by EQREL_1:27;
then [b,c] in the InternalRel of R /\ (the InternalRel of R ~ ) by A1, Def4;
then [b,c] in the InternalRel of R by XBOOLE_0:def 4;
then [a,c] in the InternalRel of R by A2, A11, A13, RELAT_2:def 8;
then [a,d] in the InternalRel of R by A2, A12, A13, RELAT_2:def 8;
then a <= d by ORDERS_2:def 9;
hence [x,z] in <=E R by A9, A10, Def5; :: thesis: verum

end;

thus <=E R is_antisymmetric_in Class (EqRel R) :: thesis: verum

proof

let x, y be set ; :: according to RELAT_2:def 4 :: thesis: ( not x in Class (EqRel R) or not y in Class (EqRel R) or not [x,y] in <=E R or not [y,x] in <=E R or x = y )
assume that
A14: x in Class (EqRel R) and
y in Class (EqRel R) and
A15: [x,y] in <=E R and
A16: [y,x] in <=E R ; :: thesis: x = y
consider a, b being Element of R such that
A17: ( x = Class (EqRel R),a & y = Class (EqRel R),b & a <= b ) by A15, Def5;
consider c, d being Element of R such that
A18: ( y = Class (EqRel R),c & x = Class (EqRel R),d & c <= d ) by A16, Def5;
A19: [a,b] in the InternalRel of R by A17, ORDERS_2:def 9;
A20: [c,d] in the InternalRel of R by A18, ORDERS_2:def 9;
consider x1 being set such that
A21: ( x1 in the carrier of R & x = Class (EqRel R),x1 ) by A14, EQREL_1:def 5;
A22: d in Class (EqRel R),a by A17, A18, A21, EQREL_1:31;
a in Class (EqRel R),a by A21, EQREL_1:28;
then A23: [a,d] in EqRel R by A22, EQREL_1:30;
A24: c in Class (EqRel R),b by A17, A18, A21, EQREL_1:31;
b in Class (EqRel R),b by A21, EQREL_1:28;
then A25: [b,c] in EqRel R by A24, EQREL_1:30;
[a,d] in the InternalRel of R /\ (the InternalRel of R ~ ) by A1, A23, Def4;
then ( [a,d] in the InternalRel of R & [a,d] in the InternalRel of R ~ ) by XBOOLE_0:def 4;
then A26: [d,a] in the InternalRel of R by RELAT_1:def 7;
[b,c] in the InternalRel of R /\ (the InternalRel of R ~ ) by A1, A25, Def4;
then ( [b,c] in the InternalRel of R & [b,c] in the InternalRel of R ~ ) by XBOOLE_0:def 4;
then [b,d] in the InternalRel of R by A2, A20, A21, RELAT_2:def 8;
then A27: [b,a] in the InternalRel of R by A2, A21, A26, RELAT_2:def 8;
[b,a] in the InternalRel of R ~ by A19, RELAT_1:def 7;
then [b,a] in the InternalRel of R /\ (the InternalRel of R ~ ) by A27, XBOOLE_0:def 4;
then [b,a] in EqRel R by A1, Def4;
then b in Class (EqRel R),a by EQREL_1:27;
hence x = y by A17, EQREL_1:31; :: thesis: verum

end;