:: deftheorem defines cut-free PRELAMB:def 13 :
for s being non empty typealg
for IT being PreProof of s holds
( IT is cut-free iff for v being Element of dom IT holds (IT . v) `2 <> 7 );