reconsider E = {} as Family-Class of X by XBOOLE_1:2;
take E ; :: thesis: E is partition-membered
let S be set ; :: according to EQREL_1:def 7 :: thesis: ( S in E implies S is a_partition of X )
assume S in E ; :: thesis: S is a_partition of X
hence S is a_partition of X ; :: thesis: verum