for s being non empty typealg
for p being Proof of s
for v being Element of dom p holds
not not (p . v) `2 = 0 & ... & not (p . v) `2 = 7