let X be set ; :: thesis: for p being a_partition of X holds {p} is Part-Family of X

let p be a_partition of X; :: thesis: {p} is Part-Family of X

for x being set st x in {p} holds

x is a_partition of X by TARSKI:def 1;

hence {p} is Part-Family of X by Def7; :: thesis: verum

let p be a_partition of X; :: thesis: {p} is Part-Family of X

for x being set st x in {p} holds

x is a_partition of X by TARSKI:def 1;

hence {p} is Part-Family of X by Def7; :: thesis: verum