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