let N be non empty with_non-empty_elements set ; :: thesis: for S being COM-Struct of N
for p being Element of FinPartSt S holds p is FinPartState of S
let S be COM-Struct of N; :: thesis: for p being Element of FinPartSt S holds p is FinPartState of S
let p be Element of FinPartSt S; :: thesis: p is FinPartState of S
p in FinPartSt S ;
then ex q being Element of sproduct the Object-Kind of S st
( q = p & q is finite ) ;
hence p is FinPartState of S ; :: thesis: verum