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

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