let Y be non empty set ; :: thesis: for P being a_partition of Y
for y being Element of Y ex A being Subset of Y st
( y in A & A in P )
let P be a_partition of Y; :: thesis: for y being Element of Y ex A being Subset of Y st
( y in A & A in P )
let y be Element of Y; :: thesis: ex A being Subset of Y st
( y in A & A in P )
consider R being Equivalence_Relation of Y such that
A1: P = Class R by EQREL_1:43;
take Class R,y ; :: thesis: ( y in Class R,y & Class R,y in P )
thus y in Class R,y by EQREL_1:28; :: thesis: Class R,y in P
thus Class R,y in P by A1, EQREL_1:def 5; :: thesis: verum