set Omega1 = {1};
set Omega2 = {1,2};
set Omega3 = {1,2,3};
set Omega4 = {1,2,3,4};
reconsider F1 = bool {1} as SigmaField of {1} ;
reconsider F2 = bool {1,2} as SigmaField of {1,2} ;
reconsider F3 = bool {1,2,3} as SigmaField of {1,2,3} ;
reconsider F4 = bool {1,2,3,4} as SigmaField of {1,2,3,4} ;
ATh100:
{1} c< {1,2}
by ZFMISC_1:7, ZFMISC_1:20;
E10:
F1 c= F2
by ZFMISC_1:7, ZFMISC_1:67;
E11:
F2 c= F3
by ATh101, ZFMISC_1:67;
F3 c= F4
by ATh102, ZFMISC_1:67;
hence
ex Omega1, Omega2, Omega3, Omega4 being non empty set st
( Omega1 c< Omega2 & Omega2 c< Omega3 & Omega3 c< Omega4 & ex F1 being SigmaField of Omega1 ex F2 being SigmaField of Omega2 ex F3 being SigmaField of Omega3 ex F4 being SigmaField of Omega4 st
( F1 c= F2 & F2 c= F3 & F3 c= F4 ) )
by ATh100, ATh101, ATh102, E10, E11; verum