let W be Universe; :: thesis: for X being set st X in W holds
sup X in W
let X be set ; :: thesis: ( X in W implies sup X in W )
assume A1: X in W ; :: thesis: sup X in W
reconsider a = union (On X) as Ordinal by ORDINAL3:7;
On X c= X by ORDINAL2:9;
then On X in W by A1, CLASSES1:def 1;
then a in W by CLASSES2:65;
then reconsider a = a as Ordinal of W ;
( sup X c= succ a & succ a in W ) by ORDINAL3:85;
hence sup X in W by CLASSES1:def 1; :: thesis: verum