let S be full SubNetStr of N; :: thesis: S is transitive
S is full SubRelStr of N by YELLOW_6:def 7;
hence S is transitive ; :: thesis: verum