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:34;
take Class (R,y) ; :: thesis: ( y in Class (R,y) & Class (R,y) in P )
thus y in Class (R,y) by EQREL_1:20; :: thesis: Class (R,y) in P
thus Class (R,y) in P by A1, EQREL_1:def 3; :: thesis: verum