set R = the non empty trivial reflexive RelStr ;
set A = the non void involutive without_fixpoints AdjectiveStr ;
set f = the Function of the carrier of the non empty trivial reflexive RelStr ,(Fin the adjectives of the non void involutive without_fixpoints AdjectiveStr );
take T = TA-structure(# the carrier of the non empty trivial reflexive RelStr , the adjectives of the non void involutive without_fixpoints AdjectiveStr , the InternalRel of the non empty trivial reflexive RelStr , the non-op of the non void involutive without_fixpoints AdjectiveStr , the Function of the carrier of the non empty trivial reflexive RelStr ,(Fin the adjectives of the non void involutive without_fixpoints AdjectiveStr ) #); :: 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 the non empty trivial reflexive RelStr , the InternalRel of the non empty trivial reflexive RelStr #) = 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 the non void involutive without_fixpoints AdjectiveStr , the non-op of the non void involutive without_fixpoints AdjectiveStr #) = 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