let A be non empty Poset; :: thesis: for S being Subset of A st the InternalRel of A |_2 S is being_linear-order holds
S is Chain of A
let S be Subset of A; :: thesis: ( the InternalRel of A |_2 S is being_linear-order implies S is Chain of A )
assume the InternalRel of A |_2 S is being_linear-order ; :: thesis: S is Chain of A
then A1: the InternalRel of A |_2 S is connected by ORDERS_1:def 5;
field (the InternalRel of A |_2 S) = S by Th107;
then A2: the InternalRel of A |_2 S is_connected_in S by A1, RELAT_2:def 14;
S is strongly_connected

proof

let x be set ; :: according to RELAT_2:def 7,ORDERS_2:def 11 :: thesis: for b₁ being set holds
( not x in S or not b₁ in S or [x,b₁] in the InternalRel of A or [b₁,x] in the InternalRel of A )
let y be set ; :: thesis: ( not x in S or not y in S or [x,y] in the InternalRel of A or [y,x] in the InternalRel of A )
assume A3: ( x in S & y in S ) ; :: thesis: ( [x,y] in the InternalRel of A or [y,x] in the InternalRel of A )
then reconsider a = x, b = y as Element of A ;

now

per cases ( x = y or x <> y ) ;

suppose x = y ; :: thesis: ( [x,y] in the InternalRel of A or [y,x] in the InternalRel of A )

then a <= b ;
hence ( [x,y] in the InternalRel of A or [y,x] in the InternalRel of A ) by Def9; :: thesis: verum

end;

suppose x <> y ; :: thesis: ( [x,y] in the InternalRel of A or [y,x] in the InternalRel of A )

then ( [x,y] in the InternalRel of A |_2 S or [y,x] in the InternalRel of A |_2 S ) by A2, A3, RELAT_2:def 6;
hence ( [x,y] in the InternalRel of A or [y,x] in the InternalRel of A ) by XBOOLE_0:def 4; :: thesis: verum

end;

end;

end;

hence ( [x,y] in the InternalRel of A or [y,x] in the InternalRel of A ) ; :: thesis: verum

end;

hence S is Chain of A ; :: thesis: verum