let IL be non empty set ; :: thesis: for N being with_non-empty_elements set
for S being AMI-Struct of IL,N
for p being Element of FinPartSt S holds p is FinPartState of S
let N be with_non-empty_elements set ; :: thesis: for S being AMI-Struct of IL,N
for p being Element of FinPartSt S holds p is FinPartState of S
let S be AMI-Struct of IL,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