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