set P = the 1 -element reflexive non void TA-structure ;
set s = the Function of the adjectives of the 1 -element reflexive non void TA-structure , the carrier of the 1 -element reflexive non void TA-structure ;
take T = TAS-structure(# the carrier of the 1 -element reflexive non void TA-structure , the adjectives of the 1 -element reflexive non void TA-structure , the InternalRel of the 1 -element reflexive non void TA-structure , the non-op of the 1 -element reflexive non void TA-structure , the adj-map of the 1 -element reflexive non void TA-structure , the Function of the adjectives of the 1 -element reflexive non void TA-structure , the carrier of the 1 -element reflexive non void TA-structure #); :: thesis: ( not T is void & T is reflexive & T is 1 -element & T is strict )
RelStr(# the carrier of the 1 -element reflexive non void TA-structure , the InternalRel of the 1 -element reflexive non void TA-structure #) = RelStr(# the carrier of T, the InternalRel of T #) ;
hence ( not T is void & T is reflexive & T is 1 -element & T is strict ) by STRUCT_0:def 19, WAYBEL_8:12; :: thesis: verum