let p be Element of MC-wff ; :: thesis: p is FinSequence-like
MC-wff c= NAT * by Def7;
hence p is FinSequence-like ; :: thesis: verum