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