let S be Subset of A; :: thesis: ( S is empty implies S is strongly_connected )
assume S is empty ; :: thesis: S is strongly_connected
then X: S = {} A ;
let x1, x2 be set ; :: according to RELAT_2:def 7,ORDERS_2:def 11 :: thesis: ( not x1 in S or not x2 in S or [x1,x2] in the InternalRel of A or [x2,x1] in the InternalRel of A )
thus ( not x1 in S or not x2 in S or [x1,x2] in the InternalRel of A or [x2,x1] in the InternalRel of A ) by X; :: thesis: verum