let P be FinSequence-membered set ; :: thesis: ( {} in P * & P c= P * )
{} in P ^^ 0 by Th4;
hence {} in P * by Th6; :: thesis: P c= P *
P ^^ 1 = P by Th8;
hence P c= P * by Th6; :: thesis: verum