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 be
set ;
RELAT_2:def 6 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 ;
( 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 Def11;
then
(
[x,y] in the
InternalRel of
A or
[y,x] in the
InternalRel of
A )
by A2, RELAT_2:def 7;
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
by ORDERS_1:def 4;
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 )
by ORDERS_1:def 4; ORDERS_1:def 5 the InternalRel of A |_2 C is connected
C = field ( the InternalRel of A |_2 C)
by Th107;
hence
the InternalRel of A |_2 C is connected
by A1, RELAT_2:def 14; verum