let R be non empty RelStr ; ( 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
; <=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)
; ORDERS_1:def 9 ( <=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; ( <=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; <=E R is_connected_in Class (EqRel R)
thus
<=E R is_connected_in Class (EqRel R)
verumproof
set CR = the
carrier of
R;
let x,
y be
object ;
RELAT_2:def 6 ( 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
;
[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;
verum
end;