let X be non empty set ; :: thesis: for x being Element of X
for F being Part-Family of X
for A being set st A in { (EqClass (x,S)) where S is a_partition of X : S in F } holds
ex T being a_partition of X st
( T in F & A = EqClass (x,T) )
let x be Element of X; :: thesis: for F being Part-Family of X
for A being set st A in { (EqClass (x,S)) where S is a_partition of X : S in F } holds
ex T being a_partition of X st
( T in F & A = EqClass (x,T) )
let F be Part-Family of X; :: thesis: for A being set st A in { (EqClass (x,S)) where S is a_partition of X : S in F } holds
ex T being a_partition of X st
( T in F & A = EqClass (x,T) )
let A be set ; :: thesis: ( A in { (EqClass (x,S)) where S is a_partition of X : S in F } implies ex T being a_partition of X st
( T in F & A = EqClass (x,T) ) )
assume A in { (EqClass (x,S)) where S is a_partition of X : S in F } ; :: thesis: ex T being a_partition of X st
( T in F & A = EqClass (x,T) )
then consider S being a_partition of X such that
A1: ( A = EqClass (x,S) & S in F ) ;
take S ; :: thesis: ( S in F & A = EqClass (x,S) )
thus ( S in F & A = EqClass (x,S) ) by A1; :: thesis: verum