theorem Th80: :: ABCMIZ_0:80

for T being non empty reflexive transitive antisymmetric with_suprema Noetherian non void adj-structured commutative TAS-structure
for t being type of T
for X being set st X = { t9 where t9 is type of T : ex A being finite Subset of the adjectives of T st
( A is_properly_applicable_to t9 & A ast t9 = t ) } holds
( ex_sup_of X,T & radix t = "\/" (X,T) )