assume not {*,non_op} misses Constructors ; :: thesis: contradiction
then consider x being object such that
A1: x in {*,non_op} and
A2: x in Constructors by XBOOLE_0:3;
( x in Modes \/ Attrs or x in Funcs ) by A2, XBOOLE_0:def 3;
then ( x in Modes or x in Attrs or x in Funcs ) by XBOOLE_0:def 3;
then consider Y, Z being set such that
A3: x in [:Y,Z:] ;
A4: ex y, z being object st
( y in Y & z in Z & [y,z] = x ) by A3, ZFMISC_1:def 2;
reconsider x = x as set by TARSKI:1;
( x = * or x = non_op ) by A1, TARSKI:def 2;
then ( the_rank_of x = 0 or the_rank_of x = 1 ) by CLASSES1:73;
then the_rank_of x c= 1 ;
then the_rank_of x in succ (succ {}) by ORDINAL1:6, ORDINAL1:12;
then x in Rank (succ (succ {})) by CLASSES1:66;
hence contradiction by A4, CLASSES1:29, CLASSES1:45; :: thesis: verum