let A be non empty Poset; :: thesis: for C being Chain of A holds the InternalRel of A |_2 C is being_linear-order
let C be Chain of A; :: thesis: the InternalRel of A |_2 C is being_linear-order
set P = the InternalRel of A |_2 C;
the InternalRel of A is being_partial-order
by ORDERS_1:def 4;
then
the InternalRel of A |_2 C is being_partial-order
by ORDERS_1:114;
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 )
by ORDERS_1:def 4; :: according to ORDERS_1:def 5 :: thesis: the InternalRel of A |_2 C is connected
A1:
C = field (the InternalRel of A |_2 C)
by Th107;
the InternalRel of A |_2 C is_connected_in C
proof
let x be
set ;
:: according to RELAT_2:def 6 :: thesis: for b1 being set holds
( not x in C or not b1 in C or x = b1 or [x,b1] in the InternalRel of A |_2 C or [b1,x] in the InternalRel of A |_2 C )let y be
set ;
:: thesis: ( 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 )
;
:: thesis: ( x = y or [x,y] in the InternalRel of A |_2 C or [y,x] in the InternalRel of A |_2 C )
the
InternalRel of
A is_strongly_connected_in C
by Def11;
then A3:
(
[x,y] in the
InternalRel of
A or
[y,x] in the
InternalRel of
A )
by A2, RELAT_2:def 7;
(
[x,y] in [:C,C:] &
[y,x] in [:C,C:] )
by A2, ZFMISC_1:106;
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;
:: thesis: verum
end;
hence
the InternalRel of A |_2 C is connected
by A1, RELAT_2:def 14; :: thesis: verum