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