:: deftheorem defines primitive PRELAMB:def 8 :
for s being non empty typealg
for IT being type of s holds
( IT is primitive iff ( not IT is left & not IT is right & not IT is middle ) );