let A be non empty Poset; for C being Chain of A holds the InternalRel of A |_2 C is being_linear-order
let C be Chain of A; the InternalRel of A |_2 C is being_linear-order
set P = the InternalRel of A |_2 C;
A1:
the InternalRel of A |_2 C is_connected_in C
proof
let x,
y be
object ;
RELAT_2:def 6 ( not x in C or not y in C or x = y or [x,y] in the InternalRel of A |_2 C or [y,x] in the InternalRel of A |_2 C )
assume A2:
(
x in C &
y in C )
;
( x = y or [x,y] in the InternalRel of A |_2 C or [y,x] in the InternalRel of A |_2 C )
then A3:
(
[x,y] in [:C,C:] &
[y,x] in [:C,C:] )
by ZFMISC_1:87;
the
InternalRel of
A is_strongly_connected_in C
by Def7;
then
(
[x,y] in the
InternalRel of
A or
[y,x] in the
InternalRel of
A )
by A2;
hence
(
x = y or
[x,y] in the
InternalRel of
A |_2 C or
[y,x] in the
InternalRel of
A |_2 C )
by A3, XBOOLE_0:def 4;
verum
end;
the InternalRel of A is being_partial-order
;
then
the InternalRel of A |_2 C is being_partial-order
by ORDERS_1:26;
hence
( the InternalRel of A |_2 C is reflexive & the InternalRel of A |_2 C is transitive & the InternalRel of A |_2 C is antisymmetric )
; ORDERS_1:def 6 the InternalRel of A |_2 C is connected
C = field ( the InternalRel of A |_2 C)
by Th46;
hence
the InternalRel of A |_2 C is connected
by A1; verum