consider R being non empty trivial reflexive RelStr ;
reconsider x = 0 , y = 1 as Element of {0 ,1} by TARSKI:def 2;
reconsider n = 0 ,1 --> y,x as UnOp of {0 ,1} ;
{0 } c= {0 ,1} by ZFMISC_1:12;
then reconsider A = {0 } as Element of Fin {0 ,1} by FINSUB_1:def 5;
set f = the carrier of R --> A;
set T = TA-structure(# the carrier of R,{0 ,1},the InternalRel of R,n,(the carrier of R --> A) #);
RelStr(# the carrier of TA-structure(# the carrier of R,{0 ,1},the InternalRel of R,n,(the carrier of R --> A) #),the InternalRel of TA-structure(# the carrier of R,{0 ,1},the InternalRel of R,n,(the carrier of R --> A) #) #) = RelStr(# the carrier of R,the InternalRel of R #) ;
then reconsider T = TA-structure(# the carrier of R,{0 ,1},the InternalRel of R,n,(the carrier of R --> A) #) as non empty trivial reflexive strict TA-structure by 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: ( 0 <> 1 & n . x = y & n . y = x ) by FUNCT_4:66;
hence ( T is involutive & T is without_fixpoints ) by 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 )
A2: ( ( a = 0 or a = 1 ) & non- a = n . a ) by TARSKI:def 2;
adjs t = A by FUNCOP_1:13;
hence ( a in adjs t implies not non- a in adjs t ) by A1, A2, TARSKI:def 1; :: thesis: verum

end;

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)
( adjs (t1 "\/" t2) = A & adjs t1 = A & adjs t2 = A ) by FUNCOP_1:13;
hence adjs (t1 "\/" t2) = (adjs t1) /\ (adjs t2) ; :: thesis: verum

end;

let a be adjective of T; :: according to ABCMIZ_0:def 14 :: thesis: not (types a) \/ (types (non- a)) is empty
A3: ( ( a = 0 or a = 1 ) & non- a = n . a ) by TARSKI:def 2;
consider t being type of T;
adjs t = A by FUNCOP_1:13;
then ( a in adjs t or non- a in adjs t ) by A1, A3, TARSKI:def 1;
then ( t in types a or t in types (non- a) ) by Th13;
hence not (types a) \/ (types (non- a)) is empty ; :: thesis: verum