:: deftheorem Def12 defines Proof PRELAMB:def 12 :
for s being non empty typealg
for b₂ being PreProof of s holds
( b₂ is Proof of s iff ( dom b₂ is finite & ( for v being Element of dom b₂ holds v is correct ) ) );