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

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