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