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 ;
field ( the InternalRel of A |_2 S) = S by Th46;
then A2: the InternalRel of A |_2 S is_connected_in S by A1;
S is strongly_connected
proof
let x, y be object ; :: according to RELAT_2:def 7,ORDERS_2:def 7 :: 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 :: thesis: ( [x,y] in the InternalRel of A or [y,x] in the InternalRel of A )
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 ) ; :: 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;
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