set R = the 1 -element reflexive RelStr ;
set A = the non void involutive without_fixpoints AdjectiveStr ;
set f = the Function of the carrier of the 1 -element reflexive RelStr ,(Fin the adjectives of the non void involutive without_fixpoints AdjectiveStr );
take T = TA-structure(# the carrier of the 1 -element reflexive RelStr , the adjectives of the non void involutive without_fixpoints AdjectiveStr , the InternalRel of the 1 -element reflexive RelStr , the non-op of the non void involutive without_fixpoints AdjectiveStr , the Function of the carrier of the 1 -element reflexive RelStr ,(Fin the adjectives of the non void involutive without_fixpoints AdjectiveStr ) #); :: thesis: ( T is 1 -element & T is reflexive & not T is void & T is involutive & T is without_fixpoints & T is strict )
thus T is 1 -element by STRUCT_0:def 19; :: thesis: ( T is reflexive & not T is void & T is involutive & T is without_fixpoints & T is strict )
RelStr(# the carrier of the 1 -element reflexive RelStr , the InternalRel of the 1 -element reflexive RelStr #) = RelStr(# the carrier of T, the InternalRel of T #) ;
hence T is reflexive by WAYBEL_8:12; :: thesis: ( not T is void & T is involutive & T is without_fixpoints & T is strict )
thus 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