consider P being non empty trivial reflexive complete Mizar-widening-like non void involutive without_fixpoints strict consistent adj-structured adjs-typed TA-structure ;
set 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,(sub P) #);
( not TAS-structure(# the carrier of P,the adjectives of P,the InternalRel of P,the non-op of P,the adj-map of P,(sub P) #) is empty & RelStr(# the carrier of P,the InternalRel of P #) = RelStr(# the carrier of TAS-structure(# the carrier of P,the adjectives of P,the InternalRel of P,the non-op of P,the adj-map of P,(sub P) #),the InternalRel of TAS-structure(# the carrier of P,the adjectives of P,the InternalRel of P,the non-op of P,the adj-map of P,(sub P) #) #) ) ;
then reconsider 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,(sub P) #) as non empty trivial reflexive non void strict TAS-structure by Def4, WAYBEL_8:12;
take T ; :: thesis: ( T is Mizar-widening-like & T is involutive & T is without_fixpoints & T is consistent & T is adj-structured & T is adjs-typed & T is non-absorbing & T is subjected & T is commutative )
thus T is Mizar-widening-like ; :: thesis: ( T is involutive & T is without_fixpoints & T is consistent & T is adj-structured & T is adjs-typed & T is non-absorbing & T is subjected & T is commutative )
AdjectiveStr(# the adjectives of P,the non-op of P #) = AdjectiveStr(# the adjectives of T,the non-op of T #) ;
hence ( T is involutive & T is without_fixpoints ) by Th5, Th6; :: thesis: ( T is consistent & T is adj-structured & T is adjs-typed & T is non-absorbing & T is subjected & T is commutative )
thus ( T is consistent & T is adj-structured & T is adjs-typed ) by Th8, Th9, Th17; :: thesis: ( T is non-absorbing & T is subjected & T is commutative )
A1: RelStr(# the carrier of P,the InternalRel of P #) = RelStr(# the carrier of T,the InternalRel of T #) ;

hereby :: according to ABCMIZ_0:def 26 :: thesis: ( T is subjected & T is commutative )

let a be adjective of T; :: thesis: sub (non- a) = sub a
reconsider b = a as adjective of P ;
thus sub (non- a) = sup ((types (non- b)) \/ (types (non- (non- b)))) by Def22
.= sup ((types (non- b)) \/ (types b)) by Def6
.= sub a by Def22 ; :: thesis: verum

end;

thus T is subjected :: thesis: T is commutative

proof

let a be adjective of T; :: according to ABCMIZ_0:def 25 :: thesis: ( (types a) \/ (types (non- a)) is_<=_than sub a & ( types a <> {} & types (non- a) <> {} implies sub a = sup ((types a) \/ (types (non- a))) ) )
reconsider b = a as adjective of P ;
( types a = types b & types (non- a) = types (non- b) ) by Th11;
then sup ((types a) \/ (types (non- a))) = sup ((types b) \/ (types (non- b))) by A1, YELLOW_0:17, YELLOW_0:26;
then sup ((types a) \/ (types (non- a))) = sub a by Def22;
hence ( (types a) \/ (types (non- a)) is_<=_than sub a & ( types a <> {} & types (non- a) <> {} implies sub a = sup ((types a) \/ (types (non- a))) ) ) by YELLOW_0:32; :: thesis: verum

end;

let t1, t2 be type of T; :: according to ABCMIZ_0:def 30 :: thesis: for a being adjective of T st a is_properly_applicable_to t1 & a ast t1 <= t2 holds
ex A being finite Subset of the adjectives of T st
( A is_properly_applicable_to t1 "\/" t2 & A ast (t1 "\/" t2) = t2 )
let a be adjective of T; :: thesis: ( a is_properly_applicable_to t1 & a ast t1 <= t2 implies ex A being finite Subset of the adjectives of T st
( A is_properly_applicable_to t1 "\/" t2 & A ast (t1 "\/" t2) = t2 ) )
assume ( a is_properly_applicable_to t1 & a ast t1 <= t2 ) ; :: thesis: ex A being finite Subset of the adjectives of T st
( A is_properly_applicable_to t1 "\/" t2 & A ast (t1 "\/" t2) = t2 )
take A = {} the adjectives of T; :: thesis: ( A is_properly_applicable_to t1 "\/" t2 & A ast (t1 "\/" t2) = t2 )
thus A is_properly_applicable_to t1 "\/" t2 by Th64; :: thesis: A ast (t1 "\/" t2) = t2
thus A ast (t1 "\/" t2) = t2 by STRUCT_0:def 10; :: thesis: verum