let C be Subset of R; :: thesis: ( C is connected implies C is strongly_connected )
set iR = the InternalRel of R;
set cR = the carrier of R;
assume C is connected ; :: thesis: C is strongly_connected
then A: the InternalRel of R is_connected_in C by Lclique;
B: the InternalRel of R is_reflexive_in the carrier of R by ORDERS_2:def 4;
thus C is strongly_connected :: thesis: verum

proof

let x, y be set ; :: according to RELAT_2:def 7,ORDERS_2:def 11 :: thesis: ( not x in C or not y in C or [x,y] in the InternalRel of R or [y,x] in the InternalRel of R )
assume that
A1: x in C and
B1: y in C ; :: thesis: ( [x,y] in the InternalRel of R or [y,x] in the InternalRel of R )

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

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

hence ( [x,y] in the InternalRel of R or [y,x] in the InternalRel of R ) by A1, B, RELAT_2:def 1; :: thesis: verum

end;

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

hence ( [x,y] in the InternalRel of R or [y,x] in the InternalRel of R ) by A1, B1, A, RELAT_2:def 6; :: thesis: verum

end;

end;

end;