let x be Element of Constructors ; :: thesis: ( ( kind_of x = a_Type implies x in Modes ) & ( x in Modes implies kind_of x = a_Type ) & ( kind_of x = an_Adj implies x in Attrs ) & ( x in Attrs implies kind_of x = an_Adj ) & ( kind_of x = a_Term implies x in Funcs ) & ( x in Funcs implies kind_of x = a_Term ) )
A1: ( x in Modes \/ Attrs or x in Funcs ) by XBOOLE_0:def 3;
A2: ( x in Modes implies x `1 in {a_Type} ) by MCART_1:10;
A3: ( x in Attrs implies x `1 in {an_Adj} ) by MCART_1:10;
( x in Funcs implies x `1 in {a_Term} ) by MCART_1:10;
hence ( ( kind_of x = a_Type implies x in Modes ) & ( x in Modes implies kind_of x = a_Type ) & ( kind_of x = an_Adj implies x in Attrs ) & ( x in Attrs implies kind_of x = an_Adj ) & ( kind_of x = a_Term implies x in Funcs ) & ( x in Funcs implies kind_of x = a_Term ) ) by A1, A2, A3, TARSKI:def 1, XBOOLE_0:def 3; :: thesis: verum