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