:: deftheorem Def4 defines Lex FLANG_1:def 4 :
for E being set
for b₂ being Subset of (E ^omega) holds
( b₂ = Lex E iff for x being set holds
( x in b₂ iff ex e being Element of E st
( e in E & x = <%e%> ) ) );