let A be RelStr ; :: thesis: ( A is reflexive & A is connected implies A is strongly_connected )
assume A1: ( A is reflexive & A is connected ) ; :: thesis:
for x, y being object st x in the carrier of A & y in the carrier of A & not [x,y] in the InternalRel of A holds
[y,x] in the InternalRel of A
proof
let x, y be object ; :: thesis: ( x in the carrier of A & y in the carrier of A & not [x,y] in the InternalRel of A implies [y,x] in the InternalRel of A )
assume A2: ( x in the carrier of A & y in the carrier of A ) ; :: 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 )
hence ( [x,y] in the InternalRel of A or [y,x] in the InternalRel of A ) by ; :: thesis: verum
end;
suppose x <> y ; :: thesis: ( [x,y] in the InternalRel of A or [y,x] in the InternalRel of A )
hence ( [x,y] in the InternalRel of A or [y,x] in the InternalRel of A ) by ; :: thesis: verum
end;
end;
end;
hence A is strongly_connected by RELAT_2:def 7; :: thesis: verum