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 ;
then A2: the InternalRel of R is_transitive_in the carrier of R ;
thus <=E R is_reflexive_in Class (EqRel R) :: according to ORDERS_1:def 8 :: thesis: ( <=E R is_transitive_in Class (EqRel R) & <=E R is_antisymmetric_in Class (EqRel R) )
proof
let x be object ; :: 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 object such that
A3: a in the carrier of R and
A4: x = Class ((EqRel R),a) by EQREL_1:def 3;
R is reflexive by A1;
then the InternalRel of R is_reflexive_in the carrier of R ;
then A5: [a,a] in the InternalRel of R by A3;
reconsider a9 = a as Element of R by A3;
a9 <= a9 by A5;
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 object ; :: 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) and
y in Class (EqRel R) and
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) and
A10: y = Class ((EqRel R),b) and
A11: a <= b by A7, Def5;
consider c, d being Element of R such that
A12: y = Class ((EqRel R),c) and
A13: z = Class ((EqRel R),d) and
A14: c <= d by A8, Def5;
A15: [a,b] in the InternalRel of R by A11;
A16: [c,d] in the InternalRel of R by A14;
A17: ex x1 being object st
( x1 in the carrier of R & x = Class ((EqRel R),x1) ) by A6, EQREL_1:def 3;
then b in Class ((EqRel R),c) by A10, A12, EQREL_1:23;
then [b,c] in EqRel R by EQREL_1:19;
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, A15, A17;
then [a,d] in the InternalRel of R by A2, A16, A17;
then a <= d ;
hence [x,z] in <=E R by A9, A13, Def5; :: thesis: verum
end;
thus <=E R is_antisymmetric_in Class (EqRel R) :: thesis: verum
proof
let x, y be object ; :: 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
A18: x in Class (EqRel R) and
y in Class (EqRel R) and
A19: [x,y] in <=E R and
A20: [y,x] in <=E R ; :: thesis: x = y
consider a, b being Element of R such that
A21: x = Class ((EqRel R),a) and
A22: y = Class ((EqRel R),b) and
A23: a <= b by A19, Def5;
consider c, d being Element of R such that
A24: y = Class ((EqRel R),c) and
A25: x = Class ((EqRel R),d) and
A26: c <= d by A20, Def5;
A27: [a,b] in the InternalRel of R by A23;
A28: [c,d] in the InternalRel of R by A26;
A29: ex x1 being object st
( x1 in the carrier of R & x = Class ((EqRel R),x1) ) by A18, EQREL_1:def 3;
then A30: d in Class ((EqRel R),a) by A21, A25, EQREL_1:23;
a in Class ((EqRel R),a) by A29, EQREL_1:20;
then A31: [a,d] in EqRel R by A30, EQREL_1:22;
A32: c in Class ((EqRel R),b) by A22, A24, A29, EQREL_1:23;
b in Class ((EqRel R),b) by A29, EQREL_1:20;
then A33: [b,c] in EqRel R by A32, EQREL_1:22;
[a,d] in the InternalRel of R /\ ( the InternalRel of R ~) by A1, A31, Def4;
then [a,d] in the InternalRel of R ~ by XBOOLE_0:def 4;
then A34: [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, A33, Def4;
then [b,c] in the InternalRel of R by XBOOLE_0:def 4;
then [b,d] in the InternalRel of R by A2, A28, A29;
then A35: [b,a] in the InternalRel of R by A2, A29, A34;
[b,a] in the InternalRel of R ~ by A27, RELAT_1:def 7;
then [b,a] in the InternalRel of R /\ ( the InternalRel of R ~) by A35, XBOOLE_0:def 4;
then [b,a] in EqRel R by A1, Def4;
then b in Class ((EqRel R),a) by EQREL_1:19;
hence x = y by A21, A22, EQREL_1:23; :: thesis: verum
end;