:: deftheorem defines | MATRLIN2:def 1 :
for S being 1-sorted
for R being Relation holds R | S = R | the carrier of S;