:: deftheorem Def3 defines -matrix-membered MATGRP_0:def 3 :
for L being non empty 1-sorted
for n being Nat
for IT being set holds
( IT is n,L -matrix-membered iff for x being object st x in IT holds
x is Matrix of n,L );