let Omega be set ; :: thesis: ( Omega = {1,2,3,4} implies ( {1} c= Omega & {2} c= Omega & {3} c= Omega & {4} c= Omega & {1,2} c= Omega & {3,4} c= Omega & {} c= Omega & Omega c= Omega ) )
assume A0: Omega = {1,2,3,4} ; :: thesis: ( {1} c= Omega & {2} c= Omega & {3} c= Omega & {4} c= Omega & {1,2} c= Omega & {3,4} c= Omega & {} c= Omega & Omega c= Omega )
then ( 1 in Omega & 2 in Omega & 3 in Omega & 4 in Omega ) by ENUMSET1:def 2;
hence ( {1} c= Omega & {2} c= Omega & {3} c= Omega & {4} c= Omega & {1,2} c= Omega & {3,4} c= Omega & {} c= Omega & Omega c= Omega ) by A0, Lemacik2, ZFMISC_1:31; :: thesis: verum