A1:
PARTITIONS X c= bool (bool X)

S is a_partition of X by PARTIT1:def 3;

hence PARTITIONS X is Part-Family of X by A1, EQREL_1:def 7; :: thesis: verum

proof

for S being set st S in PARTITIONS X holds
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in PARTITIONS X or x in bool (bool X) )

assume x in PARTITIONS X ; :: thesis: x in bool (bool X)

then x is a_partition of X by PARTIT1:def 3;

hence x in bool (bool X) ; :: thesis: verum

end;assume x in PARTITIONS X ; :: thesis: x in bool (bool X)

then x is a_partition of X by PARTIT1:def 3;

hence x in bool (bool X) ; :: thesis: verum

S is a_partition of X by PARTIT1:def 3;

hence PARTITIONS X is Part-Family of X by A1, EQREL_1:def 7; :: thesis: verum