let J be object ; :: according to FINSEQ_1:def 18 :: thesis: ( not J in p ^^ I or J is set )
assume J in p ^^ I ; :: thesis: J is set
then ex q being Element of I st
( J = p ^ q & q in I ) ;
hence J is set ; :: thesis: verum