consider R being non empty trivial reflexive RelStr , A being non void involutive without_fixpoints AdjectiveStr , f being Function of the carrier of R,(Fin the adjectives of A);
take T = TA-structure(# the carrier of R,the adjectives of A,the InternalRel of R,the non-op of A,f #); :: thesis: ( T is trivial & T is reflexive & not T is empty & not T is void & T is involutive & T is without_fixpoints & T is strict )
thus T is trivial ; :: thesis: ( T is reflexive & not T is empty & not T is void & T is involutive & T is without_fixpoints & T is strict )
RelStr(# the carrier of R,the InternalRel of R #) = RelStr(# the carrier of T,the InternalRel of T #) ;
hence T is reflexive by WAYBEL_8:12; :: thesis: ( not T is empty & not T is void & T is involutive & T is without_fixpoints & T is strict )
thus ( not T is empty & not T is void ) ; :: thesis: ( T is involutive & T is without_fixpoints & T is strict )
AdjectiveStr(# the adjectives of A,the non-op of A #) = AdjectiveStr(# the adjectives of T,the non-op of T #) ;
hence ( T is involutive & T is without_fixpoints ) by Th5, Th6; :: thesis: T is strict
thus T is strict ; :: thesis: verum