let E be set ; :: thesis: for A being Subset of (E ^omega) st A * = E ^omega holds
Lex E c= A
let A be Subset of (E ^omega); :: thesis: ( A * = E ^omega implies Lex E c= A )
assume A1: A * = E ^omega ; :: thesis: Lex E c= A
thus Lex E c= A :: thesis: verum

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in Lex E or x in A )
assume A2: x in Lex E ; :: thesis: x in A
then ex e being Element of E st
( e in E & x = <%e%> ) by Def4;
hence x in A by A1, A2, Th72; :: thesis: verum

end;