{0} c= {0,1} by ZFMISC_1:7;
then reconsider A = {0} as Element of Fin {0,1} by FINSUB_1:def 5;
reconsider x = 0 , y = 1 as Element of {0,1} by TARSKI:def 2;
set R = the 1 -element reflexive RelStr ;
reconsider n = (0,1) --> (y,x) as UnOp of {0,1} ;
set f = the carrier of the 1 -element reflexive RelStr --> A;
set T = TA-structure(# the carrier of the 1 -element reflexive RelStr ,{0,1}, the InternalRel of the 1 -element reflexive RelStr ,n,( the carrier of the 1 -element reflexive RelStr --> A) #);
RelStr(# the carrier of TA-structure(# the carrier of the 1 -element reflexive RelStr ,{0,1}, the InternalRel of the 1 -element reflexive RelStr ,n,( the carrier of the 1 -element reflexive RelStr --> A) #), the InternalRel of TA-structure(# the carrier of the 1 -element reflexive RelStr ,{0,1}, the InternalRel of the 1 -element reflexive RelStr ,n,( the carrier of the 1 -element reflexive RelStr --> A) #) #) = RelStr(# the carrier of the 1 -element reflexive RelStr , the InternalRel of the 1 -element reflexive RelStr #) ;
then reconsider T = TA-structure(# the carrier of the 1 -element reflexive RelStr ,{0,1}, the InternalRel of the 1 -element reflexive RelStr ,n,( the carrier of the 1 -element reflexive RelStr --> A) #) as 1 -element reflexive strict TA-structure by STRUCT_0:def 19, WAYBEL_8:12;
take T ; :: thesis: ( not T is void & T is Mizar-widening-like & T is involutive & T is without_fixpoints & T is consistent & T is adj-structured & T is adjs-typed )
thus not T is void ; :: thesis: ( T is Mizar-widening-like & T is involutive & T is without_fixpoints & T is consistent & T is adj-structured & T is adjs-typed )
thus T is Mizar-widening-like ; :: thesis: ( T is involutive & T is without_fixpoints & T is consistent & T is adj-structured & T is adjs-typed )
A1: n . y = x by FUNCT_4:63;
A2: n . x = y by FUNCT_4:63;
hence ( T is involutive & T is without_fixpoints ) by A1, Th4; :: thesis: ( T is consistent & T is adj-structured & T is adjs-typed )

hereby :: according to ABCMIZ_0:def 9 :: thesis: ( T is adj-structured & T is adjs-typed )

let t be type of T; :: thesis: for a being adjective of T st a in adjs t holds
not non- a in adjs t
let a be adjective of T; :: thesis: ( a in adjs t implies not non- a in adjs t )
A3: adjs t = A by FUNCOP_1:7;
( a = 0 or a = 1 ) by TARSKI:def 2;
hence ( a in adjs t implies not non- a in adjs t ) by A2, A3, TARSKI:def 1; :: thesis: verum

end;

set t = the type of T;

hereby :: according to ABCMIZ_0:def 11 :: thesis: T is adjs-typed

let t1, t2 be type of T; :: thesis: adjs (t1 "\/" t2) = (adjs t1) /\ (adjs t2)
A4: adjs t2 = A by FUNCOP_1:7;
adjs t1 = A by FUNCOP_1:7;
hence adjs (t1 "\/" t2) = (adjs t1) /\ (adjs t2) by A4, FUNCOP_1:7; :: thesis: verum

end;

let a be adjective of T; :: according to ABCMIZ_0:def 14 :: thesis: not (types a) \/ (types (non- a)) is empty
A5: adjs the type of T = A by FUNCOP_1:7;
( a = 0 or a = 1 ) by TARSKI:def 2;
then ( a in adjs the type of T or non- a in adjs the type of T ) by A1, A5, TARSKI:def 1;
then ( the type of T in types a or the type of T in types (non- a) ) by Th13;
hence not (types a) \/ (types (non- a)) is empty ; :: thesis: verum