let X be non empty set ; :: thesis: for PX being a_partition of X
for Pi being set st Pi in PX holds
ex x being Element of X st x in Pi
let PX be a_partition of X; :: thesis: for Pi being set st Pi in PX holds
ex x being Element of X st x in Pi
let Pi be set ; :: thesis: ( Pi in PX implies ex x being Element of X st x in Pi )
assume Pi in PX ; :: thesis: ex x being Element of X st x in Pi
then reconsider Pi = Pi as Element of PX ;
set q = the Element of Pi;
reconsider q = the Element of Pi as Element of X ;
take q ; :: thesis: q in Pi
thus q in Pi ; :: thesis: verum