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