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}

for x being set holds

( not x <> w or not x in Lang (w,({} ((E ^omega),(E ^omega)))) ) by Th46, Th42;

then for x being object 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

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

for x being set holds

( not x <> w or not x in Lang (w,({} ((E ^omega),(E ^omega)))) ) by Th46, Th42;

then for x being object 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