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