defpred S_{1}[ set ] means $1 is non empty IntervalSet of U;

ex X being set st

for x being set holds

( x in X iff ( x in bool (bool U) & S_{1}[x] ) )
from XFAMILY:sch 1();

then consider X being set such that

A1: for x being set holds

( x in X iff ( x in bool (bool U) & S_{1}[x] ) )
;

set x = the Element of U;

reconsider E = { the Element of U} as Subset of U by ZFMISC_1:31;

{E} is non empty IntervalSet of U by Th10;

then reconsider X = X as non empty set by A1;

take X ; :: thesis: for x being set holds

( x in X iff x is non empty IntervalSet of U )

thus for x being set holds

( x in X iff x is non empty IntervalSet of U ) by A1; :: thesis: verum

ex X being set st

for x being set holds

( x in X iff ( x in bool (bool U) & S

then consider X being set such that

A1: for x being set holds

( x in X iff ( x in bool (bool U) & S

set x = the Element of U;

reconsider E = { the Element of U} as Subset of U by ZFMISC_1:31;

{E} is non empty IntervalSet of U by Th10;

then reconsider X = X as non empty set by A1;

take X ; :: thesis: for x being set holds

( x in X iff x is non empty IntervalSet of U )

thus for x being set holds

( x in X iff x is non empty IntervalSet of U ) by A1; :: thesis: verum