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, Th10;
hence
<=E R is_reflexive_in Class (EqRel R)
by ORDERS_1:def 7; :: according to ORDERS_1:def 8 :: 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, ORDERS_1:def 7; :: 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, ORDERS_1:def 7; :: thesis: <=E R is_connected_in Class (EqRel R)
thus
<=E R is_connected_in Class (EqRel R)
:: thesis: verumproof
set CR = the
carrier of
R;
let x,
y be
set ;
:: 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
set such that A7:
a in the
carrier of
R
and A8:
x = Class (EqRel R),
a
by A4, EQREL_1:def 5;
consider b being
set such that A9:
b in the
carrier of
R
and A10:
y = Class (EqRel R),
b
by A5, EQREL_1:def 5;
reconsider a' =
a,
b' =
b as
Element of
R by A7, A9;
not
a' <= b'
by A6, A8, A10, Def5;
then
b' <= a'
by A2, WAYBEL_0:def 29;
hence
[y,x] in <=E R
by A8, A10, Def5;
:: thesis: verum
end;