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 A1: S = {} A ;
let x1, x2 be object ; :: according to RELAT_2:def 7,ORDERS_2:def 7 :: 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 A1; :: thesis: verum