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