let F be Graph-yielding Function; :: thesis: ( ( F is simple implies rng F is simple ) & ( rng F is simple implies F is simple ) & ( F is Dsimple implies rng F is Dsimple ) & ( rng F is Dsimple implies F is Dsimple ) & ( F is Tree-like implies rng F is Tree-like ) & ( rng F is Tree-like implies F is Tree-like ) )
hereby :: thesis: ( ( rng F is simple implies F is simple ) & ( F is Dsimple implies rng F is Dsimple ) & ( rng F is Dsimple implies F is Dsimple ) & ( F is Tree-like implies rng F is Tree-like ) & ( rng F is Tree-like implies F is Tree-like ) )
assume F is simple ; :: thesis: rng F is simple
then ( rng F is non-multi & rng F is loopless ) by Th3;
hence rng F is simple ; :: thesis: verum
end;
hereby :: thesis: ( ( F is Dsimple implies rng F is Dsimple ) & ( rng F is Dsimple implies F is Dsimple ) & ( F is Tree-like implies rng F is Tree-like ) & ( rng F is Tree-like implies F is Tree-like ) )
assume rng F is simple ; :: thesis: F is simple
then ( F is non-multi & F is loopless ) by Th3;
hence F is simple ; :: thesis: verum
end;
hereby :: thesis: ( ( rng F is Dsimple implies F is Dsimple ) & ( F is Tree-like implies rng F is Tree-like ) & ( rng F is Tree-like implies F is Tree-like ) )
assume F is Dsimple ; :: thesis: rng F is Dsimple
then ( rng F is non-Dmulti & rng F is loopless ) by Th3;
hence rng F is Dsimple ; :: thesis: verum
end;
hereby :: thesis: ( F is Tree-like iff rng F is Tree-like )
assume rng F is Dsimple ; :: thesis: F is Dsimple
then ( F is non-Dmulti & F is loopless ) by Th3;
hence F is Dsimple ; :: thesis: verum
end;
hereby :: thesis: ( rng F is Tree-like implies F is Tree-like )
assume F is Tree-like ; :: thesis: rng F is Tree-like
then ( rng F is acyclic & rng F is connected ) by Th3;
hence rng F is Tree-like ; :: thesis: verum
end;
hereby :: thesis: verum
assume rng F is Tree-like ; :: thesis: F is Tree-like
then ( F is acyclic & F is connected ) by Th3;
hence F is Tree-like ; :: thesis: verum
end;