let i be set ; :: according to PBOOLE:def 1 :: thesis: ( i in {} implies ([[0]] {}) . i in ([[0]] {}) . i )
thus ( i in {} implies ([[0]] {}) . i in ([[0]] {}) . i ) ; :: thesis: verum