set X = {0};
set Y = {0,1,2};
reconsider 00 = 0 as Element of {0} by TARSKI:def 1;
reconsider 01 = 1, 02 = 2, y0 = 0 as Element of {0,1,2} by ENUMSET1:def 1;
set a = (0,1,2) --> ({},<*00*>,<*00,00*>);
set r = {0,1,2} --> 00;
A1: 0 ,1,2 are_mutually_distinct ;
( <*> {0} in {0} * & <*00*> in {0} * & <*00,00*> in {0} * ) by FINSEQ_1:def 11;
then {{},<*00*>,<*00,00*>} c= {0} * by ZFMISC_1:133;
then ( rng ((0,1,2) --> ({},<*00*>,<*00,00*>)) c= {0} * & dom ((0,1,2) --> ({},<*00*>,<*00,00*>)) = {0,1,2} ) by FUNCT_4:128, FUNCT_4:147, A1;
then reconsider a = (0,1,2) --> ({},<*00*>,<*00,00*>) as Function of {0,1,2},({0} *) by FUNCT_2:2;
reconsider r = {0,1,2} --> 00 as Function of {0,1,2},{0} ;
take B = BoolSignature(# {0},{0,1,2},a,r,00,<*y0,01,02*> #); :: thesis: ( B is 3 -connectives & B is 1-1-connectives & B is bool-correct & not B is empty & not B is void )
thus len the connectives of B = 3 by FINSEQ_1:45; :: according to AOFA_A00:def 29 :: thesis: ( B is 1-1-connectives & B is bool-correct & not B is empty & not B is void )
thus the connectives of B is one-to-one by FINSEQ_3:95; :: according to AOFA_A00:def 28 :: thesis: ( B is bool-correct & not B is empty & not B is void )
thus len the connectives of B >= 3 by FINSEQ_1:45; :: according to AOFA_A00:def 30 :: thesis: ( the connectives of B . 1 is_of_type {} , the bool-sort of B & the connectives of B . 2 is_of_type <* the bool-sort of B*>, the bool-sort of B & the connectives of B . 3 is_of_type <* the bool-sort of B, the bool-sort of B*>, the bool-sort of B & not B is empty & not B is void )
the connectives of B . 1 = 0 by FINSEQ_1:45;
hence the Arity of B . ( the connectives of B . 1) = {} by FUNCT_4:134; :: according to AOFA_A00:def 8 :: thesis: ( the ResultSort of B . ( the connectives of B . 1) = the bool-sort of B & the connectives of B . 2 is_of_type <* the bool-sort of B*>, the bool-sort of B & the connectives of B . 3 is_of_type <* the bool-sort of B, the bool-sort of B*>, the bool-sort of B & not B is empty & not B is void )
thus the ResultSort of B . ( the connectives of B . 1) = the bool-sort of B ; :: thesis: ( the connectives of B . 2 is_of_type <* the bool-sort of B*>, the bool-sort of B & the connectives of B . 3 is_of_type <* the bool-sort of B, the bool-sort of B*>, the bool-sort of B & not B is empty & not B is void )
the connectives of B . 2 = 1 by FINSEQ_1:45;
hence the Arity of B . ( the connectives of B . 2) = <* the bool-sort of B*> by FUNCT_4:135; :: according to AOFA_A00:def 8 :: thesis: ( the ResultSort of B . ( the connectives of B . 2) = the bool-sort of B & the connectives of B . 3 is_of_type <* the bool-sort of B, the bool-sort of B*>, the bool-sort of B & not B is empty & not B is void )
thus the ResultSort of B . ( the connectives of B . 2) = the bool-sort of B ; :: thesis: ( the connectives of B . 3 is_of_type <* the bool-sort of B, the bool-sort of B*>, the bool-sort of B & not B is empty & not B is void )
the connectives of B . 3 = 2 by FINSEQ_1:45;
hence the Arity of B . ( the connectives of B . 3) = <* the bool-sort of B, the bool-sort of B*> by FUNCT_4:135; :: according to AOFA_A00:def 8 :: thesis: ( the ResultSort of B . ( the connectives of B . 3) = the bool-sort of B & not B is empty & not B is void )
thus the ResultSort of B . ( the connectives of B . 3) = the bool-sort of B ; :: thesis: ( not B is empty & not B is void )
thus not the carrier of B is empty ; :: according to STRUCT_0:def 1 :: thesis: not B is void
thus not the carrier' of B is empty ; :: according to STRUCT_0:def 13 :: thesis: verum
thus verum ; :: thesis: verum