{0 } c= {0 ,1} by ZFMISC_1:12;
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;
consider R being non empty trivial reflexive RelStr ;
reconsider n = 0 ,1 --> y,x as UnOp of {0 ,1} ;
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: n . y = x by FUNCT_4:66;
A2: n . x = y by FUNCT_4:66;
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:13;
( 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;

consider t being 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:13;
adjs t1 = A by FUNCOP_1:13;
hence adjs (t1 "\/" t2) = (adjs t1) /\ (adjs t2) by A4, FUNCOP_1:13; :: 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 t = A by FUNCOP_1:13;
( a = 0 or a = 1 ) by TARSKI:def 2;
then ( a in adjs t or non- a in adjs t ) by A1, A5, 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