:: deftheorem NT defines non-trivial MSAFREE5:def 7 :
for R being Relation holds
( R is non-trivial iff for I being set st I in rng R holds
not I is trivial );