theorem E3: :: ABCMIZ_0:1
for b1 being Noetherian sup-Semilattice
for b2 being Ideal of b1 holds
( ex_sup_of b2,b1 & sup b2 in b2 )
proof end;

theorem E13: :: ABCMIZ_0:10
for b1 being reflexive transitive antisymmetric with_suprema TA-structure st b1 is adj-structured holds
for b2, b3 being type of b1 st b2 <= b3 holds
adjs b3 c= adjs b2
proof end;

theorem E16: :: ABCMIZ_0:11
for b1, b2 being TA-structure st TA-structure(# the carrier of b1,the adjectives of b1,the InternalRel of b1,the non-op of b1,the adj-map of b1 #) = TA-structure(# the carrier of b2,the adjectives of b2,the InternalRel of b2,the non-op of b2,the adj-map of b2 #) holds
for b3 being adjective of b1
for b4 being adjective of b2 st b3 = b4 holds
types b3 = types b4
proof end;

theorem :: ABCMIZ_0:12
for b1 being non empty TA-structure
for b2 being adjective of b1 holds types b2 = { b3 where B is type of b1 : b2 in adjs b3 }
proof end;

theorem E17: :: ABCMIZ_0:13
for b1 being TA-structure
for b2 being type of b1
for b3 being adjective of b1 holds
( b3 in adjs b2 iff b2 in types b3 )
proof end;

theorem E18: :: ABCMIZ_0:14
for b1 being non empty TA-structure
for b2 being type of b1
for b3 being Subset of the adjectives of b1 holds
( b3 c= adjs b2 iff b2 in types b3 )
proof end;

theorem :: ABCMIZ_0:15
for b1 being non void TA-structure
for b2 being type of b1 holds adjs b2 = { b3 where B is adjective of b1 : b2 in types b3 }
proof end;

theorem E19: :: ABCMIZ_0:16
for b1 being non empty TA-structure holds types ({} the adjectives of b1) = the carrier of b1
proof end;

theorem E20: :: ABCMIZ_0:17
for b1, b2 being TA-structure st TA-structure(# the carrier of b1,the adjectives of b1,the InternalRel of b1,the non-op of b1,the adj-map of b1 #) = TA-structure(# the carrier of b2,the adjectives of b2,the InternalRel of b2,the non-op of b2,the adj-map of b2 #) & b1 is adjs-typed holds
b2 is adjs-typed
proof end;

theorem :: ABCMIZ_0:18
for b1 being consistent TA-structure
for b2 being adjective of b1 holds types b2 misses types (non- b2)
proof end;

theorem :: ABCMIZ_0:19
canceled;

theorem :: ABCMIZ_0:2
for b1, b2 being AdjectiveStr st the adjectives of b1 = the adjectives of b2 & b1 is void holds
b2 is void
proof end;

theorem E23: :: ABCMIZ_0:20
for b1 being reflexive transitive antisymmetric with_suprema adj-structured TA-structure
for b2 being adjective of b1
for b3 being type of b1 st b2 is_applicable_to b3 holds
(types b2) /\ (downarrow b3) is Ideal of b1
proof end;

theorem E24: :: ABCMIZ_0:21
for b1 being reflexive transitive antisymmetric with_suprema Noetherian adj-structured TA-structure
for b2 being type of b1
for b3 being adjective of b1 st b3 is_applicable_to b2 holds
b3 ast b2 <= b2
proof end;

theorem E25: :: ABCMIZ_0:22
for b1 being reflexive transitive antisymmetric with_suprema Noetherian adj-structured TA-structure
for b2 being type of b1
for b3 being adjective of b1 st b3 is_applicable_to b2 holds
b3 in adjs (b3 ast b2)
proof end;

theorem E26: :: ABCMIZ_0:23
for b1 being reflexive transitive antisymmetric with_suprema Noetherian adj-structured TA-structure
for b2 being type of b1
for b3 being adjective of b1 st b3 is_applicable_to b2 holds
b3 ast b2 in types b3
proof end;

theorem E27: :: ABCMIZ_0:24
for b1 being reflexive transitive antisymmetric with_suprema Noetherian adj-structured TA-structure
for b2 being type of b1
for b3 being adjective of b1
for b4 being type of b1 st b4 <= b2 & b3 in adjs b4 holds
( b3 is_applicable_to b2 & b4 <= b3 ast b2 )
proof end;

theorem E28: :: ABCMIZ_0:25
for b1 being reflexive transitive antisymmetric with_suprema Noetherian adj-structured TA-structure
for b2 being type of b1
for b3 being adjective of b1 st b3 in adjs b2 holds
( b3 is_applicable_to b2 & b3 ast b2 = b2 )
proof end;

theorem :: ABCMIZ_0:26
for b1 being reflexive transitive antisymmetric with_suprema Noetherian adj-structured TA-structure
for b2 being type of b1
for b3, b4 being adjective of b1 st b3 is_applicable_to b2 & b4 is_applicable_to b3 ast b2 holds
( b4 is_applicable_to b2 & b3 is_applicable_to b4 ast b2 & b3 ast (b4 ast b2) = b4 ast (b3 ast b2) )
proof end;

theorem E29: :: ABCMIZ_0:27
for b1 being reflexive transitive antisymmetric with_suprema adj-structured TA-structure
for b2 being Subset of the adjectives of b1
for b3 being type of b1 st b2 is_applicable_to b3 holds
(types b2) /\ (downarrow b3) is Ideal of b1
proof end;

theorem E30: :: ABCMIZ_0:28
for b1 being non empty reflexive transitive antisymmetric TA-structure
for b2 being type of b1 holds ({} the adjectives of b1) ast b2 = b2
proof end;

theorem :: ABCMIZ_0:29
for b1 being non empty reflexive transitive non void TA-structure
for b2 being type of b1 holds apply (<*> the adjectives of b1),b2 = <*b2*>
proof end;

theorem :: ABCMIZ_0:3
for b1, b2 being AdjectiveStr st AdjectiveStr(# the adjectives of b1,the non-op of b1 #) = AdjectiveStr(# the adjectives of b2,the non-op of b2 #) holds
for b3 being adjective of b1
for b4 being adjective of b2 st b3 = b4 holds
non- b3 = non- b4 ;

theorem E32: :: ABCMIZ_0:30
for b1 being non empty reflexive transitive non void TA-structure
for b2 being type of b1
for b3 being adjective of b1 holds apply <*b3*>,b2 = <*b2,(b3 ast b2)*>
proof end;

theorem E33: :: ABCMIZ_0:31
for b1 being non empty reflexive transitive non void TA-structure
for b2 being type of b1 holds (<*> the adjectives of b1) ast b2 = b2
proof end;

theorem E34: :: ABCMIZ_0:32
for b1 being non empty reflexive transitive non void TA-structure
for b2 being type of b1
for b3 being adjective of b1 holds <*b3*> ast b2 = b3 ast b2
proof end;

theorem :: ABCMIZ_0:33
for b1, b2 being FinSequence
for b3 being natural number st b3 >= 1 & b3 < len b1 holds
(b1 $^ b2) . b3 = b1 . b3
proof end;

theorem E35: :: ABCMIZ_0:34
for b1 being non empty FinSequence
for b2 being FinSequence
for b3 being natural number st b3 < len b2 holds
(b1 $^ b2) . ((len b1) + b3) = b2 . (b3 + 1)
proof end;

theorem E36: :: ABCMIZ_0:35
for b1 being non empty reflexive transitive non void TA-structure
for b2 being type of b1
for b3, b4 being FinSequence of the adjectives of b1 holds apply (b3 ^ b4),b2 = (apply b3,b2) $^ (apply b4,(b3 ast b2))
proof end;

theorem E37: :: ABCMIZ_0:36
for b1 being non empty reflexive transitive non void TA-structure
for b2 being type of b1
for b3, b4 being FinSequence of the adjectives of b1
for b5 being natural number st b5 in dom b3 holds
(apply (b3 ^ b4),b2) . b5 = (apply b3,b2) . b5
proof end;

theorem E38: :: ABCMIZ_0:37
for b1 being non empty reflexive transitive non void TA-structure
for b2 being type of b1
for b3, b4 being FinSequence of the adjectives of b1 holds (apply (b3 ^ b4),b2) . ((len b3) + 1) = b3 ast b2
proof end;

theorem E39: :: ABCMIZ_0:38
for b1 being non empty reflexive transitive non void TA-structure
for b2 being type of b1
for b3, b4 being FinSequence of the adjectives of b1 holds b4 ast (b3 ast b2) = (b3 ^ b4) ast b2
proof end;

theorem :: ABCMIZ_0:39
for b1 being non empty reflexive transitive non void TA-structure
for b2 being type of b1 holds <*> the adjectives of b1 is_applicable_to b2
proof end;

theorem E6: :: ABCMIZ_0:4
for b1, b2 being set st b1 <> b2 holds
for b3 being AdjectiveStr st the adjectives of b3 = {b1,b2} & the non-op of b3 . b1 = b2 & the non-op of b3 . b2 = b1 holds
( not b3 is void & b3 is involutive & b3 is without_fixpoints )
proof end;

theorem E41: :: ABCMIZ_0:40
for b1 being non empty reflexive transitive non void TA-structure
for b2 being type of b1
for b3 being adjective of b1 holds
( b3 is_applicable_to b2 iff <*b3*> is_applicable_to b2 )
proof end;

theorem E42: :: ABCMIZ_0:41
for b1 being non empty reflexive transitive non void TA-structure
for b2 being type of b1
for b3, b4 being FinSequence of the adjectives of b1 st b3 ^ b4 is_applicable_to b2 holds
( b3 is_applicable_to b2 & b4 is_applicable_to b3 ast b2 )
proof end;

theorem E43: :: ABCMIZ_0:42
for b1 being reflexive transitive antisymmetric with_suprema Noetherian non void adj-structured TA-structure
for b2 being type of b1
for b3 being FinSequence of the adjectives of b1 st b3 is_applicable_to b2 holds
for b4, b5 being natural number st 1 <= b4 & b4 <= b5 & b5 <= (len b3) + 1 holds
for b6, b7 being type of b1 st b6 = (apply b3,b2) . b4 & b7 = (apply b3,b2) . b5 holds
b7 <= b6
proof end;

theorem E44: :: ABCMIZ_0:43
for b1 being reflexive transitive antisymmetric with_suprema Noetherian non void adj-structured TA-structure
for b2 being type of b1
for b3 being FinSequence of the adjectives of b1 st b3 is_applicable_to b2 holds
for b4 being type of b1 st b4 in rng (apply b3,b2) holds
( b3 ast b2 <= b4 & b4 <= b2 )
proof end;

theorem E45: :: ABCMIZ_0:44
for b1 being reflexive transitive antisymmetric with_suprema Noetherian non void adj-structured TA-structure
for b2 being type of b1
for b3 being FinSequence of the adjectives of b1 st b3 is_applicable_to b2 holds
b3 ast b2 <= b2
proof end;

theorem E46: :: ABCMIZ_0:45
for b1 being reflexive transitive antisymmetric with_suprema Noetherian non void adj-structured TA-structure
for b2 being type of b1
for b3 being FinSequence of the adjectives of b1 st b3 is_applicable_to b2 holds
rng b3 c= adjs (b3 ast b2)
proof end;

theorem E47: :: ABCMIZ_0:46
for b1 being reflexive transitive antisymmetric with_suprema Noetherian non void adj-structured TA-structure
for b2 being type of b1
for b3 being FinSequence of the adjectives of b1 st b3 is_applicable_to b2 holds
for b4 being Subset of the adjectives of b1 st b4 = rng b3 holds
b4 is_applicable_to b2
proof end;

theorem E48: :: ABCMIZ_0:47
for b1 being reflexive transitive antisymmetric with_suprema Noetherian non void adj-structured TA-structure
for b2 being type of b1
for b3, b4 being FinSequence of the adjectives of b1 st b3 is_applicable_to b2 & rng b4 c= rng b3 holds
for b5 being type of b1 st b5 in rng (apply b4,b2) holds
b3 ast b2 <= b5
proof end;

theorem E49: :: ABCMIZ_0:48
for b1 being reflexive transitive antisymmetric with_suprema Noetherian non void adj-structured TA-structure
for b2 being type of b1
for b3, b4 being FinSequence of the adjectives of b1 st b3 ^ b4 is_applicable_to b2 holds
b4 ^ b3 is_applicable_to b2
proof end;

theorem :: ABCMIZ_0:49
for b1 being reflexive transitive antisymmetric with_suprema Noetherian non void adj-structured TA-structure
for b2 being type of b1
for b3, b4 being FinSequence of the adjectives of b1 st b3 ^ b4 is_applicable_to b2 holds
(b3 ^ b4) ast b2 = (b4 ^ b3) ast b2
proof end;

theorem E7: :: ABCMIZ_0:5
for b1, b2 being AdjectiveStr st AdjectiveStr(# the adjectives of b1,the non-op of b1 #) = AdjectiveStr(# the adjectives of b2,the non-op of b2 #) & b1 is involutive holds
b2 is involutive
proof end;

theorem E50: :: ABCMIZ_0:50
for b1 being reflexive transitive antisymmetric with_suprema Noetherian adj-structured TA-structure
for b2 being type of b1
for b3 being Subset of the adjectives of b1 st b3 is_applicable_to b2 holds
b3 ast b2 <= b2
proof end;

theorem E51: :: ABCMIZ_0:51
for b1 being reflexive transitive antisymmetric with_suprema Noetherian adj-structured TA-structure
for b2 being type of b1
for b3 being Subset of the adjectives of b1 st b3 is_applicable_to b2 holds
b3 c= adjs (b3 ast b2)
proof end;

theorem :: ABCMIZ_0:52
for b1 being reflexive transitive antisymmetric with_suprema Noetherian adj-structured TA-structure
for b2 being type of b1
for b3 being Subset of the adjectives of b1 st b3 is_applicable_to b2 holds
b3 ast b2 in types b3
proof end;

theorem E52: :: ABCMIZ_0:53
for b1 being reflexive transitive antisymmetric with_suprema Noetherian adj-structured TA-structure
for b2 being type of b1
for b3 being Subset of the adjectives of b1
for b4 being type of b1 st b4 <= b2 & b3 c= adjs b4 holds
( b3 is_applicable_to b2 & b4 <= b3 ast b2 )
proof end;

theorem :: ABCMIZ_0:54
for b1 being reflexive transitive antisymmetric with_suprema Noetherian adj-structured TA-structure
for b2 being type of b1
for b3 being Subset of the adjectives of b1 st b3 c= adjs b2 holds
( b3 is_applicable_to b2 & b3 ast b2 = b2 )
proof end;

theorem E53: :: ABCMIZ_0:55
for b1 being TA-structure
for b2 being type of b1
for b3, b4 being Subset of the adjectives of b1 st b3 is_applicable_to b2 & b4 c= b3 holds
b4 is_applicable_to b2
proof end;

theorem E54: :: ABCMIZ_0:56
for b1 being reflexive transitive antisymmetric with_suprema Noetherian non void adj-structured TA-structure
for b2 being type of b1
for b3 being adjective of b1
for b4, b5 being Subset of the adjectives of b1 st b5 = b4 \/ {b3} & b5 is_applicable_to b2 holds
b3 ast (b4 ast b2) = b5 ast b2
proof end;

theorem E55: :: ABCMIZ_0:57
for b1 being reflexive transitive antisymmetric with_suprema Noetherian non void adj-structured TA-structure
for b2 being type of b1
for b3 being FinSequence of the adjectives of b1 st b3 is_applicable_to b2 holds
for b4 being Subset of the adjectives of b1 st b4 = rng b3 holds
b3 ast b2 = b4 ast b2
proof end;

theorem E59: :: ABCMIZ_0:58
for b1 being non empty reflexive transitive non void TAS-structure
for b2 being type of b1
for b3 being FinSequence of the adjectives of b1 st b3 is_properly_applicable_to b2 holds
b3 is_applicable_to b2
proof end;

theorem :: ABCMIZ_0:59
for b1 being non empty reflexive transitive non void TAS-structure
for b2 being type of b1 holds <*> the adjectives of b1 is_properly_applicable_to b2
proof end;

theorem E8: :: ABCMIZ_0:6
for b1, b2 being AdjectiveStr st AdjectiveStr(# the adjectives of b1,the non-op of b1 #) = AdjectiveStr(# the adjectives of b2,the non-op of b2 #) & b1 is without_fixpoints holds
b2 is without_fixpoints
proof end;

theorem :: ABCMIZ_0:60
for b1 being non empty reflexive transitive non void TAS-structure
for b2 being type of b1
for b3 being adjective of b1 holds
( b3 is_properly_applicable_to b2 iff <*b3*> is_properly_applicable_to b2 )
proof end;

theorem E60: :: ABCMIZ_0:61
for b1 being non empty reflexive transitive non void TAS-structure
for b2 being type of b1
for b3, b4 being FinSequence of the adjectives of b1 st b3 ^ b4 is_properly_applicable_to b2 holds
( b3 is_properly_applicable_to b2 & b4 is_properly_applicable_to b3 ast b2 )
proof end;

theorem E61: :: ABCMIZ_0:62
for b1 being non empty reflexive transitive non void TAS-structure
for b2 being type of b1
for b3, b4 being FinSequence of the adjectives of b1 st b3 is_properly_applicable_to b2 & b4 is_properly_applicable_to b3 ast b2 holds
b3 ^ b4 is_properly_applicable_to b2
proof end;

theorem E63: :: ABCMIZ_0:63
for b1 being non empty reflexive transitive non void TAS-structure
for b2 being type of b1
for b3 being Subset of the adjectives of b1 st b3 is_properly_applicable_to b2 holds
b3 is finite
proof end;

theorem E64: :: ABCMIZ_0:64
for b1 being non empty reflexive transitive non void TAS-structure
for b2 being type of b1 holds {} the adjectives of b1 is_properly_applicable_to b2
proof end;

theorem E65: :: ABCMIZ_0:65
for b1 being non empty reflexive transitive non void TAS-structure
for b2 being type of b1
for b3 being Subset of the adjectives of b1 st b3 is_properly_applicable_to b2 holds
ex b4 being Subset of the adjectives of b1 st
( b4 c= b3 & b4 is_properly_applicable_to b2 & b3 ast b2 = b4 ast b2 & ( for b5 being Subset of the adjectives of b1 st b5 c= b4 & b5 is_properly_applicable_to b2 & b3 ast b2 = b5 ast b2 holds
b5 = b4 ) )
proof end;

theorem E67: :: ABCMIZ_0:66
for b1 being reflexive transitive antisymmetric with_suprema Noetherian non void adj-structured TAS-structure
for b2 being type of b1
for b3 being Subset of the adjectives of b1 st b3 is_properly_applicable_to b2 holds
ex b4 being one-to-one FinSequence of the adjectives of b1 st
( rng b4 = b3 & b4 is_properly_applicable_to b2 )
proof end;

theorem E69: :: ABCMIZ_0:67
for b1 being reflexive transitive antisymmetric with_suprema Noetherian non void adj-structured TAS-structure holds b1 @--> c= the InternalRel of b1
proof end;

theorem E70: :: ABCMIZ_0:68
for b1 being reflexive transitive antisymmetric with_suprema Noetherian non void adj-structured TAS-structure
for b2, b3 being type of b1 st b1 @--> reduces b2,b3 holds
b2 <= b3
proof end;

theorem E71: :: ABCMIZ_0:69
for b1 being reflexive transitive antisymmetric with_suprema Noetherian non void adj-structured TAS-structure holds b1 @--> is irreflexive
proof end;

theorem :: ABCMIZ_0:7
for b1, b2 being TA-structure st TA-structure(# the carrier of b1,the adjectives of b1,the InternalRel of b1,the non-op of b1,the adj-map of b1 #) = TA-structure(# the carrier of b2,the adjectives of b2,the InternalRel of b2,the non-op of b2,the adj-map of b2 #) holds
for b3 being type of b1
for b4 being type of b2 st b3 = b4 holds
adjs b3 = adjs b4 ;

theorem E72: :: ABCMIZ_0:70
for b1 being reflexive transitive antisymmetric with_suprema Noetherian non void adj-structured TAS-structure holds b1 @--> is strongly-normalizing
proof end;

theorem E73: :: ABCMIZ_0:71
for b1 being reflexive transitive antisymmetric with_suprema Noetherian non void adj-structured TAS-structure
for b2 being type of b1
for b3 being finite Subset of the adjectives of b1 st ( for b4 being Subset of the adjectives of b1 st b4 c= b3 & b4 is_properly_applicable_to b2 & b3 ast b2 = b4 ast b2 holds
b4 = b3 ) holds
for b4 being one-to-one FinSequence of the adjectives of b1 st rng b4 = b3 & b4 is_properly_applicable_to b2 holds
for b5 being natural number st 1 <= b5 & b5 <= len b4 holds
[((apply b4,b2) . (b5 + 1)),((apply b4,b2) . b5)] in b1 @-->
proof end;

theorem E74: :: ABCMIZ_0:72
for b1 being reflexive transitive antisymmetric with_suprema Noetherian non void adj-structured TAS-structure
for b2 being type of b1
for b3 being finite Subset of the adjectives of b1 st ( for b4 being Subset of the adjectives of b1 st b4 c= b3 & b4 is_properly_applicable_to b2 & b3 ast b2 = b4 ast b2 holds
b4 = b3 ) holds
for b4 being one-to-one FinSequence of the adjectives of b1 st rng b4 = b3 & b4 is_properly_applicable_to b2 holds
Rev (apply b4,b2) is RedSequence of b1 @-->
proof end;

theorem E75: :: ABCMIZ_0:73
for b1 being reflexive transitive antisymmetric with_suprema Noetherian non void adj-structured TAS-structure
for b2 being type of b1
for b3 being finite Subset of the adjectives of b1 st b3 is_properly_applicable_to b2 holds
b1 @--> reduces b3 ast b2,b2
proof end;

theorem E76: :: ABCMIZ_0:74
for b1 being non empty set
for b2 being Relation of b1
for b3 being RedSequence of b2 st b3 . 1 in b1 holds
b3 is FinSequence of b1
proof end;

theorem E77: :: ABCMIZ_0:75
for b1 being non empty set
for b2 being Relation of b1
for b3 being Element of b1
for b4 being set st b2 reduces b3,b4 holds
b4 in b1
proof end;

theorem E78: :: ABCMIZ_0:76
for b1 being non empty set
for b2 being Relation of b1 st b2 is with_UN_property & b2 is weakly-normalizing holds
for b3 being Element of b1 holds nf b3,b2 in b1
proof end;

theorem E79: :: ABCMIZ_0:77
for b1 being reflexive transitive antisymmetric with_suprema Noetherian non void adj-structured TAS-structure
for b2, b3 being type of b1 st b1 @--> reduces b2,b3 holds
ex b4 being finite Subset of the adjectives of b1 st
( b4 is_properly_applicable_to b3 & b2 = b4 ast b3 )
proof end;

theorem E80: :: ABCMIZ_0:78
for b1 being reflexive transitive antisymmetric with_suprema Noetherian non void adj-structured commutative TAS-structure holds
( b1 @--> is with_Church-Rosser_property & b1 @--> is with_UN_property )
proof end;

theorem E81: :: ABCMIZ_0:79
for b1 being non empty reflexive transitive antisymmetric with_suprema Noetherian non void adj-structured commutative TAS-structure
for b2 being type of b1 holds b1 @--> reduces b2, radix b2
proof end;

theorem E10: :: ABCMIZ_0:8
for b1, b2 being TA-structure st TA-structure(# the carrier of b1,the adjectives of b1,the InternalRel of b1,the non-op of b1,the adj-map of b1 #) = TA-structure(# the carrier of b2,the adjectives of b2,the InternalRel of b2,the non-op of b2,the adj-map of b2 #) & b1 is consistent holds
b2 is consistent
proof end;

theorem E82: :: ABCMIZ_0:80
for b1 being non empty reflexive transitive antisymmetric with_suprema Noetherian non void adj-structured commutative TAS-structure
for b2 being type of b1 holds b2 <= radix b2
proof end;

theorem E83: :: ABCMIZ_0:81
for b1 being non empty reflexive transitive antisymmetric with_suprema Noetherian non void adj-structured commutative TAS-structure
for b2 being type of b1
for b3 being set st b3 = { b4 where B is type of b1 : ex b1 being finite Subset of the adjectives of b1 st
( b5 is_properly_applicable_to b4 & b5 ast b4 = b2 ) } holds
( ex_sup_of b3,b1 & radix b2 = "\/" b3,b1 )
proof end;

theorem E84: :: ABCMIZ_0:82
for b1 being non empty reflexive transitive antisymmetric with_suprema Noetherian non void adj-structured commutative TAS-structure
for b2, b3 being type of b1
for b4 being adjective of b1 st b4 is_properly_applicable_to b2 & b4 ast b2 <= radix b3 holds
b2 <= radix b3
proof end;

theorem :: ABCMIZ_0:83
for b1 being non empty reflexive transitive antisymmetric with_suprema Noetherian non void adj-structured commutative TAS-structure
for b2, b3 being type of b1 st b2 <= b3 holds
radix b2 <= radix b3
proof end;

theorem :: ABCMIZ_0:84
for b1 being non empty reflexive transitive antisymmetric with_suprema Noetherian non void adj-structured commutative TAS-structure
for b2 being type of b1
for b3 being adjective of b1 st b3 is_properly_applicable_to b2 holds
radix (b3 ast b2) = radix b2
proof end;

theorem E11: :: ABCMIZ_0:9
for b1, b2 being non empty TA-structure st TA-structure(# the carrier of b1,the adjectives of b1,the InternalRel of b1,the non-op of b1,the adj-map of b1 #) = TA-structure(# the carrier of b2,the adjectives of b2,the InternalRel of b2,the non-op of b2,the adj-map of b2 #) & b1 is adj-structured holds
b2 is adj-structured
proof end;