reconsider M = N " X as full SubRelStr of N by Def10;
M is transitive ;
hence ( N " X is transitive & N " X is full ) ; :: thesis: verum