let E be set ; :: thesis: for w being Element of E ^omega holds Lang w,({} (E ^omega ),(E ^omega )) = {w}
let w be Element of E ^omega ; :: thesis: Lang w,({} (E ^omega ),(E ^omega )) = {w}

now

let x be set ; :: thesis: ( x <> w implies not x in Lang w,({} (E ^omega ),(E ^omega )) )
assume that
A1: x <> w and
A2: x in Lang w,({} (E ^omega ),(E ^omega )) ; :: thesis: contradiction
reconsider t = x as Element of E ^omega by A2;
w ==>* t, {} (E ^omega ),(E ^omega ) by A2, Th46;
hence contradiction by A1, Th42; :: thesis: verum

end;

then for x being set holds
( x in Lang w,({} (E ^omega ),(E ^omega )) iff x = w ) by Th47;
hence Lang w,({} (E ^omega ),(E ^omega )) = {w} by TARSKI:def 1; :: thesis: verum