let E be set ; :: thesis: for A being Subset of (E ^omega)
for a being Element of E ^omega st a in A * holds
A * = (A \/ {a}) *
let A be Subset of (E ^omega); :: thesis: for a being Element of E ^omega st a in A * holds
A * = (A \/ {a}) *
let a be Element of E ^omega ; :: thesis: ( a in A * implies A * = (A \/ {a}) * )
assume a in A * ; :: thesis: A * = (A \/ {a}) *
then {a} c= A * by ZFMISC_1:31;
hence A * = (A \/ {a}) * by Th68; :: thesis: verum