A1: PARTITIONS X c= bool (bool X)

proof

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;

for S being set st S in PARTITIONS X holds
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