Special_SigmaField1 c< Special_SigmaField2 by XX1;
hence ex Omega being non empty set ex F1, F2, F3 being SigmaField of Omega st
( F1 c< F2 & F2 c< F3 ) by XX2; :: thesis: verum