take [0] I ; :: thesis: [0] I is empty-yielding
let i be set ; :: according to PBOOLE:def 15 :: thesis: ( i in I implies ([0] I) . i is empty )
assume i in I ; :: thesis: ([0] I) . i is empty
thus ([0] I) . i is empty by Th5; :: thesis: verum