let N be with_non-empty_elements set ; :: thesis: for S being COM-Struct of N
for p being FinPartState of S holds p in FinPartSt S
let S be COM-Struct of N; :: thesis: for p being FinPartState of S holds p in FinPartSt S
let p be FinPartState of S; :: thesis: p in FinPartSt S
p in sproduct the Object-Kind of S by CARD_3:153;
hence p in FinPartSt S ; :: thesis: verum