let A be set ; :: thesis: for X being non empty set
for S being a_partition of X st A in S holds
ex x being Element of X st A = EqClass (x,S)
let X be non empty set ; :: thesis: for S being a_partition of X st A in S holds
ex x being Element of X st A = EqClass (x,S)
let S be a_partition of X; :: thesis: ( A in S implies ex x being Element of X st A = EqClass (x,S) )
assume A1: A in S ; :: thesis: ex x being Element of X st A = EqClass (x,S)
then not A is empty by Def4;
then consider x being object such that
A2: x in A ;
take x ; :: thesis: ( x is set & x is Element of X & A = EqClass (x,S) )
thus ( x is set & x is Element of X & A = EqClass (x,S) ) by A1, A2, Def6; :: thesis: verum