let X be set ; :: thesis: Lim X c= X
thus for x being set st x in Lim X holds
x in X by ORDINAL1:def 11; :: according to TARSKI:def 3 :: thesis: verum