S c= X by PBOOLE:def 18;
then ( z in S . x & S . x c= X . x & not S . x is empty ) ;
hence z is Element of X . x ; :: thesis: verum