consider P being non empty trivial reflexive non void TA-structure ;
consider s being Function of the adjectives of P,the carrier of P;
take T = TAS-structure(# the carrier of P,the adjectives of P,the InternalRel of P,the non-op of P,the adj-map of P,s #); :: thesis: ( not T is void & T is reflexive & T is trivial & not T is empty & T is strict )
RelStr(# the carrier of P,the InternalRel of P #) = 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