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 clique ; :: thesis: C is strongly_connected
then A1: the InternalRel of R is_connected_in C ;
A2: the InternalRel of R is_reflexive_in the carrier of R by ORDERS_2:def 2;
thus C is strongly_connected :: thesis: verum
proof
let x, y be object ; :: according to RELAT_2:def 7,ORDERS_2:def 7 :: 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
A3: x in C and
A4: 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 A3, A2; :: 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 A3, A4, A1; :: thesis: verum
end;
end;
end;