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