let R be non empty RelStr ; :: thesis: ( R is quasi_ordered & R is connected implies <=E R linearly_orders Class (EqRel R) )
assume that
A1: R is quasi_ordered and
A2: R is connected ; :: thesis: <=E R linearly_orders Class (EqRel R)
A3: <=E R partially_orders Class (EqRel R) by A1, Th8;
hence <=E R is_reflexive_in Class (EqRel R) ; :: according to ORDERS_1:def 9 :: thesis: ( <=E R is_transitive_in Class (EqRel R) & <=E R is_antisymmetric_in Class (EqRel R) & <=E R is_connected_in Class (EqRel R) )
thus <=E R is_transitive_in Class (EqRel R) by A3; :: thesis: ( <=E R is_antisymmetric_in Class (EqRel R) & <=E R is_connected_in Class (EqRel R) )
thus <=E R is_antisymmetric_in Class (EqRel R) by A3; :: thesis: <=E R is_connected_in Class (EqRel R)
thus <=E R is_connected_in Class (EqRel R) :: thesis: verum

proof

set CR = the carrier of R;
let x, y be object ; :: according to RELAT_2:def 6 :: thesis: ( not x in Class (EqRel R) or not y in Class (EqRel R) or x = y or [x,y] in <=E R or [y,x] in <=E R )
assume that
A4: x in Class (EqRel R) and
A5: y in Class (EqRel R) and
x <> y and
A6: not [x,y] in <=E R ; :: thesis: [y,x] in <=E R
consider a being object such that
A7: a in the carrier of R and
A8: x = Class ((EqRel R),a) by A4, EQREL_1:def 3;
consider b being object such that
A9: b in the carrier of R and
A10: y = Class ((EqRel R),b) by A5, EQREL_1:def 3;
reconsider a9 = a, b9 = b as Element of R by A7, A9;
not a9 <= b9 by A6, A8, A10, Def5;
then b9 <= a9 by A2, WAYBEL_0:def 29;
hence [y,x] in <=E R by A8, A10, Def5; :: thesis: verum

end;