:: ABCMIZ_0 semantic presentation

begin

registration
cluster1 -element reflexive  -> 1 -element complete for RelStr ;
coherence
 for b1 being 1 -element RelStr st b1 is reflexive holds
b1 is complete ;
end;

definition
let T be RelStr ;
mode type of T is Element of T;
end;

definition
let T be RelStr ;
attrT is Noetherian  means :Def1: :: ABCMIZ_0:def 1
 the InternalRel of T is co-well_founded ;
end;

:: deftheorem Def1 defines Noetherian ABCMIZ_0:def_1_:_
 for T being RelStr holds
( T is Noetherian iff the InternalRel of T is co-well_founded );

registration
cluster1 -element  -> 1 -element Noetherian for RelStr ;
coherence
 for b1 being 1 -element RelStr holds b1 is Noetherian
proof
let S be 1 -element RelStr ; ::_thesis: S is Noetherian
let Y be set ; :: according to REWRITE1:def_16,ABCMIZ_0:def_1 ::_thesis: ( not Y c= field the InternalRel of S or Y = {} or ex b1 being set st
( b1 in Y & ( for b2 being set holds
( not b2 in Y or b1 = b2 or not [b1,b2] in the InternalRel of S ) ) ) )
set R = the InternalRel of S;
assume A1: Y c= field the InternalRel of S ; ::_thesis: ( Y = {} or ex b1 being set st
( b1 in Y & ( for b2 being set holds
( not b2 in Y or b1 = b2 or not [b1,b2] in the InternalRel of S ) ) ) )
assume  Y <> {} ; ::_thesis: ex b1 being set st
( b1 in Y & ( for b2 being set holds
( not b2 in Y or b1 = b2 or not [b1,b2] in the InternalRel of S ) ) )
then reconsider X = Y as non empty set ;
set a = the Element of X;
take  the Element of X ; ::_thesis: ( the Element of X in Y & ( for b1 being set holds
( not b1 in Y or the Element of X = b1 or not [ the Element of X,b1] in the InternalRel of S ) ) )
thus  the Element of X in Y ; ::_thesis: for b1 being set holds
( not b1 in Y or the Element of X = b1 or not [ the Element of X,b1] in the InternalRel of S )
then A2: the Element of X in field the InternalRel of S by A1;
let b be set ; ::_thesis: ( not b in Y or the Element of X = b or not [ the Element of X,b] in the InternalRel of S )
A3: field the InternalRel of S c= the carrier of S \/ the carrier of S by RELSET_1:8;
assume  b in Y ; ::_thesis: ( the Element of X = b or not [ the Element of X,b] in the InternalRel of S )
then  b in field the InternalRel of S by A1;
hence  ( the Element of X = b or not [ the Element of X,b] in the InternalRel of S ) by A2, A3, ZFMISC_1:def_10; ::_thesis: verum
end;
end;

definition
let T be non empty RelStr ;
redefine attr T is Noetherian  means :Def2: :: ABCMIZ_0:def 2
 for A being non empty Subset of T ex a being Element of T st
( a in A & ( for b being Element of T st b in A holds
not a < b ) );
compatibility
 ( T is Noetherian iff for A being non empty Subset of T ex a being Element of T st
( a in A & ( for b being Element of T st b in A holds
not a < b ) ) )
proof
set R = the InternalRel of T;
thus  ( T is Noetherian implies for A being non empty Subset of T ex a being Element of T st
( a in A & ( for b being Element of T st b in A holds
not a < b ) ) ) ::_thesis: ( ( for A being non empty Subset of T ex a being Element of T st
( a in A & ( for b being Element of T st b in A holds
not a < b ) ) ) implies T is Noetherian )
proof
assume A1: for Y being set st Y c= field the InternalRel of T & Y <> {} holds
ex a being set st
( a in Y & ( for b being set st b in Y & a <> b holds
not [a,b] in the InternalRel of T ) ) ; :: according to REWRITE1:def_16,ABCMIZ_0:def_1 ::_thesis: for A being non empty Subset of T ex a being Element of T st
( a in A & ( for b being Element of T st b in A holds
not a < b ) )
let A be non empty Subset of T; ::_thesis: ex a being Element of T st
( a in A & ( for b being Element of T st b in A holds
not a < b ) )
set a = the Element of A;
reconsider a = the Element of A as Element of T ;
set Y = A /\ (field the InternalRel of T);
percases ( A misses field the InternalRel of T or A meets field the InternalRel of T ) ;
supposeA2: A misses field the InternalRel of T ; ::_thesis: ex a being Element of T st
( a in A & ( for b being Element of T st b in A holds
not a < b ) )
take  a ; ::_thesis: ( a in A & ( for b being Element of T st b in A holds
not a < b ) )
thus  a in A ; ::_thesis: for b being Element of T st b in A holds
not a < b
let b be Element of T; ::_thesis: ( b in A implies not a < b )
assume that
 b in A and
A3: a < b ; ::_thesis: contradiction
 a <= b by A3, ORDERS_2:def_6;
then  [a,b] in the InternalRel of T by ORDERS_2:def_5;
then  a in field the InternalRel of T by RELAT_1:15;
hence  contradiction by A2, XBOOLE_0:3; ::_thesis: verum
end;
suppose A meets field the InternalRel of T ; ::_thesis: ex a being Element of T st
( a in A & ( for b being Element of T st b in A holds
not a < b ) )
then  A /\ (field the InternalRel of T) <> {} by XBOOLE_0:def_7;
then consider x being set  such that
A4: x in A /\ (field the InternalRel of T) and
A5: for y being set st y in A /\ (field the InternalRel of T) & x <> y holds
not [x,y] in the InternalRel of T by A1, XBOOLE_1:17;
reconsider x = x as Element of T by A4;
take  x ; ::_thesis: ( x in A & ( for b being Element of T st b in A holds
not x < b ) )
thus  x in A by A4, XBOOLE_0:def_4; ::_thesis: for b being Element of T st b in A holds
not x < b
let b be Element of T; ::_thesis: ( b in A implies not x < b )
assume that
A6: b in A and
A7: x < b ; ::_thesis: contradiction
 x <= b by A7, ORDERS_2:def_6;
then A8: [x,b] in the InternalRel of T by ORDERS_2:def_5;
then  b in field the InternalRel of T by RELAT_1:15;
then  b in A /\ (field the InternalRel of T) by A6, XBOOLE_0:def_4;
hence  contradiction by A5, A7, A8; ::_thesis: verum
end;
end;
end;
assume A9: for A being non empty Subset of T ex a being Element of T st
( a in A & ( for b being Element of T st b in A holds
not a < b ) ) ; ::_thesis: T is Noetherian
let Y be set ; :: according to REWRITE1:def_16,ABCMIZ_0:def_1 ::_thesis: ( not Y c= field the InternalRel of T or Y = {} or ex b1 being set st
( b1 in Y & ( for b2 being set holds
( not b2 in Y or b1 = b2 or not [b1,b2] in the InternalRel of T ) ) ) )
assume that
A10: Y c= field the InternalRel of T and
A11: Y <> {} ; ::_thesis: ex b1 being set st
( b1 in Y & ( for b2 being set holds
( not b2 in Y or b1 = b2 or not [b1,b2] in the InternalRel of T ) ) )
 field the InternalRel of T c= the carrier of T \/ the carrier of T by RELSET_1:8;
then reconsider A = Y as non empty Subset of T by A10, A11, XBOOLE_1:1;
consider a being Element of T such that
A12: a in A and
A13: for b being Element of T st b in A holds
not a < b by A9;
take  a ; ::_thesis: ( a in Y & ( for b1 being set holds
( not b1 in Y or a = b1 or not [a,b1] in the InternalRel of T ) ) )
thus  a in Y by A12; ::_thesis: for b1 being set holds
( not b1 in Y or a = b1 or not [a,b1] in the InternalRel of T )
let b be set ; ::_thesis: ( not b in Y or a = b or not [a,b] in the InternalRel of T )
assume that
A14: b in Y and
A15: a <> b ; ::_thesis: not [a,b] in the InternalRel of T
 b in A by A14;
then reconsider b = b as Element of T ;
 not a < b by A13, A14;
then  not a <= b by A15, ORDERS_2:def_6;
hence  not [a,b] in the InternalRel of T by ORDERS_2:def_5; ::_thesis: verum
end;
end;

:: deftheorem Def2 defines Noetherian ABCMIZ_0:def_2_:_
 for T being non empty RelStr holds
( T is Noetherian iff for A being non empty Subset of T ex a being Element of T st
( a in A & ( for b being Element of T st b in A holds
not a < b ) ) );

definition
let T be Poset;
attrT is Mizar-widening-like  means :: ABCMIZ_0:def 3
( T is sup-Semilattice & T is Noetherian );
end;

:: deftheorem  defines Mizar-widening-like ABCMIZ_0:def_3_:_
 for T being Poset holds
( T is Mizar-widening-like iff ( T is sup-Semilattice & T is Noetherian ) );

registration
cluster reflexive transitive antisymmetric Mizar-widening-like  ->  with_suprema upper-bounded Noetherian for RelStr ;
coherence
 for b1 being Poset st b1 is Mizar-widening-like holds
( b1 is Noetherian & b1 is with_suprema & b1 is upper-bounded )
proof
let T be Poset; ::_thesis: ( T is Mizar-widening-like implies ( T is Noetherian & T is with_suprema & T is upper-bounded ) )
assume that
A1: T is sup-Semilattice and
A2: T is Noetherian ; :: according to ABCMIZ_0:def_3 ::_thesis: ( T is Noetherian & T is with_suprema & T is upper-bounded )
reconsider S = T as sup-Semilattice by A1;
 the carrier of S c= the carrier of S ;
then consider a being Element of T such that
 a in the carrier of T and
A3: for b being Element of T st b in the carrier of T holds
not a < b by A2, Def2;
thus  ( T is Noetherian & T is with_suprema ) by A1, A2; ::_thesis: T is upper-bounded
take  a ; :: according to YELLOW_0:def_5 ::_thesis: the carrier of T is_<=_than a
let b be Element of T; :: according to LATTICE3:def_9 ::_thesis: ( not b in the carrier of T or b <= a )
A4: a "\/" b in the carrier of S ;
then A5: a "\/" b >= a by YELLOW_0:22;
 not a < a "\/" b by A3, A4;
then  a "\/" b = a by A5, ORDERS_2:def_6;
hence  ( not b in the carrier of T or b <= a ) by A1, YELLOW_0:22; ::_thesis: verum
end;
end;

registration
cluster reflexive transitive antisymmetric with_suprema Noetherian  ->  Mizar-widening-like for RelStr ;
coherence
 for b1 being sup-Semilattice st b1 is Noetherian holds
b1 is Mizar-widening-like
proof
let T be sup-Semilattice; ::_thesis: ( T is Noetherian implies T is Mizar-widening-like )
assume A1: T is Noetherian ; ::_thesis: T is Mizar-widening-like
thus  T is sup-Semilattice ; :: according to ABCMIZ_0:def_3 ::_thesis: T is Noetherian
thus  T is Noetherian by A1; ::_thesis: verum
end;
end;

registration
cluster non empty reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded V139() up-complete /\-complete Mizar-widening-like for RelStr ;
existence
 ex b1 being complete sup-Semilattice st b1 is Mizar-widening-like
proof
set T = the 1 -element LATTICE;
take  the 1 -element LATTICE ; ::_thesis: the 1 -element LATTICE is Mizar-widening-like
thus  the 1 -element LATTICE is sup-Semilattice ; :: according to ABCMIZ_0:def_3 ::_thesis: the 1 -element LATTICE is Noetherian
thus  the 1 -element LATTICE is Noetherian ; ::_thesis: verum
end;
end;

registration
let T be Noetherian RelStr ;
cluster the InternalRel of T ->  co-well_founded ;
coherence
 the InternalRel of T is co-well_founded by Def1;
end;

theorem Th1: :: ABCMIZ_0:1
for T being Noetherian sup-Semilattice
for I being Ideal of T holds
( ex_sup_of I,T & sup I in I )
proof
let T be Noetherian sup-Semilattice; ::_thesis: for I being Ideal of T holds
( ex_sup_of I,T & sup I in I )
let I be Ideal of T; ::_thesis: ( ex_sup_of I,T & sup I in I )
consider a being Element of T such that
A1: a in I and
A2: for b being Element of T st b in I holds
not a < b by Def2;
A3: I is_<=_than a
proof
let d be Element of T; :: according to LATTICE3:def_9 ::_thesis: ( not d in I or d <= a )
assume  d in I ; ::_thesis: d <= a
then  a "\/" d in I by A1, WAYBEL_0:40;
then A4: not a < a "\/" d by A2;
 a <= a "\/" d by YELLOW_0:22;
then  a = a "\/" d by A4, ORDERS_2:def_6;
hence  d <= a by YELLOW_0:22; ::_thesis: verum
end;
 for c being Element of T st I is_<=_than c holds
a <= c by A1, LATTICE3:def_9;
hence  ( ex_sup_of I,T & sup I in I ) by A1, A3, YELLOW_0:30; ::_thesis: verum
end;

begin

definition
attrc1 is strict ;
struct AdjectiveStr  -> ;
aggrAdjectiveStr(# adjectives, non-op #) ->  AdjectiveStr ;
sel adjectives c1 ->  set ;
sel non-op c1 ->  UnOp of the adjectives of c1;
end;

definition
let A be AdjectiveStr ;
attrA is void  means :Def4: :: ABCMIZ_0:def 4
 the adjectives of A is empty ;
mode adjective of A is Element of the adjectives of A;
end;

:: deftheorem Def4 defines void ABCMIZ_0:def_4_:_
 for A being AdjectiveStr holds
( A is void iff the adjectives of A is empty );

theorem :: ABCMIZ_0:2
for A1, A2 being AdjectiveStr st the adjectives of A1 = the adjectives of A2 & A1 is void holds
A2 is void
proof
let A1, A2 be AdjectiveStr ; ::_thesis: ( the adjectives of A1 = the adjectives of A2 & A1 is void implies A2 is void )
assume A1: the adjectives of A1 = the adjectives of A2 ; ::_thesis: ( not A1 is void or A2 is void )
assume  the adjectives of A1 is empty ; :: according to ABCMIZ_0:def_4 ::_thesis: A2 is void
hence  the adjectives of A2 is empty by A1; :: according to ABCMIZ_0:def_4 ::_thesis: verum
end;

definition
let A be AdjectiveStr ;
let a be Element of the adjectives of A;
func non- a ->  adjective of A equals :: ABCMIZ_0:def 5
 the non-op of A . a;
coherence
 the non-op of A . a is adjective of A
proof
percases ( the adjectives of A is empty or not the adjectives of A is empty ) ;
supposeA1: the adjectives of A is empty ; ::_thesis: the non-op of A . a is adjective of A
then A2: dom the non-op of A = the adjectives of A ;
 a = {} by A1, SUBSET_1:def_1;
hence  the non-op of A . a is adjective of A by A1, A2, FUNCT_1:def_2; ::_thesis: verum
end;
suppose not the adjectives of A is empty ; ::_thesis: the non-op of A . a is adjective of A
hence  the non-op of A . a is adjective of A by FUNCT_2:5; ::_thesis: verum
end;
end;
end;
end;

:: deftheorem  defines non- ABCMIZ_0:def_5_:_
 for A being AdjectiveStr
for a being Element of the adjectives of A holds non- a = the non-op of A . a;

theorem :: ABCMIZ_0:3
for A1, A2 being AdjectiveStr st AdjectiveStr(# the adjectives of A1, the non-op of A1 #) = AdjectiveStr(# the adjectives of A2, the non-op of A2 #) holds
for a1 being adjective of A1
for a2 being adjective of A2 st a1 = a2 holds
non- a1 = non- a2 ;

definition
let A be AdjectiveStr ;
attrA is involutive  means :Def6: :: ABCMIZ_0:def 6
 for a being adjective of A holds non- (non- a) = a;
attrA is without_fixpoints  means :: ABCMIZ_0:def 7
 for a being adjective of A holds not non- a = a;
end;

:: deftheorem Def6 defines involutive ABCMIZ_0:def_6_:_
 for A being AdjectiveStr holds
( A is involutive iff for a being adjective of A holds non- (non- a) = a );

:: deftheorem  defines without_fixpoints ABCMIZ_0:def_7_:_
 for A being AdjectiveStr holds
( A is without_fixpoints iff for a being adjective of A holds not non- a = a );

theorem Th4: :: ABCMIZ_0:4
for a1, a2 being set st a1 <> a2 holds
for A being AdjectiveStr st the adjectives of A = {a1,a2} & the non-op of A . a1 = a2 & the non-op of A . a2 = a1 holds
( not A is void & A is involutive & A is without_fixpoints )
proof
let a1, a2 be set ; ::_thesis: ( a1 <> a2 implies for A being AdjectiveStr st the adjectives of A = {a1,a2} & the non-op of A . a1 = a2 & the non-op of A . a2 = a1 holds
( not A is void & A is involutive & A is without_fixpoints ) )
assume A1: a1 <> a2 ; ::_thesis: for A being AdjectiveStr st the adjectives of A = {a1,a2} & the non-op of A . a1 = a2 & the non-op of A . a2 = a1 holds
( not A is void & A is involutive & A is without_fixpoints )
let A be AdjectiveStr ; ::_thesis: ( the adjectives of A = {a1,a2} & the non-op of A . a1 = a2 & the non-op of A . a2 = a1 implies ( not A is void & A is involutive & A is without_fixpoints ) )
assume that
A2: the adjectives of A = {a1,a2} and
A3: the non-op of A . a1 = a2 and
A4: the non-op of A . a2 = a1 ; ::_thesis: ( not A is void & A is involutive & A is without_fixpoints )
thus  not the adjectives of A is empty by A2; :: according to ABCMIZ_0:def_4 ::_thesis: ( A is involutive & A is without_fixpoints )
hereby  :: according to ABCMIZ_0:def_6 ::_thesis: A is without_fixpoints
let a be adjective of A; ::_thesis: non- (non- a) = a
 ( a = a1 or a = a2 ) by A2, TARSKI:def_2;
hence  non- (non- a) = a by A3, A4; ::_thesis: verum
end;
let a be adjective of A; :: according to ABCMIZ_0:def_7 ::_thesis: not non- a = a
assume A5: non- a = a ; ::_thesis: contradiction
 ( a = a1 or a = a2 ) by A2, TARSKI:def_2;
hence  contradiction by A1, A3, A4, A5; ::_thesis: verum
end;

theorem Th5: :: ABCMIZ_0:5
for A1, A2 being AdjectiveStr st AdjectiveStr(# the adjectives of A1, the non-op of A1 #) = AdjectiveStr(# the adjectives of A2, the non-op of A2 #) & A1 is involutive holds
A2 is involutive
proof
let A1, A2 be AdjectiveStr ; ::_thesis: ( AdjectiveStr(# the adjectives of A1, the non-op of A1 #) = AdjectiveStr(# the adjectives of A2, the non-op of A2 #) & A1 is involutive implies A2 is involutive )
assume A1: AdjectiveStr(# the adjectives of A1, the non-op of A1 #) = AdjectiveStr(# the adjectives of A2, the non-op of A2 #) ; ::_thesis: ( not A1 is involutive or A2 is involutive )
assume A2: for a being adjective of A1 holds non- (non- a) = a ; :: according to ABCMIZ_0:def_6 ::_thesis: A2 is involutive
let a be adjective of A2; :: according to ABCMIZ_0:def_6 ::_thesis: non- (non- a) = a
reconsider b = a as adjective of A1 by A1;
thus  non- (non- a) = non- (non- b) by A1
.= a by A2 ; ::_thesis: verum
end;

theorem Th6: :: ABCMIZ_0:6
for A1, A2 being AdjectiveStr st AdjectiveStr(# the adjectives of A1, the non-op of A1 #) = AdjectiveStr(# the adjectives of A2, the non-op of A2 #) & A1 is without_fixpoints holds
A2 is without_fixpoints
proof
let A1, A2 be AdjectiveStr ; ::_thesis: ( AdjectiveStr(# the adjectives of A1, the non-op of A1 #) = AdjectiveStr(# the adjectives of A2, the non-op of A2 #) & A1 is without_fixpoints implies A2 is without_fixpoints )
assume A1: AdjectiveStr(# the adjectives of A1, the non-op of A1 #) = AdjectiveStr(# the adjectives of A2, the non-op of A2 #) ; ::_thesis: ( not A1 is without_fixpoints or A2 is without_fixpoints )
assume A2: for a being adjective of A1 holds not non- a = a ; :: according to ABCMIZ_0:def_7 ::_thesis: A2 is without_fixpoints
given a being adjective of A2 such that A3: non- a = a ; :: according to ABCMIZ_0:def_7 ::_thesis: contradiction
reconsider b = a as adjective of A1 by A1;
 non- b = b by A1, A3;
hence  contradiction by A2; ::_thesis: verum
end;

registration
cluster strict non void involutive without_fixpoints for AdjectiveStr ;
existence
 ex b1 being strict AdjectiveStr st
( not b1 is void & b1 is involutive & b1 is without_fixpoints )
proof
reconsider x = 0 , y = 1 as Element of {0,1} by TARSKI:def_2;
reconsider n = (0,1) --> (y,x) as UnOp of {0,1} ;
take  AdjectiveStr(# {0,1},n #) ; ::_thesis: ( not AdjectiveStr(# {0,1},n #) is void & AdjectiveStr(# {0,1},n #) is involutive & AdjectiveStr(# {0,1},n #) is without_fixpoints )
A1: n . y = x by FUNCT_4:63;
 n . x = y by FUNCT_4:63;
hence  ( not AdjectiveStr(# {0,1},n #) is void & AdjectiveStr(# {0,1},n #) is involutive & AdjectiveStr(# {0,1},n #) is without_fixpoints ) by A1, Th4; ::_thesis: verum
end;
end;

registration
let A be non void AdjectiveStr ;
cluster the adjectives of A ->  non empty ;
coherence
 not the adjectives of A is empty by Def4;
end;

definition
attrc1 is strict ;
struct TA-structure  ->  RelStr , AdjectiveStr ;
aggrTA-structure(# carrier, adjectives, InternalRel, non-op, adj-map #) ->  TA-structure ;
sel adj-map c1 ->  Function of the carrier of c1,(Fin the adjectives of c1);
end;

registration
let X be non empty set ;
let A be set ;
let r be Relation of X;
let n be UnOp of A;
let a be Function of X,(Fin A);
cluster TA-structure(# X,A,r,n,a #) ->  non empty ;
coherence
 not TA-structure(# X,A,r,n,a #) is empty ;
end;

registration
let X be set ;
let A be non empty set ;
let r be Relation of X;
let n be UnOp of A;
let a be Function of X,(Fin A);
cluster TA-structure(# X,A,r,n,a #) ->  non void ;
coherence
 not TA-structure(# X,A,r,n,a #) is void by Def4;
end;

registration
cluster1 -element reflexive non void involutive without_fixpoints strict for TA-structure ;
existence
 ex b1 being TA-structure st
( b1 is 1 -element & b1 is reflexive & not b1 is void & b1 is involutive & b1 is without_fixpoints & b1 is strict )
proof
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 )
 the carrier of T is 1 -element ;
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
end;
end;

definition
let T be TA-structure ;
let t be Element of T;
func adjs t ->  Subset of the adjectives of T equals :: ABCMIZ_0:def 8
 the adj-map of T . t;
coherence
 the adj-map of T . t is Subset of the adjectives of T
proof
percases ( the carrier of T is empty or not the carrier of T is empty ) ;
supposeA1: the carrier of T is empty ; ::_thesis: the adj-map of T . t is Subset of the adjectives of T
then  dom the adj-map of T = the carrier of T ;
then  the adj-map of T . t = {} the adjectives of T by A1, FUNCT_1:def_2;
hence  the adj-map of T . t is Subset of the adjectives of T ; ::_thesis: verum
end;
suppose not the carrier of T is empty ; ::_thesis: the adj-map of T . t is Subset of the adjectives of T
then  the adj-map of T . t in Fin the adjectives of T by FUNCT_2:5;
hence  the adj-map of T . t is Subset of the adjectives of T by FINSUB_1:17; ::_thesis: verum
end;
end;
end;
end;

:: deftheorem  defines adjs ABCMIZ_0:def_8_:_
 for T being TA-structure
for t being Element of T holds adjs t = the adj-map of T . t;

theorem :: ABCMIZ_0:7
for T1, T2 being TA-structure st TA-structure(# the carrier of T1, the adjectives of T1, the InternalRel of T1, the non-op of T1, the adj-map of T1 #) = TA-structure(# the carrier of T2, the adjectives of T2, the InternalRel of T2, the non-op of T2, the adj-map of T2 #) holds
for t1 being type of T1
for t2 being type of T2 st t1 = t2 holds
adjs t1 = adjs t2 ;

definition
let T be TA-structure ;
attrT is consistent  means :Def9: :: ABCMIZ_0:def 9
 for t being type of T
for a being adjective of T st a in adjs t holds
not non- a in adjs t;
end;

:: deftheorem Def9 defines consistent ABCMIZ_0:def_9_:_
 for T being TA-structure holds
( T is consistent iff for t being type of T
for a being adjective of T st a in adjs t holds
not non- a in adjs t );

theorem Th8: :: ABCMIZ_0:8
for T1, T2 being TA-structure st TA-structure(# the carrier of T1, the adjectives of T1, the InternalRel of T1, the non-op of T1, the adj-map of T1 #) = TA-structure(# the carrier of T2, the adjectives of T2, the InternalRel of T2, the non-op of T2, the adj-map of T2 #) & T1 is consistent holds
T2 is consistent
proof
let T1, T2 be TA-structure ; ::_thesis: ( TA-structure(# the carrier of T1, the adjectives of T1, the InternalRel of T1, the non-op of T1, the adj-map of T1 #) = TA-structure(# the carrier of T2, the adjectives of T2, the InternalRel of T2, the non-op of T2, the adj-map of T2 #) & T1 is consistent implies T2 is consistent )
assume that
A1: TA-structure(# the carrier of T1, the adjectives of T1, the InternalRel of T1, the non-op of T1, the adj-map of T1 #) = TA-structure(# the carrier of T2, the adjectives of T2, the InternalRel of T2, the non-op of T2, the adj-map of T2 #) and
A2: for t being type of T1
for a being adjective of T1 st a in adjs t holds
not non- a in adjs t ; :: according to ABCMIZ_0:def_9 ::_thesis: T2 is consistent
let t2 be type of T2; :: according to ABCMIZ_0:def_9 ::_thesis: for a being adjective of T2 st a in adjs t2 holds
not non- a in adjs t2
let a2 be adjective of T2; ::_thesis: ( a2 in adjs t2 implies not non- a2 in adjs t2 )
reconsider a1 = a2 as adjective of T1 by A1;
reconsider t1 = t2 as type of T1 by A1;
assume  a2 in adjs t2 ; ::_thesis: not non- a2 in adjs t2
then  not non- a1 in adjs t1 by A1, A2;
hence  not non- a2 in adjs t2 by A1; ::_thesis: verum
end;

definition
let T be non empty TA-structure ;
attrT is adj-structured  means :: ABCMIZ_0:def 10
 the adj-map of T is join-preserving Function of T,((BoolePoset the adjectives of T) opp);
end;

:: deftheorem  defines adj-structured ABCMIZ_0:def_10_:_
 for T being non empty TA-structure holds
( T is adj-structured iff the adj-map of T is join-preserving Function of T,((BoolePoset the adjectives of T) opp) );

theorem Th9: :: ABCMIZ_0:9
for T1, T2 being non empty TA-structure st TA-structure(# the carrier of T1, the adjectives of T1, the InternalRel of T1, the non-op of T1, the adj-map of T1 #) = TA-structure(# the carrier of T2, the adjectives of T2, the InternalRel of T2, the non-op of T2, the adj-map of T2 #) & T1 is adj-structured holds
T2 is adj-structured
proof
let T1, T2 be non empty TA-structure ; ::_thesis: ( TA-structure(# the carrier of T1, the adjectives of T1, the InternalRel of T1, the non-op of T1, the adj-map of T1 #) = TA-structure(# the carrier of T2, the adjectives of T2, the InternalRel of T2, the non-op of T2, the adj-map of T2 #) & T1 is adj-structured implies T2 is adj-structured )
assume A1: TA-structure(# the carrier of T1, the adjectives of T1, the InternalRel of T1, the non-op of T1, the adj-map of T1 #) = TA-structure(# the carrier of T2, the adjectives of T2, the InternalRel of T2, the non-op of T2, the adj-map of T2 #) ; ::_thesis: ( not T1 is adj-structured or T2 is adj-structured )
assume  the adj-map of T1 is join-preserving Function of T1,((BoolePoset the adjectives of T1) opp) ; :: according to ABCMIZ_0:def_10 ::_thesis: T2 is adj-structured
then reconsider f = the adj-map of T1 as join-preserving Function of T1,((BoolePoset the adjectives of T1) opp) ;
reconsider g = f as Function of T2,((BoolePoset the adjectives of T2) opp) by A1;
A2: RelStr(# the carrier of T1, the InternalRel of T1 #) = RelStr(# the carrier of T2, the InternalRel of T2 #) by A1;
 g is join-preserving
proof
let x, y be type of T2; :: according to WAYBEL_0:def_35 ::_thesis: g preserves_sup_of {x,y}
reconsider x9 = x, y9 = y as type of T1 by A1;
assume A3: ex_sup_of {x,y},T2 ; :: according to WAYBEL_0:def_31 ::_thesis: ( ex_sup_of g .: {x,y},(BoolePoset the adjectives of T2) opp & "\/" ((g .: {x,y}),((BoolePoset the adjectives of T2) opp)) = g . ("\/" ({x,y},T2)) )
then A4: ex_sup_of {x9,y9},T1 by A2, YELLOW_0:14;
A5: f preserves_sup_of {x9,y9} by WAYBEL_0:def_35;
hence  ex_sup_of g .: {x,y},(BoolePoset the adjectives of T2) opp by A1, A4, WAYBEL_0:def_31; ::_thesis: "\/" ((g .: {x,y}),((BoolePoset the adjectives of T2) opp)) = g . ("\/" ({x,y},T2))
 sup (f .: {x9,y9}) = f . (sup {x9,y9}) by A4, A5, WAYBEL_0:def_31;
hence  "\/" ((g .: {x,y}),((BoolePoset the adjectives of T2) opp)) = g . ("\/" ({x,y},T2)) by A1, A2, A3, YELLOW_0:26; ::_thesis: verum
end;
hence  the adj-map of T2 is join-preserving Function of T2,((BoolePoset the adjectives of T2) opp) by A1; :: according to ABCMIZ_0:def_10 ::_thesis: verum
end;

definition
let T be reflexive transitive antisymmetric with_suprema TA-structure ;
redefine attr T is adj-structured  means :Def11: :: ABCMIZ_0:def 11
 for t1, t2 being type of T holds adjs (t1 "\/" t2) = (adjs t1) /\ (adjs t2);
compatibility
 ( T is adj-structured iff for t1, t2 being type of T holds adjs (t1 "\/" t2) = (adjs t1) /\ (adjs t2) )
proof
A1: dom the adj-map of T = the carrier of T by FUNCT_2:def_1;
A2: Fin the adjectives of T c= bool the adjectives of T by FINSUB_1:13;
BoolePoset the adjectives of T = InclPoset (bool the adjectives of T) by YELLOW_1:4
.= RelStr(# (bool the adjectives of T),(RelIncl (bool the adjectives of T)) #) by YELLOW_1:def_1 ;
then  rng the adj-map of T c= the carrier of ((BoolePoset the adjectives of T) opp) by A2, XBOOLE_1:1;
then reconsider f = the adj-map of T as Function of T,((BoolePoset the adjectives of T) opp) by A1, FUNCT_2:2;
thus  ( T is adj-structured implies for t1, t2 being type of T holds adjs (t1 "\/" t2) = (adjs t1) /\ (adjs t2) ) ::_thesis: ( ( for t1, t2 being type of T holds adjs (t1 "\/" t2) = (adjs t1) /\ (adjs t2) ) implies T is adj-structured )
proof
assume  the adj-map of T is join-preserving Function of T,((BoolePoset the adjectives of T) opp) ; :: according to ABCMIZ_0:def_10 ::_thesis: for t1, t2 being type of T holds adjs (t1 "\/" t2) = (adjs t1) /\ (adjs t2)
then reconsider f = the adj-map of T as join-preserving Function of T,((BoolePoset the adjectives of T) opp) ;
let t1, t2 be type of T; ::_thesis: adjs (t1 "\/" t2) = (adjs t1) /\ (adjs t2)
thus  adjs (t1 "\/" t2) = (f . t1) "\/" (f . t2) by WAYBEL_6:2
.= (~ (f . t1)) "/\" (~ (f . t2)) by YELLOW_7:22
.= (adjs t1) /\ (adjs t2) by YELLOW_1:17 ; ::_thesis: verum
end;
assume A3: for t1, t2 being type of T holds adjs (t1 "\/" t2) = (adjs t1) /\ (adjs t2) ; ::_thesis: T is adj-structured
now__::_thesis:_for_t1,_t2_being_type_of_T_holds_f_._(t1_"\/"_t2)_=_(f_._t1)_"\/"_(f_._t2)
let t1, t2 be type of T; ::_thesis: f . (t1 "\/" t2) = (f . t1) "\/" (f . t2)
thus f . (t1 "\/" t2) = adjs (t1 "\/" t2)
.= (adjs t1) /\ (adjs t2) by A3
.= (~ (f . t1)) "/\" (~ (f . t2)) by YELLOW_1:17
.= (f . t1) "\/" (f . t2) by YELLOW_7:22 ; ::_thesis: verum
end;
hence  the adj-map of T is join-preserving Function of T,((BoolePoset the adjectives of T) opp) by WAYBEL_6:2; :: according to ABCMIZ_0:def_10 ::_thesis: verum
end;
end;

:: deftheorem Def11 defines adj-structured ABCMIZ_0:def_11_:_
 for T being reflexive transitive antisymmetric with_suprema TA-structure holds
( T is adj-structured iff for t1, t2 being type of T holds adjs (t1 "\/" t2) = (adjs t1) /\ (adjs t2) );

theorem Th10: :: ABCMIZ_0:10
for T being reflexive transitive antisymmetric with_suprema TA-structure st T is adj-structured holds
for t1, t2 being type of T st t1 <= t2 holds
adjs t2 c= adjs t1
proof
let T be reflexive transitive antisymmetric with_suprema TA-structure ; ::_thesis: ( T is adj-structured implies for t1, t2 being type of T st t1 <= t2 holds
adjs t2 c= adjs t1 )
assume A1: for t1, t2 being type of T holds adjs (t1 "\/" t2) = (adjs t1) /\ (adjs t2) ; :: according to ABCMIZ_0:def_11 ::_thesis: for t1, t2 being type of T st t1 <= t2 holds
adjs t2 c= adjs t1
let t1, t2 be type of T; ::_thesis: ( t1 <= t2 implies adjs t2 c= adjs t1 )
assume  t1 <= t2 ; ::_thesis: adjs t2 c= adjs t1
then  t1 "\/" t2 = t2 by YELLOW_0:24;
then  adjs t2 = (adjs t1) /\ (adjs t2) by A1;
hence  adjs t2 c= adjs t1 by XBOOLE_1:17; ::_thesis: verum
end;

definition
let T be TA-structure ;
let a be Element of the adjectives of T;
func types a ->  Subset of T means :Def12: :: ABCMIZ_0:def 12
 for x being set holds
( x in it iff ex t being type of T st
( x = t & a in adjs t ) );
existence
 ex b1 being Subset of T st
for x being set holds
( x in b1 iff ex t being type of T st
( x = t & a in adjs t ) )
proof
defpred S1[ set ] means  ex t being type of T st
( $1 = t & a in adjs t );
consider tt being set  such that
A1: for x being set holds
( x in tt iff ( x in the carrier of T & S1[x] ) ) from XBOOLE_0:sch_1();
 tt c= the carrier of T
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in tt or x in the carrier of T )
thus  ( not x in tt or x in the carrier of T ) by A1; ::_thesis: verum
end;
then reconsider tt = tt as Subset of T ;
take  tt ; ::_thesis: for x being set holds
( x in tt iff ex t being type of T st
( x = t & a in adjs t ) )
let x be set ; ::_thesis: ( x in tt iff ex t being type of T st
( x = t & a in adjs t ) )
thus  ( x in tt implies ex t being type of T st
( x = t & a in adjs t ) ) by A1; ::_thesis: ( ex t being type of T st
( x = t & a in adjs t ) implies x in tt )
given t being type of T such that A2: x = t and
A3: a in adjs t ; ::_thesis: x in tt
now__::_thesis:_x_in_the_carrier_of_T
A4: dom the adj-map of T = the carrier of T by FUNCT_2:def_1;
assume  not x in the carrier of T ; ::_thesis: contradiction
hence  contradiction by A2, A3, A4, FUNCT_1:def_2; ::_thesis: verum
end;
hence  x in tt by A1, A2, A3; ::_thesis: verum
end;
uniqueness
 for b1, b2 being Subset of T st ( for x being set holds
( x in b1 iff ex t being type of T st
( x = t & a in adjs t ) ) ) & ( for x being set holds
( x in b2 iff ex t being type of T st
( x = t & a in adjs t ) ) ) holds
b1 = b2
proof
defpred S1[ set ] means  ex t being type of T st
( $1 = t & a in adjs t );
let X1, X2 be Subset of T; ::_thesis: ( ( for x being set holds
( x in X1 iff ex t being type of T st
( x = t & a in adjs t ) ) ) & ( for x being set holds
( x in X2 iff ex t being type of T st
( x = t & a in adjs t ) ) ) implies X1 = X2 )
assume that
A5: for x being set holds
( x in X1 iff S1[x] ) and
A6: for x being set holds
( x in X2 iff S1[x] ) ; ::_thesis: X1 = X2
thus  X1 = X2 from XBOOLE_0:sch_2(A5, A6); ::_thesis: verum
end;
end;

:: deftheorem Def12 defines types ABCMIZ_0:def_12_:_
 for T being TA-structure
for a being Element of the adjectives of T
for b3 being Subset of T holds
( b3 = types a iff for x being set holds
( x in b3 iff ex t being type of T st
( x = t & a in adjs t ) ) );

definition
let T be non empty TA-structure ;
let A be Subset of the adjectives of T;
func types A ->  Subset of T means :Def13: :: ABCMIZ_0:def 13
 for t being type of T holds
( t in it iff for a being adjective of T st a in A holds
t in types a );
existence
 ex b1 being Subset of T st
for t being type of T holds
( t in b1 iff for a being adjective of T st a in A holds
t in types a )
proof
defpred S1[ set ] means  for a being adjective of T st a in A holds
$1 in types a;
consider tt being set  such that
A1: for x being set holds
( x in tt iff ( x in the carrier of T & S1[x] ) ) from XBOOLE_0:sch_1();
 tt c= the carrier of T
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in tt or x in the carrier of T )
thus  ( not x in tt or x in the carrier of T ) by A1; ::_thesis: verum
end;
then reconsider tt = tt as Subset of T ;
take  tt ; ::_thesis: for t being type of T holds
( t in tt iff for a being adjective of T st a in A holds
t in types a )
thus  for t being type of T holds
( t in tt iff for a being adjective of T st a in A holds
t in types a ) by A1; ::_thesis: verum
end;
uniqueness
 for b1, b2 being Subset of T st ( for t being type of T holds
( t in b1 iff for a being adjective of T st a in A holds
t in types a ) ) & ( for t being type of T holds
( t in b2 iff for a being adjective of T st a in A holds
t in types a ) ) holds
b1 = b2
proof
let X1, X2 be Subset of T; ::_thesis: ( ( for t being type of T holds
( t in X1 iff for a being adjective of T st a in A holds
t in types a ) ) & ( for t being type of T holds
( t in X2 iff for a being adjective of T st a in A holds
t in types a ) ) implies X1 = X2 )
assume that
A2: for t being type of T holds
( t in X1 iff for a being adjective of T st a in A holds
t in types a ) and
A3: for t being type of T holds
( t in X2 iff for a being adjective of T st a in A holds
t in types a ) ; ::_thesis: X1 = X2
now__::_thesis:_for_x_being_set_holds_
(_x_in_X1_iff_x_in_X2_)
let x be set ; ::_thesis: ( x in X1 iff x in X2 )
 ( x in X1 iff ( x is type of T & ( for a being adjective of T st a in A holds
x in types a ) ) ) by A2;
hence  ( x in X1 iff x in X2 ) by A3; ::_thesis: verum
end;
hence  X1 = X2 by TARSKI:1; ::_thesis: verum
end;
end;

:: deftheorem Def13 defines types ABCMIZ_0:def_13_:_
 for T being non empty TA-structure
for A being Subset of the adjectives of T
for b3 being Subset of T holds
( b3 = types A iff for t being type of T holds
( t in b3 iff for a being adjective of T st a in A holds
t in types a ) );

theorem Th11: :: ABCMIZ_0:11
for T1, T2 being TA-structure st TA-structure(# the carrier of T1, the adjectives of T1, the InternalRel of T1, the non-op of T1, the adj-map of T1 #) = TA-structure(# the carrier of T2, the adjectives of T2, the InternalRel of T2, the non-op of T2, the adj-map of T2 #) holds
for a1 being adjective of T1
for a2 being adjective of T2 st a1 = a2 holds
types a1 = types a2
proof
let T1, T2 be TA-structure ; ::_thesis: ( TA-structure(# the carrier of T1, the adjectives of T1, the InternalRel of T1, the non-op of T1, the adj-map of T1 #) = TA-structure(# the carrier of T2, the adjectives of T2, the InternalRel of T2, the non-op of T2, the adj-map of T2 #) implies for a1 being adjective of T1
for a2 being adjective of T2 st a1 = a2 holds
types a1 = types a2 )
assume A1: TA-structure(# the carrier of T1, the adjectives of T1, the InternalRel of T1, the non-op of T1, the adj-map of T1 #) = TA-structure(# the carrier of T2, the adjectives of T2, the InternalRel of T2, the non-op of T2, the adj-map of T2 #) ; ::_thesis: for a1 being adjective of T1
for a2 being adjective of T2 st a1 = a2 holds
types a1 = types a2
let a1 be adjective of T1; ::_thesis: for a2 being adjective of T2 st a1 = a2 holds
types a1 = types a2
let a2 be adjective of T2; ::_thesis: ( a1 = a2 implies types a1 = types a2 )
assume A2: a1 = a2 ; ::_thesis: types a1 = types a2
now__::_thesis:_(_types_a1_is_Subset_of_T2_&_(_for_x_being_set_holds_
(_(_x_in_types_a1_implies_ex_t2_being_type_of_T2_st_
(_x_=_t2_&_a2_in_adjs_t2_)_)_&_(_ex_t2_being_type_of_T2_st_
(_x_=_t2_&_a2_in_adjs_t2_)_implies_x_in_types_a1_)_)_)_)
thus  types a1 is Subset of T2 by A1; ::_thesis: for x being set holds
( ( x in types a1 implies ex t2 being type of T2 st
( x = t2 & a2 in adjs t2 ) ) & ( ex t2 being type of T2 st
( x = t2 & a2 in adjs t2 ) implies x in types a1 ) )
let x be set ; ::_thesis: ( ( x in types a1 implies ex t2 being type of T2 st
( x = t2 & a2 in adjs t2 ) ) & ( ex t2 being type of T2 st
( x = t2 & a2 in adjs t2 ) implies x in types a1 ) )
hereby  ::_thesis: ( ex t2 being type of T2 st
( x = t2 & a2 in adjs t2 ) implies x in types a1 )
assume  x in types a1 ; ::_thesis: ex t2 being type of T2 st
( x = t2 & a2 in adjs t2 )
then consider t1 being type of T1 such that
A3: x = t1 and
A4: a1 in adjs t1 by Def12;
reconsider t2 = t1 as type of T2 by A1;
 adjs t1 = adjs t2 by A1;
hence  ex t2 being type of T2 st
( x = t2 & a2 in adjs t2 ) by A2, A3, A4; ::_thesis: verum
end;
given t2 being type of T2 such that A5: x = t2 and
A6: a2 in adjs t2 ; ::_thesis: x in types a1
reconsider t1 = t2 as type of T1 by A1;
 adjs t1 = adjs t2 by A1;
hence  x in types a1 by A2, A5, A6, Def12; ::_thesis: verum
end;
hence  types a1 = types a2 by Def12; ::_thesis: verum
end;

theorem :: ABCMIZ_0:12
for T being non empty TA-structure
for a being adjective of T holds types a =  {  t where t is type of T : a in adjs t  }
proof
let T be non empty TA-structure ; ::_thesis: for a being adjective of T holds types a =  {  t where t is type of T : a in adjs t  }
let a be adjective of T; ::_thesis: types a =  {  t where t is type of T : a in adjs t  }
set X =  {  t where t is type of T : a in adjs t  }  ;
  {  t where t is type of T : a in adjs t  }  c= the carrier of T
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in  {  t where t is type of T : a in adjs t  }  or x in the carrier of T )
assume  x in  {  t where t is type of T : a in adjs t  }  ; ::_thesis: x in the carrier of T
then  ex t being type of T st
( x = t & a in adjs t ) ;
hence  x in the carrier of T ; ::_thesis: verum
end;
then reconsider X =  {  t where t is type of T : a in adjs t  }  as Subset of T ;
 for x being set holds
( x in X iff ex t being type of T st
( x = t & a in adjs t ) ) ;
hence  types a =  {  t where t is type of T : a in adjs t  }  by Def12; ::_thesis: verum
end;

theorem Th13: :: ABCMIZ_0:13
for T being TA-structure
for t being type of T
for a being adjective of T holds
( a in adjs t iff t in types a )
proof
let T be TA-structure ; ::_thesis: for t being type of T
for a being adjective of T holds
( a in adjs t iff t in types a )
let t be type of T; ::_thesis: for a being adjective of T holds
( a in adjs t iff t in types a )
let a be adjective of T; ::_thesis: ( a in adjs t iff t in types a )
thus  ( a in adjs t implies t in types a ) by Def12; ::_thesis: ( t in types a implies a in adjs t )
assume  t in types a ; ::_thesis: a in adjs t
then  ex t9 being type of T st
( t = t9 & a in adjs t9 ) by Def12;
hence  a in adjs t ; ::_thesis: verum
end;

theorem Th14: :: ABCMIZ_0:14
for T being non empty TA-structure
for t being type of T
for A being Subset of the adjectives of T holds
( A c= adjs t iff t in types A )
proof
let T be non empty TA-structure ; ::_thesis: for t being type of T
for A being Subset of the adjectives of T holds
( A c= adjs t iff t in types A )
let t be type of T; ::_thesis: for A being Subset of the adjectives of T holds
( A c= adjs t iff t in types A )
let a be Subset of the adjectives of T; ::_thesis: ( a c= adjs t iff t in types a )
hereby  ::_thesis: ( t in types a implies a c= adjs t )
assume  a c= adjs t ; ::_thesis: t in types a
then  for b being adjective of T st b in a holds
t in types b by Th13;
hence  t in types a by Def13; ::_thesis: verum
end;
assume A1: t in types a ; ::_thesis: a c= adjs t
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in a or x in adjs t )
assume A2: x in a ; ::_thesis: x in adjs t
then reconsider x = x as adjective of T ;
 t in types x by A1, A2, Def13;
hence  x in adjs t by Th13; ::_thesis: verum
end;

theorem :: ABCMIZ_0:15
for T being non void TA-structure
for t being type of T holds adjs t =  {  a where a is adjective of T : t in types a  }
proof
let T be non void TA-structure ; ::_thesis: for t being type of T holds adjs t =  {  a where a is adjective of T : t in types a  }
let t be type of T; ::_thesis: adjs t =  {  a where a is adjective of T : t in types a  }
set X =  {  a where a is adjective of T : t in types a  }  ;
thus  adjs t c=  {  a where a is adjective of T : t in types a  }  :: according to XBOOLE_0:def_10 ::_thesis:  {  a where a is adjective of T : t in types a  }  c= adjs t
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in adjs t or x in  {  a where a is adjective of T : t in types a  }  )
assume A1: x in adjs t ; ::_thesis: x in  {  a where a is adjective of T : t in types a  }
then reconsider a = x as adjective of T ;
 t in types a by A1, Th13;
hence  x in  {  a where a is adjective of T : t in types a  }  ; ::_thesis: verum
end;
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in  {  a where a is adjective of T : t in types a  }  or x in adjs t )
assume  x in  {  a where a is adjective of T : t in types a  }  ; ::_thesis: x in adjs t
then  ex a being adjective of T st
( x = a & t in types a ) ;
hence  x in adjs t by Th13; ::_thesis: verum
end;

theorem Th16: :: ABCMIZ_0:16
for T being non empty TA-structure holds types ({} the adjectives of T) = the carrier of T
proof
let T be non empty TA-structure ; ::_thesis: types ({} the adjectives of T) = the carrier of T
thus  types ({} the adjectives of T) c= the carrier of T ; :: according to XBOOLE_0:def_10 ::_thesis: the carrier of T c= types ({} the adjectives of T)
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in the carrier of T or x in types ({} the adjectives of T) )
assume  x in the carrier of T ; ::_thesis: x in types ({} the adjectives of T)
then reconsider t = x as type of T ;
 for a being adjective of T st a in {} the adjectives of T holds
t in types a ;
hence  x in types ({} the adjectives of T) by Def13; ::_thesis: verum
end;

definition
let T be TA-structure ;
attrT is adjs-typed  means :: ABCMIZ_0:def 14
 for a being adjective of T holds not (types a) \/ (types (non- a)) is empty ;
end;

:: deftheorem  defines adjs-typed ABCMIZ_0:def_14_:_
 for T being TA-structure holds
( T is adjs-typed iff for a being adjective of T holds not (types a) \/ (types (non- a)) is empty );

theorem Th17: :: ABCMIZ_0:17
for T1, T2 being TA-structure st TA-structure(# the carrier of T1, the adjectives of T1, the InternalRel of T1, the non-op of T1, the adj-map of T1 #) = TA-structure(# the carrier of T2, the adjectives of T2, the InternalRel of T2, the non-op of T2, the adj-map of T2 #) & T1 is adjs-typed holds
T2 is adjs-typed
proof
let T1, T2 be TA-structure ; ::_thesis: ( TA-structure(# the carrier of T1, the adjectives of T1, the InternalRel of T1, the non-op of T1, the adj-map of T1 #) = TA-structure(# the carrier of T2, the adjectives of T2, the InternalRel of T2, the non-op of T2, the adj-map of T2 #) & T1 is adjs-typed implies T2 is adjs-typed )
assume that
A1: TA-structure(# the carrier of T1, the adjectives of T1, the InternalRel of T1, the non-op of T1, the adj-map of T1 #) = TA-structure(# the carrier of T2, the adjectives of T2, the InternalRel of T2, the non-op of T2, the adj-map of T2 #) and
A2: for a being adjective of T1 holds not (types a) \/ (types (non- a)) is empty ; :: according to ABCMIZ_0:def_14 ::_thesis: T2 is adjs-typed
let b be adjective of T2; :: according to ABCMIZ_0:def_14 ::_thesis: not (types b) \/ (types (non- b)) is empty
reconsider a = b as adjective of T1 by A1;
A3: not (types a) \/ (types (non- a)) is empty by A2;
 types a = types b by A1, Th11;
hence  not (types b) \/ (types (non- b)) is empty by A1, A3, Th11; ::_thesis: verum
end;

registration
cluster non empty trivial finite 1 -element reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded V139() connected up-complete /\-complete Noetherian Mizar-widening-like non void involutive without_fixpoints strict consistent adj-structured adjs-typed for TA-structure ;
existence
 ex b1 being 1 -element reflexive transitive antisymmetric complete upper-bounded strict TA-structure st
( not b1 is void & b1 is Mizar-widening-like & b1 is involutive & b1 is without_fixpoints & b1 is consistent & b1 is adj-structured & b1 is adjs-typed )
proof
 {0} c= {0,1} by ZFMISC_1:7;
then reconsider A = {0} as Element of Fin {0,1} by FINSUB_1:def_5;
reconsider x = 0 , y = 1 as Element of {0,1} by TARSKI:def_2;
set R = the 1 -element reflexive RelStr ;
reconsider n = (0,1) --> (y,x) as UnOp of {0,1} ;
set f = the carrier of the 1 -element reflexive RelStr --> A;
set T = TA-structure(# the carrier of the 1 -element reflexive RelStr ,{0,1}, the InternalRel of the 1 -element reflexive RelStr ,n,( the carrier of the 1 -element reflexive RelStr --> A) #);
 the carrier of TA-structure(# the carrier of the 1 -element reflexive RelStr ,{0,1}, the InternalRel of the 1 -element reflexive RelStr ,n,( the carrier of the 1 -element reflexive RelStr --> A) #) is 1 -element ;
 RelStr(# the carrier of TA-structure(# the carrier of the 1 -element reflexive RelStr ,{0,1}, the InternalRel of the 1 -element reflexive RelStr ,n,( the carrier of the 1 -element reflexive RelStr --> A) #), the InternalRel of TA-structure(# the carrier of the 1 -element reflexive RelStr ,{0,1}, the InternalRel of the 1 -element reflexive RelStr ,n,( the carrier of the 1 -element reflexive RelStr --> A) #) #) = RelStr(# the carrier of the 1 -element reflexive RelStr , the InternalRel of the 1 -element reflexive RelStr #) ;
then reconsider T = TA-structure(# the carrier of the 1 -element reflexive RelStr ,{0,1}, the InternalRel of the 1 -element reflexive RelStr ,n,( the carrier of the 1 -element reflexive RelStr --> A) #) as 1 -element reflexive strict TA-structure by STRUCT_0:def_19, WAYBEL_8:12;
take  T ; ::_thesis: ( not T is void & T is Mizar-widening-like & T is involutive & T is without_fixpoints & T is consistent & T is adj-structured & T is adjs-typed )
thus  not T is void ; ::_thesis: ( T is Mizar-widening-like & T is involutive & T is without_fixpoints & T is consistent & T is adj-structured & T is adjs-typed )
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 )
A1: n . y = x by FUNCT_4:63;
A2: n . x = y by FUNCT_4:63;
hence  ( T is involutive & T is without_fixpoints ) by A1, Th4; ::_thesis: ( T is consistent & T is adj-structured & T is adjs-typed )
hereby  :: according to ABCMIZ_0:def_9 ::_thesis: ( T is adj-structured & T is adjs-typed )
let t be type of T; ::_thesis: for a being adjective of T st a in adjs t holds
not non- a in adjs t
let a be adjective of T; ::_thesis: ( a in adjs t implies not non- a in adjs t )
A3: adjs t = A by FUNCOP_1:7;
 ( a = 0 or a = 1 ) by TARSKI:def_2;
hence  ( a in adjs t implies not non- a in adjs t ) by A2, A3, TARSKI:def_1; ::_thesis: verum
end;
set t = the type of T;
hereby  :: according to ABCMIZ_0:def_11 ::_thesis: T is adjs-typed
let t1, t2 be type of T; ::_thesis: adjs (t1 "\/" t2) = (adjs t1) /\ (adjs t2)
A4: adjs t2 = A by FUNCOP_1:7;
 adjs t1 = A by FUNCOP_1:7;
hence  adjs (t1 "\/" t2) = (adjs t1) /\ (adjs t2) by A4, FUNCOP_1:7; ::_thesis: verum
end;
let a be adjective of T; :: according to ABCMIZ_0:def_14 ::_thesis: not (types a) \/ (types (non- a)) is empty
A5: adjs the type of T = A by FUNCOP_1:7;
 ( a = 0 or a = 1 ) by TARSKI:def_2;
then  ( a in adjs the type of T or non- a in adjs the type of T ) by A1, A5, TARSKI:def_1;
then  ( the type of T in types a or the type of T in types (non- a) ) by Th13;
hence  not (types a) \/ (types (non- a)) is empty ; ::_thesis: verum
end;
end;

theorem :: ABCMIZ_0:18
for T being consistent TA-structure
for a being adjective of T holds types a misses types (non- a)
proof
let T be consistent TA-structure ; ::_thesis: for a being adjective of T holds types a misses types (non- a)
let a be adjective of T; ::_thesis: types a misses types (non- a)
assume  types a meets types (non- a) ; ::_thesis: contradiction
then consider x being set  such that
A1: x in types a and
A2: x in types (non- a) by XBOOLE_0:3;
A3: ex t2 being type of T st
( x = t2 & non- a in adjs t2 ) by A2, Def12;
 ex t1 being type of T st
( x = t1 & a in adjs t1 ) by A1, Def12;
hence  contradiction by A3, Def9; ::_thesis: verum
end;

registration
let T be reflexive transitive antisymmetric with_suprema adj-structured TA-structure ;
let a be adjective of T;
cluster types a ->  directed lower ;
coherence
 ( types a is lower & types a is directed )
proof
thus  types a is lower ::_thesis: types a is directed
proof
let x, y be Element of T; :: according to WAYBEL_0:def_19 ::_thesis: ( not x in types a or not y <= x or y in types a )
assume that
A1: x in types a and
A2: y <= x ; ::_thesis: y in types a
A3: adjs x c= adjs y by A2, Th10;
 a in adjs x by A1, Th13;
hence  y in types a by A3, Th13; ::_thesis: verum
end;
let x, y be Element of T; :: according to WAYBEL_0:def_1 ::_thesis: ( not x in types a or not y in types a or ex b1 being Element of the carrier of T st
( b1 in types a & x <= b1 & y <= b1 ) )
assume that
A4: x in types a and
A5: y in types a ; ::_thesis: ex b1 being Element of the carrier of T st
( b1 in types a & x <= b1 & y <= b1 )
take  x "\/" y ; ::_thesis: ( x "\/" y in types a & x <= x "\/" y & y <= x "\/" y )
A6: a in adjs y by A5, Th13;
 a in adjs x by A4, Th13;
then  a in (adjs x) /\ (adjs y) by A6, XBOOLE_0:def_4;
then  a in adjs (x "\/" y) by Def11;
hence  ( x "\/" y in types a & x <= x "\/" y & y <= x "\/" y ) by Th13, YELLOW_0:22; ::_thesis: verum
end;
end;

registration
let T be reflexive transitive antisymmetric with_suprema adj-structured TA-structure ;
let A be Subset of the adjectives of T;
cluster types A ->  directed lower ;
coherence
 ( types A is lower & types A is directed )
proof
thus  types A is lower ::_thesis: types A is directed
proof
let x, y be Element of T; :: according to WAYBEL_0:def_19 ::_thesis: ( not x in types A or not y <= x or y in types A )
assume that
A1: x in types A and
A2: y <= x ; ::_thesis: y in types A
now__::_thesis:_for_a_being_adjective_of_T_st_a_in_A_holds_
y_in_types_a
let a be adjective of T; ::_thesis: ( a in A implies y in types a )
assume  a in A ; ::_thesis: y in types a
then  x in types a by A1, Def13;
then A3: a in adjs x by Th13;
 adjs x c= adjs y by A2, Th10;
hence  y in types a by A3, Th13; ::_thesis: verum
end;
hence  y in types A by Def13; ::_thesis: verum
end;
let x, y be Element of T; :: according to WAYBEL_0:def_1 ::_thesis: ( not x in types A or not y in types A or ex b1 being Element of the carrier of T st
( b1 in types A & x <= b1 & y <= b1 ) )
assume that
A4: x in types A and
A5: y in types A ; ::_thesis: ex b1 being Element of the carrier of T st
( b1 in types A & x <= b1 & y <= b1 )
take  x "\/" y ; ::_thesis: ( x "\/" y in types A & x <= x "\/" y & y <= x "\/" y )
now__::_thesis:_for_a_being_adjective_of_T_st_a_in_A_holds_
x_"\/"_y_in_types_a
let a be adjective of T; ::_thesis: ( a in A implies x "\/" y in types a )
assume A6: a in A ; ::_thesis: x "\/" y in types a
then  y in types a by A5, Def13;
then A7: a in adjs y by Th13;
 x in types a by A4, A6, Def13;
then  a in adjs x by Th13;
then  a in (adjs x) /\ (adjs y) by A7, XBOOLE_0:def_4;
then  a in adjs (x "\/" y) by Def11;
hence  x "\/" y in types a by Th13; ::_thesis: verum
end;
hence  ( x "\/" y in types A & x <= x "\/" y & y <= x "\/" y ) by Def13, YELLOW_0:22; ::_thesis: verum
end;
end;

begin

definition
let T be TA-structure ;
let t be Element of T;
let a be adjective of T;
preda is_applicable_to t means :Def15: :: ABCMIZ_0:def 15
 ex t9 being type of T st
( t9 in types a & t9 <= t );
end;

:: deftheorem Def15 defines is_applicable_to ABCMIZ_0:def_15_:_
 for T being TA-structure
for t being Element of T
for a being adjective of T holds
( a is_applicable_to t iff ex t9 being type of T st
( t9 in types a & t9 <= t ) );

definition
let T be TA-structure ;
let t be type of T;
let A be Subset of the adjectives of T;
predA is_applicable_to t means :Def16: :: ABCMIZ_0:def 16
 ex t9 being type of T st
( A c= adjs t9 & t9 <= t );
end;

:: deftheorem Def16 defines is_applicable_to ABCMIZ_0:def_16_:_
 for T being TA-structure
for t being type of T
for A being Subset of the adjectives of T holds
( A is_applicable_to t iff ex t9 being type of T st
( A c= adjs t9 & t9 <= t ) );

theorem Th19: :: ABCMIZ_0:19
for T being reflexive transitive antisymmetric with_suprema adj-structured TA-structure
for a being adjective of T
for t being type of T st a is_applicable_to t holds
(types a) /\ (downarrow t) is Ideal of T
proof
let T be reflexive transitive antisymmetric with_suprema adj-structured TA-structure ; ::_thesis: for a being adjective of T
for t being type of T st a is_applicable_to t holds
(types a) /\ (downarrow t) is Ideal of T
let a be adjective of T; ::_thesis: for t being type of T st a is_applicable_to t holds
(types a) /\ (downarrow t) is Ideal of T
let t be type of T; ::_thesis: ( a is_applicable_to t implies (types a) /\ (downarrow t) is Ideal of T )
given t9 being type of T such that A1: t9 in types a and
A2: t9 <= t ; :: according to ABCMIZ_0:def_15 ::_thesis: (types a) /\ (downarrow t) is Ideal of T
 t9 in downarrow t by A2, WAYBEL_0:17;
hence  (types a) /\ (downarrow t) is Ideal of T by A1, WAYBEL_0:27, WAYBEL_0:44, XBOOLE_0:def_4; ::_thesis: verum
end;

definition
let T be non empty reflexive transitive TA-structure ;
let t be Element of T;
let a be adjective of T;
funca ast t ->  type of T equals :: ABCMIZ_0:def 17
 sup ((types a) /\ (downarrow t));
coherence
 sup ((types a) /\ (downarrow t)) is type of T ;
end;

:: deftheorem  defines ast ABCMIZ_0:def_17_:_
 for T being non empty reflexive transitive TA-structure
for t being Element of T
for a being adjective of T holds a ast t = sup ((types a) /\ (downarrow t));

theorem Th20: :: ABCMIZ_0:20
for T being reflexive transitive antisymmetric with_suprema Noetherian adj-structured TA-structure
for t being type of T
for a being adjective of T st a is_applicable_to t holds
a ast t <= t
proof
let T be reflexive transitive antisymmetric with_suprema Noetherian adj-structured TA-structure ; ::_thesis: for t being type of T
for a being adjective of T st a is_applicable_to t holds
a ast t <= t
let t be type of T; ::_thesis: for a being adjective of T st a is_applicable_to t holds
a ast t <= t
let a be adjective of T; ::_thesis: ( a is_applicable_to t implies a ast t <= t )
assume  a is_applicable_to t ; ::_thesis: a ast t <= t
then  (types a) /\ (downarrow t) is Ideal of T by Th19;
then  sup ((types a) /\ (downarrow t)) in (types a) /\ (downarrow t) by Th1;
then  a ast t in downarrow t by XBOOLE_0:def_4;
hence  a ast t <= t by WAYBEL_0:17; ::_thesis: verum
end;

theorem Th21: :: ABCMIZ_0:21
for T being reflexive transitive antisymmetric with_suprema Noetherian adj-structured TA-structure
for t being type of T
for a being adjective of T st a is_applicable_to t holds
a in adjs (a ast t)
proof
let T be reflexive transitive antisymmetric with_suprema Noetherian adj-structured TA-structure ; ::_thesis: for t being type of T
for a being adjective of T st a is_applicable_to t holds
a in adjs (a ast t)
let t be type of T; ::_thesis: for a being adjective of T st a is_applicable_to t holds
a in adjs (a ast t)
let a be adjective of T; ::_thesis: ( a is_applicable_to t implies a in adjs (a ast t) )
assume  a is_applicable_to t ; ::_thesis: a in adjs (a ast t)
then  (types a) /\ (downarrow t) is Ideal of T by Th19;
then  sup ((types a) /\ (downarrow t)) in (types a) /\ (downarrow t) by Th1;
then  a ast t in types a by XBOOLE_0:def_4;
hence  a in adjs (a ast t) by Th13; ::_thesis: verum
end;

theorem Th22: :: ABCMIZ_0:22
for T being reflexive transitive antisymmetric with_suprema Noetherian adj-structured TA-structure
for t being type of T
for a being adjective of T st a is_applicable_to t holds
a ast t in types a
proof
let T be reflexive transitive antisymmetric with_suprema Noetherian adj-structured TA-structure ; ::_thesis: for t being type of T
for a being adjective of T st a is_applicable_to t holds
a ast t in types a
let t be type of T; ::_thesis: for a being adjective of T st a is_applicable_to t holds
a ast t in types a
let a be adjective of T; ::_thesis: ( a is_applicable_to t implies a ast t in types a )
assume  a is_applicable_to t ; ::_thesis: a ast t in types a
then  (types a) /\ (downarrow t) is Ideal of T by Th19;
then  sup ((types a) /\ (downarrow t)) in (types a) /\ (downarrow t) by Th1;
hence  a ast t in types a by XBOOLE_0:def_4; ::_thesis: verum
end;

theorem Th23: :: ABCMIZ_0:23
for T being reflexive transitive antisymmetric with_suprema Noetherian adj-structured TA-structure
for t being type of T
for a being adjective of T
for t9 being type of T st t9 <= t & a in adjs t9 holds
( a is_applicable_to t & t9 <= a ast t )
proof
let T be reflexive transitive antisymmetric with_suprema Noetherian adj-structured TA-structure ; ::_thesis: for t being type of T
for a being adjective of T
for t9 being type of T st t9 <= t & a in adjs t9 holds
( a is_applicable_to t & t9 <= a ast t )
let t be type of T; ::_thesis: for a being adjective of T
for t9 being type of T st t9 <= t & a in adjs t9 holds
( a is_applicable_to t & t9 <= a ast t )
let a be adjective of T; ::_thesis: for t9 being type of T st t9 <= t & a in adjs t9 holds
( a is_applicable_to t & t9 <= a ast t )
let t9 be type of T; ::_thesis: ( t9 <= t & a in adjs t9 implies ( a is_applicable_to t & t9 <= a ast t ) )
assume that
A1: t9 <= t and
A2: a in adjs t9 ; ::_thesis: ( a is_applicable_to t & t9 <= a ast t )
A3: t9 in downarrow t by A1, WAYBEL_0:17;
thus  a is_applicable_to t ::_thesis: t9 <= a ast t
proof
take  t9 ; :: according to ABCMIZ_0:def_15 ::_thesis: ( t9 in types a & t9 <= t )
thus  ( t9 in types a & t9 <= t ) by A1, A2, Th13; ::_thesis: verum
end;
then  (types a) /\ (downarrow t) is Ideal of T by Th19;
then  ex_sup_of (types a) /\ (downarrow t),T by Th1;
then A4: a ast t is_>=_than (types a) /\ (downarrow t) by YELLOW_0:30;
 t9 in types a by A2, Th13;
then  t9 in (types a) /\ (downarrow t) by A3, XBOOLE_0:def_4;
hence  t9 <= a ast t by A4, LATTICE3:def_9; ::_thesis: verum
end;

theorem Th24: :: ABCMIZ_0:24
for T being reflexive transitive antisymmetric with_suprema Noetherian adj-structured TA-structure
for t being type of T
for a being adjective of T st a in adjs t holds
( a is_applicable_to t & a ast t = t )
proof
let T be reflexive transitive antisymmetric with_suprema Noetherian adj-structured TA-structure ; ::_thesis: for t being type of T
for a being adjective of T st a in adjs t holds
( a is_applicable_to t & a ast t = t )
let t be type of T; ::_thesis: for a being adjective of T st a in adjs t holds
( a is_applicable_to t & a ast t = t )
let a be adjective of T; ::_thesis: ( a in adjs t implies ( a is_applicable_to t & a ast t = t ) )
assume A1: a in adjs t ; ::_thesis: ( a is_applicable_to t & a ast t = t )
hence  a is_applicable_to t by Th23; ::_thesis: a ast t = t
then A2: a ast t <= t by Th20;
 t <= a ast t by A1, Th23;
hence  a ast t = t by A2, YELLOW_0:def_3; ::_thesis: verum
end;

theorem :: ABCMIZ_0:25
for T being reflexive transitive antisymmetric with_suprema Noetherian adj-structured TA-structure
for t being type of T
for a, b being adjective of T st a is_applicable_to t & b is_applicable_to a ast t holds
( b is_applicable_to t & a is_applicable_to b ast t & a ast (b ast t) = b ast (a ast t) )
proof
let T be reflexive transitive antisymmetric with_suprema Noetherian adj-structured TA-structure ; ::_thesis: for t being type of T
for a, b being adjective of T st a is_applicable_to t & b is_applicable_to a ast t holds
( b is_applicable_to t & a is_applicable_to b ast t & a ast (b ast t) = b ast (a ast t) )
let t be type of T; ::_thesis: for a, b being adjective of T st a is_applicable_to t & b is_applicable_to a ast t holds
( b is_applicable_to t & a is_applicable_to b ast t & a ast (b ast t) = b ast (a ast t) )
let a, b be adjective of T; ::_thesis: ( a is_applicable_to t & b is_applicable_to a ast t implies ( b is_applicable_to t & a is_applicable_to b ast t & a ast (b ast t) = b ast (a ast t) ) )
assume that
A1: a is_applicable_to t and
A2: b is_applicable_to a ast t ; ::_thesis: ( b is_applicable_to t & a is_applicable_to b ast t & a ast (b ast t) = b ast (a ast t) )
consider t9 being type of T such that
A3: t9 in types b and
A4: t9 <= a ast t by A2, Def15;
A5: b in adjs t9 by A3, Th13;
A6: a ast t <= t by A1, Th20;
thus A7: b is_applicable_to t ::_thesis: ( a is_applicable_to b ast t & a ast (b ast t) = b ast (a ast t) )
proof
take  t9 ; :: according to ABCMIZ_0:def_15 ::_thesis: ( t9 in types b & t9 <= t )
thus  ( t9 in types b & t9 <= t ) by A6, A3, A4, YELLOW_0:def_2; ::_thesis: verum
end;
A8: t9 <= t by A6, A4, YELLOW_0:def_2;
thus A9: a is_applicable_to b ast t ::_thesis: a ast (b ast t) = b ast (a ast t)
proof
take  t9 ; :: according to ABCMIZ_0:def_15 ::_thesis: ( t9 in types a & t9 <= b ast t )
 a ast t in types a by A1, Th22;
hence  t9 in types a by A4, WAYBEL_0:def_19; ::_thesis: t9 <= b ast t
thus  t9 <= b ast t by A8, A5, Th23; ::_thesis: verum
end;
then A10: a ast (b ast t) <= b ast t by Th20;
A11: a ast t in types a by A1, Th22;
A12: a ast (b ast t) is_>=_than (types b) /\ (downarrow (a ast t))
proof
let t9 be type of T; :: according to LATTICE3:def_9 ::_thesis: ( not t9 in (types b) /\ (downarrow (a ast t)) or t9 <= a ast (b ast t) )
assume A13: t9 in (types b) /\ (downarrow (a ast t)) ; ::_thesis: t9 <= a ast (b ast t)
then  t9 in types b by XBOOLE_0:def_4;
then A14: b in adjs t9 by Th13;
 t9 in downarrow (a ast t) by A13, XBOOLE_0:def_4;
then A15: t9 <= a ast t by WAYBEL_0:17;
then  t9 in types a by A11, WAYBEL_0:def_19;
then A16: a in adjs t9 by Th13;
 t9 <= t by A6, A15, YELLOW_0:def_2;
then  t9 <= b ast t by A14, Th23;
hence  t9 <= a ast (b ast t) by A16, Th23; ::_thesis: verum
end;
 b ast t <= t by A7, Th20;
then A17: a ast (b ast t) <= t by A10, YELLOW_0:def_2;
 a in adjs (a ast (b ast t)) by A9, Th21;
then  a ast (b ast t) <= a ast t by A17, Th23;
then A18: a ast (b ast t) in downarrow (a ast t) by WAYBEL_0:17;
A19: a ast (b ast t) <= b ast t by A9, Th20;
 b ast t in types b by A7, Th22;
then  a ast (b ast t) in types b by A19, WAYBEL_0:def_19;
then  a ast (b ast t) in (types b) /\ (downarrow (a ast t)) by A18, XBOOLE_0:def_4;
then  for t9 being type of T st t9 is_>=_than (types b) /\ (downarrow (a ast t)) holds
a ast (b ast t) <= t9 by LATTICE3:def_9;
hence  a ast (b ast t) = b ast (a ast t) by A12, YELLOW_0:30; ::_thesis: verum
end;

theorem Th26: :: ABCMIZ_0:26
for T being reflexive transitive antisymmetric with_suprema adj-structured TA-structure
for A being Subset of the adjectives of T
for t being type of T st A is_applicable_to t holds
(types A) /\ (downarrow t) is Ideal of T
proof
let T be reflexive transitive antisymmetric with_suprema adj-structured TA-structure ; ::_thesis: for A being Subset of the adjectives of T
for t being type of T st A is_applicable_to t holds
(types A) /\ (downarrow t) is Ideal of T
let A be Subset of the adjectives of T; ::_thesis: for t being type of T st A is_applicable_to t holds
(types A) /\ (downarrow t) is Ideal of T
let t be type of T; ::_thesis: ( A is_applicable_to t implies (types A) /\ (downarrow t) is Ideal of T )
given t9 being type of T such that A1: A c= adjs t9 and
A2: t9 <= t ; :: according to ABCMIZ_0:def_16 ::_thesis: (types A) /\ (downarrow t) is Ideal of T
A3: t9 in downarrow t by A2, WAYBEL_0:17;
 t9 in types A by A1, Th14;
hence  (types A) /\ (downarrow t) is Ideal of T by A3, WAYBEL_0:27, WAYBEL_0:44, XBOOLE_0:def_4; ::_thesis: verum
end;

definition
let T be non empty reflexive transitive TA-structure ;
let t be type of T;
let A be Subset of the adjectives of T;
funcA ast t ->  type of T equals :: ABCMIZ_0:def 18
 sup ((types A) /\ (downarrow t));
coherence
 sup ((types A) /\ (downarrow t)) is type of T ;
end;

:: deftheorem  defines ast ABCMIZ_0:def_18_:_
 for T being non empty reflexive transitive TA-structure
for t being type of T
for A being Subset of the adjectives of T holds A ast t = sup ((types A) /\ (downarrow t));

theorem Th27: :: ABCMIZ_0:27
for T being non empty reflexive transitive antisymmetric TA-structure
for t being type of T holds ({} the adjectives of T) ast t = t
proof
let T be non empty reflexive transitive antisymmetric TA-structure ; ::_thesis: for t being type of T holds ({} the adjectives of T) ast t = t
let t be type of T; ::_thesis: ({} the adjectives of T) ast t = t
set A = {} the adjectives of T;
 types ({} the adjectives of T) = the carrier of T by Th16;
then  (types ({} the adjectives of T)) /\ (downarrow t) = downarrow t by XBOOLE_1:28;
hence  ({} the adjectives of T) ast t = t by WAYBEL_0:34; ::_thesis: verum
end;

definition
let T be non empty reflexive transitive non void TA-structure ;
let t be type of T;
let p be FinSequence of the adjectives of T;
func apply (p,t) ->  FinSequence of the carrier of T means :Def19: :: ABCMIZ_0:def 19
( len it = (len p) + 1 & it . 1 = t & ( for i being Element of NAT
for a being adjective of T
for t being type of T st i in dom p & a = p . i & t = it . i holds
it . (i + 1) = a ast t ) );
existence
 ex b1 being FinSequence of the carrier of T st
( len b1 = (len p) + 1 & b1 . 1 = t & ( for i being Element of NAT
for a being adjective of T
for t being type of T st i in dom p & a = p . i & t = b1 . i holds
b1 . (i + 1) = a ast t ) )
proof
defpred S1[ set , set , set ] means  ex a being adjective of T st
( a = p . $1 & ( ( $2 is not type of T & $3 = 0 ) or ex t being type of T st
( t = $2 & $3 = a ast t ) ) );
A1: for i being Element of NAT st 1 <= i & i < (len p) + 1 holds
for x being set ex y being set st S1[i,x,y]
proof
let i be Element of NAT ; ::_thesis: ( 1 <= i & i < (len p) + 1 implies for x being set ex y being set st S1[i,x,y] )
assume A2: 1 <= i ; ::_thesis: ( not i < (len p) + 1 or for x being set ex y being set st S1[i,x,y] )
assume  i < (len p) + 1 ; ::_thesis: for x being set ex y being set st S1[i,x,y]
then  i <= len p by NAT_1:13;
then  i in dom p by A2, FINSEQ_3:25;
then  p . i in rng p by FUNCT_1:3;
then reconsider a = p . i as adjective of T ;
let x be set ; ::_thesis: ex y being set st S1[i,x,y]
percases ( not x is type of T or x is type of T ) ;
supposeA3: x is not type of T ; ::_thesis: ex y being set st S1[i,x,y]
take  0 ; ::_thesis: S1[i,x, 0 ]
take  a ; ::_thesis: ( a = p . i & ( ( x is not type of T & 0 = 0 ) or ex t being type of T st
( t = x & 0 = a ast t ) ) )
thus  ( a = p . i & ( ( x is not type of T & 0 = 0 ) or ex t being type of T st
( t = x & 0 = a ast t ) ) ) by A3; ::_thesis: verum
end;
suppose x is type of T ; ::_thesis: ex y being set st S1[i,x,y]
then reconsider t = x as type of T ;
take  a ast t ; ::_thesis: S1[i,x,a ast t]
take  a ; ::_thesis: ( a = p . i & ( ( x is not type of T & a ast t = 0 ) or ex t being type of T st
( t = x & a ast t = a ast t ) ) )
thus  a = p . i ; ::_thesis: ( ( x is not type of T & a ast t = 0 ) or ex t being type of T st
( t = x & a ast t = a ast t ) )
thus  ( ( x is not type of T & a ast t = 0 ) or ex t being type of T st
( t = x & a ast t = a ast t ) ) ; ::_thesis: verum
end;
end;
end;
consider q being FinSequence such that
A4: len q = (len p) + 1 and
A5: ( q . 1 = t or (len p) + 1 = 0 ) and
A6: for i being Element of NAT st 1 <= i & i < (len p) + 1 holds
S1[i,q . i,q . (i + 1)] from RECDEF_1:sch_3(A1);
defpred S2[ Element of NAT ] means ( $1 in dom q implies q . $1 is type of T );
A7: now__::_thesis:_for_k_being_Element_of_NAT_st_S2[k]_holds_
S2[k_+_1]
let k be Element of NAT ; ::_thesis: ( S2[k] implies S2[k + 1] )
assume A8: S2[k] ; ::_thesis: S2[k + 1]
now__::_thesis:_(_k_+_1_in_dom_q_implies_q_._(k_+_1)_is_type_of_T_)
assume  k + 1 in dom q ; ::_thesis: q . (k + 1) is type of T
then  k + 1 <= len q by FINSEQ_3:25;
then A9: k < len q by NAT_1:13;
A10: ( k <> 0 implies k >= 0 + 1 ) by NAT_1:13;
then  ( k <> 0 implies ex a being adjective of T st
( a = p . k & ( ( q . k is not type of T & q . (k + 1) = 0 ) or ex t being type of T st
( t = q . k & q . (k + 1) = a ast t ) ) ) ) by A4, A6, A9;
hence  q . (k + 1) is type of T by A5, A8, A10, A9, FINSEQ_3:25; ::_thesis: verum
end;
hence  S2[k + 1] ; ::_thesis: verum
end;
A11: S2[ 0 ] by FINSEQ_3:24;
A12: for k being Element of NAT holds S2[k] from NAT_1:sch_1(A11, A7);
 rng q c= the carrier of T
proof
let a be set ; :: according to TARSKI:def_3 ::_thesis: ( not a in rng q or a in the carrier of T )
assume  a in rng q ; ::_thesis: a in the carrier of T
then  ex x being set st
( x in dom q & a = q . x ) by FUNCT_1:def_3;
then  a is type of T by A12;
hence  a in the carrier of T ; ::_thesis: verum
end;
then reconsider q = q as FinSequence of the carrier of T by FINSEQ_1:def_4;
take  q ; ::_thesis: ( len q = (len p) + 1 & q . 1 = t & ( for i being Element of NAT
for a being adjective of T
for t being type of T st i in dom p & a = p . i & t = q . i holds
q . (i + 1) = a ast t ) )
thus  ( len q = (len p) + 1 & q . 1 = t ) by A4, A5; ::_thesis: for i being Element of NAT
for a being adjective of T
for t being type of T st i in dom p & a = p . i & t = q . i holds
q . (i + 1) = a ast t
let i be Element of NAT ; ::_thesis: for a being adjective of T
for t being type of T st i in dom p & a = p . i & t = q . i holds
q . (i + 1) = a ast t
let a be adjective of T; ::_thesis: for t being type of T st i in dom p & a = p . i & t = q . i holds
q . (i + 1) = a ast t
let t be type of T; ::_thesis: ( i in dom p & a = p . i & t = q . i implies q . (i + 1) = a ast t )
assume that
A13: i in dom p and
A14: a = p . i and
A15: t = q . i ; ::_thesis: q . (i + 1) = a ast t
 i <= len p by A13, FINSEQ_3:25;
then A16: i < (len p) + 1 by NAT_1:13;
 i >= 1 by A13, FINSEQ_3:25;
then  ex a being adjective of T st
( a = p . i & ( ( q . i is not type of T & q . (i + 1) = 0 ) or ex t being type of T st
( t = q . i & q . (i + 1) = a ast t ) ) ) by A6, A16;
hence  q . (i + 1) = a ast t by A14, A15; ::_thesis: verum
end;
correctness
uniqueness
for b1, b2 being FinSequence of the carrier of T st len b1 = (len p) + 1 & b1 . 1 = t & ( for i being Element of NAT
for a being adjective of T
for t being type of T st i in dom p & a = p . i & t = b1 . i holds
b1 . (i + 1) = a ast t ) & len b2 = (len p) + 1 & b2 . 1 = t & ( for i being Element of NAT
for a being adjective of T
for t being type of T st i in dom p & a = p . i & t = b2 . i holds
b2 . (i + 1) = a ast t ) holds
b1 = b2;
proof
let q1, q2 be FinSequence of the carrier of T; ::_thesis: ( len q1 = (len p) + 1 & q1 . 1 = t & ( for i being Element of NAT
for a being adjective of T
for t being type of T st i in dom p & a = p . i & t = q1 . i holds
q1 . (i + 1) = a ast t ) & len q2 = (len p) + 1 & q2 . 1 = t & ( for i being Element of NAT
for a being adjective of T
for t being type of T st i in dom p & a = p . i & t = q2 . i holds
q2 . (i + 1) = a ast t ) implies q1 = q2 )
assume that
A17: len q1 = (len p) + 1 and
A18: q1 . 1 = t and
A19: for i being Element of NAT
for a being adjective of T
for t being type of T st i in dom p & a = p . i & t = q1 . i holds
q1 . (i + 1) = a ast t and
A20: len q2 = (len p) + 1 and
A21: q2 . 1 = t and
A22: for i being Element of NAT
for a being adjective of T
for t being type of T st i in dom p & a = p . i & t = q2 . i holds
q2 . (i + 1) = a ast t ; ::_thesis: q1 = q2
defpred S1[ Nat] means ( $1 in dom q1 implies q1 . $1 = q2 . $1 );
A23: now__::_thesis:_for_i_being_Nat_st_S1[i]_holds_
S1[i_+_1]
let i be Nat; ::_thesis: ( S1[i] implies S1[i + 1] )
assume A24: S1[i] ; ::_thesis: S1[i + 1]
now__::_thesis:_(_i_+_1_in_dom_q1_implies_q1_._(i_+_1)_=_q2_._(i_+_1)_)
assume  i + 1 in dom q1 ; ::_thesis: q1 . (i + 1) = q2 . (i + 1)
then A25: i + 1 <= len q1 by FINSEQ_3:25;
then A26: i <= len q1 by NAT_1:13;
A27: i <= len p by A17, A25, XREAL_1:6;
percases ( i = 0 or i > 0 ) ;
suppose i = 0 ; ::_thesis: q1 . (i + 1) = q2 . (i + 1)
hence  q1 . (i + 1) = q2 . (i + 1) by A18, A21; ::_thesis: verum
end;
suppose i > 0 ; ::_thesis: q1 . (i + 1) = q2 . (i + 1)
then A28: i >= 0 + 1 by NAT_1:13;
then A29: i in dom p by A27, FINSEQ_3:25;
then reconsider a = p . i as adjective of T by FINSEQ_2:11;
 i in dom q1 by A26, A28, FINSEQ_3:25;
then reconsider t = q1 . i as type of T by FINSEQ_2:11;
thus q1 . (i + 1) = a ast t by A19, A29
.= q2 . (i + 1) by A22, A24, A26, A28, A29, FINSEQ_3:25 ; ::_thesis: verum
end;
end;
end;
hence  S1[i + 1] ; ::_thesis: verum
end;
A30: S1[ 0 ] by FINSEQ_3:25;
A31: for i being Nat holds S1[i] from NAT_1:sch_2(A30, A23);
 dom q1 = dom q2 by A17, A20, FINSEQ_3:29;
hence  q1 = q2 by A31, FINSEQ_1:13; ::_thesis: verum
end;
end;

:: deftheorem Def19 defines apply ABCMIZ_0:def_19_:_
 for T being non empty reflexive transitive non void TA-structure
for t being type of T
for p being FinSequence of the adjectives of T
for b4 being FinSequence of the carrier of T holds
( b4 = apply (p,t) iff ( len b4 = (len p) + 1 & b4 . 1 = t & ( for i being Element of NAT
for a being adjective of T
for t being type of T st i in dom p & a = p . i & t = b4 . i holds
b4 . (i + 1) = a ast t ) ) );

registration
let T be non empty reflexive transitive non void TA-structure ;
let t be type of T;
let p be FinSequence of the adjectives of T;
cluster apply (p,t) ->  non empty ;
coherence
 not apply (p,t) is empty
proof
 len (apply (p,t)) = (len p) + 1 by Def19;
hence  not apply (p,t) is empty ; ::_thesis: verum
end;
end;

theorem :: ABCMIZ_0:28
for T being non empty reflexive transitive non void TA-structure
for t being type of T holds apply ((<*> the adjectives of T),t) = <*t*>
proof
let T be non empty reflexive transitive non void TA-structure ; ::_thesis: for t being type of T holds apply ((<*> the adjectives of T),t) = <*t*>
let t be type of T; ::_thesis: apply ((<*> the adjectives of T),t) = <*t*>
A1: (apply ((<*> the adjectives of T),t)) . 1 = t by Def19;
 len (apply ((<*> the adjectives of T),t)) = 0 + 1 by Def19, CARD_1:27;
hence  apply ((<*> the adjectives of T),t) = <*t*> by A1, FINSEQ_1:40; ::_thesis: verum
end;

theorem Th29: :: ABCMIZ_0:29
for T being non empty reflexive transitive non void TA-structure
for t being type of T
for a being adjective of T holds apply (<*a*>,t) = <*t,(a ast t)*>
proof
let T be non empty reflexive transitive non void TA-structure ; ::_thesis: for t being type of T
for a being adjective of T holds apply (<*a*>,t) = <*t,(a ast t)*>
let t be type of T; ::_thesis: for a being adjective of T holds apply (<*a*>,t) = <*t,(a ast t)*>
let a be adjective of T; ::_thesis: apply (<*a*>,t) = <*t,(a ast t)*>
A1: <*a*> . 1 = a by FINSEQ_1:40;
A2: (apply (<*a*>,t)) . 1 = t by Def19;
A3: len <*a*> = 1 by FINSEQ_1:40;
then A4: len (apply (<*a*>,t)) = 1 + 1 by Def19;
 1 in dom <*a*> by A3, FINSEQ_3:25;
then  (apply (<*a*>,t)) . ((len <*a*>) + 1) = a ast t by A3, A2, A1, Def19;
hence  apply (<*a*>,t) = <*t,(a ast t)*> by A3, A4, A2, FINSEQ_1:44; ::_thesis: verum
end;

definition
let T be non empty reflexive transitive non void TA-structure ;
let t be type of T;
let v be FinSequence of the adjectives of T;
funcv ast t ->  type of T equals :: ABCMIZ_0:def 20
(apply (v,t)) . ((len v) + 1);
coherence
 (apply (v,t)) . ((len v) + 1) is type of T
proof
A1: (len v) + 1 >= 1 by NAT_1:11;
 len (apply (v,t)) = (len v) + 1 by Def19;
then  (len v) + 1 in dom (apply (v,t)) by A1, FINSEQ_3:25;
hence  (apply (v,t)) . ((len v) + 1) is type of T by FINSEQ_2:11; ::_thesis: verum
end;
end;

:: deftheorem  defines ast ABCMIZ_0:def_20_:_
 for T being non empty reflexive transitive non void TA-structure
for t being type of T
for v being FinSequence of the adjectives of T holds v ast t = (apply (v,t)) . ((len v) + 1);

theorem :: ABCMIZ_0:30
for T being non empty reflexive transitive non void TA-structure
for t being type of T holds (<*> the adjectives of T) ast t = t by Def19;

theorem Th31: :: ABCMIZ_0:31
for T being non empty reflexive transitive non void TA-structure
for t being type of T
for a being adjective of T holds <*a*> ast t = a ast t
proof
let T be non empty reflexive transitive non void TA-structure ; ::_thesis: for t being type of T
for a being adjective of T holds <*a*> ast t = a ast t
let t be type of T; ::_thesis: for a being adjective of T holds <*a*> ast t = a ast t
let a be adjective of T; ::_thesis: <*a*> ast t = a ast t
A1: len <*a*> = 1 by FINSEQ_1:40;
 apply (<*a*>,t) = <*t,(a ast t)*> by Th29;
hence  <*a*> ast t = a ast t by A1, FINSEQ_1:44; ::_thesis: verum
end;

theorem :: ABCMIZ_0:32
for p, q being FinSequence
for i being Nat st i >= 1 & i < len p holds
(p $^ q) . i = p . i
proof
let p, q be FinSequence; ::_thesis: for i being Nat st i >= 1 & i < len p holds
(p $^ q) . i = p . i
let i be Nat; ::_thesis: ( i >= 1 & i < len p implies (p $^ q) . i = p . i )
assume that
A1: i >= 1 and
A2: i < len p ; ::_thesis: (p $^ q) . i = p . i
percases ( q = {} or q <> {} ) ;
suppose q = {} ; ::_thesis: (p $^ q) . i = p . i
hence  (p $^ q) . i = p . i by REWRITE1:1; ::_thesis: verum
end;
suppose q <> {} ; ::_thesis: (p $^ q) . i = p . i
then consider j being Element of NAT , r being FinSequence such that
A3: len p = j + 1 and
A4: r = p | (Seg j) and
A5: p $^ q = r ^ q by A2, CARD_1:27, REWRITE1:def_1;
A6: p = r ^ <*(p . (len p))*> by A3, A4, FINSEQ_3:55;
 j < len p by A3, NAT_1:13;
then A7: len r = j by A4, FINSEQ_1:17;
 i <= j by A2, A3, NAT_1:13;
then A8: i in dom r by A1, A7, FINSEQ_3:25;
then  (p $^ q) . i = r . i by A5, FINSEQ_1:def_7;
hence  (p $^ q) . i = p . i by A8, A6, FINSEQ_1:def_7; ::_thesis: verum
end;
end;
end;

theorem Th33: :: ABCMIZ_0:33
for p being non empty FinSequence
for q being FinSequence
for i being Nat st i < len q holds
(p $^ q) . ((len p) + i) = q . (i + 1)
proof
let p be non empty FinSequence; ::_thesis: for q being FinSequence
for i being Nat st i < len q holds
(p $^ q) . ((len p) + i) = q . (i + 1)
let q be FinSequence; ::_thesis: for i being Nat st i < len q holds
(p $^ q) . ((len p) + i) = q . (i + 1)
let i be Nat; ::_thesis: ( i < len q implies (p $^ q) . ((len p) + i) = q . (i + 1) )
A1: i + 1 >= 1 by NAT_1:11;
assume A2: i < len q ; ::_thesis: (p $^ q) . ((len p) + i) = q . (i + 1)
then consider j being Element of NAT , r being FinSequence such that
A3: len p = j + 1 and
A4: r = p | (Seg j) and
A5: p $^ q = r ^ q by CARD_1:27, REWRITE1:def_1;
 i + 1 <= len q by A2, NAT_1:13;
then A6: i + 1 in dom q by A1, FINSEQ_3:25;
 j < len p by A3, NAT_1:13;
then  len r = j by A4, FINSEQ_1:17;
then  (len p) + i = (len r) + (i + 1) by A3;
hence  (p $^ q) . ((len p) + i) = q . (i + 1) by A5, A6, FINSEQ_1:def_7; ::_thesis: verum
end;

theorem Th34: :: ABCMIZ_0:34
for T being non empty reflexive transitive non void TA-structure
for t being type of T
for v1, v2 being FinSequence of the adjectives of T holds apply ((v1 ^ v2),t) = (apply (v1,t)) $^ (apply (v2,(v1 ast t)))
proof
let T be non empty reflexive transitive non void TA-structure ; ::_thesis: for t being type of T
for v1, v2 being FinSequence of the adjectives of T holds apply ((v1 ^ v2),t) = (apply (v1,t)) $^ (apply (v2,(v1 ast t)))
let t be type of T; ::_thesis: for v1, v2 being FinSequence of the adjectives of T holds apply ((v1 ^ v2),t) = (apply (v1,t)) $^ (apply (v2,(v1 ast t)))
let v1, v2 be FinSequence of the adjectives of T; ::_thesis: apply ((v1 ^ v2),t) = (apply (v1,t)) $^ (apply (v2,(v1 ast t)))
consider tt being FinSequence of the carrier of T, q being Element of T such that
A1: apply (v1,t) = tt ^ <*q*> by HILBERT2:4;
set s = (apply (v1,t)) $^ (apply (v2,(v1 ast t)));
set p = v1 ^ v2;
A2: len (apply (v1,t)) = (len v1) + 1 by Def19;
A3: (apply (v1,t)) $^ (apply (v2,(v1 ast t))) = tt ^ (apply (v2,(v1 ast t))) by A1, REWRITE1:2;
 len <*q*> = 1 by FINSEQ_1:39;
then A4: (len v1) + 1 = (len tt) + 1 by A2, A1, FINSEQ_1:22;
A5: ((apply (v1,t)) $^ (apply (v2,(v1 ast t)))) . 1 = t
proof
percases ( len v1 = 0 or len v1 > 0 ) ;
supposeA6: len v1 = 0 ; ::_thesis: ((apply (v1,t)) $^ (apply (v2,(v1 ast t)))) . 1 = t
then  tt = {} by A4;
then A7: (apply (v1,t)) $^ (apply (v2,(v1 ast t))) = apply (v2,(v1 ast t)) by A3, FINSEQ_1:34;
 v1 ast t = t by A6, Def19;
hence  ((apply (v1,t)) $^ (apply (v2,(v1 ast t)))) . 1 = t by A7, Def19; ::_thesis: verum
end;
suppose len v1 > 0 ; ::_thesis: ((apply (v1,t)) $^ (apply (v2,(v1 ast t)))) . 1 = t
then  len tt >= 0 + 1 by A4, NAT_1:13;
then A8: 1 in dom tt by FINSEQ_3:25;
then A9: tt . 1 = (apply (v1,t)) . 1 by A1, FINSEQ_1:def_7;
 ((apply (v1,t)) $^ (apply (v2,(v1 ast t)))) . 1 = tt . 1 by A3, A8, FINSEQ_1:def_7;
hence  ((apply (v1,t)) $^ (apply (v2,(v1 ast t)))) . 1 = t by A9, Def19; ::_thesis: verum
end;
end;
end;
A10: now__::_thesis:_for_i_being_Element_of_NAT_
for_a_being_adjective_of_T
for_t9_being_type_of_T_st_i_in_dom_(v1_^_v2)_&_a_=_(v1_^_v2)_._i_&_t9_=_((apply_(v1,t))_$^_(apply_(v2,(v1_ast_t))))_._i_holds_
((apply_(v1,t))_$^_(apply_(v2,(v1_ast_t))))_._(i_+_1)_=_a_ast_t9
A11: len (v1 ^ v2) = (len v1) + (len v2) by FINSEQ_1:22;
A12: len (apply (v2,(v1 ast t))) = (len v2) + 1 by Def19;
let i be Element of NAT ; ::_thesis: for a being adjective of T
for t9 being type of T st i in dom (v1 ^ v2) & a = (v1 ^ v2) . i & t9 = ((apply (v1,t)) $^ (apply (v2,(v1 ast t)))) . i holds
((apply (v1,t)) $^ (apply (v2,(v1 ast t)))) . (b3 + 1) = b4 ast b5
let a be adjective of T; ::_thesis: for t9 being type of T st i in dom (v1 ^ v2) & a = (v1 ^ v2) . i & t9 = ((apply (v1,t)) $^ (apply (v2,(v1 ast t)))) . i holds
((apply (v1,t)) $^ (apply (v2,(v1 ast t)))) . (b2 + 1) = b3 ast b4
let t9 be type of T; ::_thesis: ( i in dom (v1 ^ v2) & a = (v1 ^ v2) . i & t9 = ((apply (v1,t)) $^ (apply (v2,(v1 ast t)))) . i implies ((apply (v1,t)) $^ (apply (v2,(v1 ast t)))) . (b1 + 1) = b2 ast b3 )
assume that
A13: i in dom (v1 ^ v2) and
A14: a = (v1 ^ v2) . i and
A15: t9 = ((apply (v1,t)) $^ (apply (v2,(v1 ast t)))) . i ; ::_thesis: ((apply (v1,t)) $^ (apply (v2,(v1 ast t)))) . (b1 + 1) = b2 ast b3
A16: 1 <= i by A13, FINSEQ_3:25;
A17: i <= len (v1 ^ v2) by A13, FINSEQ_3:25;
percases ( i < len v1 or i = len v1 or i > len v1 ) by XXREAL_0:1;
supposeA18: i < len v1 ; ::_thesis: ((apply (v1,t)) $^ (apply (v2,(v1 ast t)))) . (b1 + 1) = b2 ast b3
A19: i + 1 >= 1 by NAT_1:11;
 i + 1 <= len v1 by A18, NAT_1:13;
then A20: i + 1 in dom tt by A4, A19, FINSEQ_3:25;
then A21: ((apply (v1,t)) $^ (apply (v2,(v1 ast t)))) . (i + 1) = tt . (i + 1) by A3, FINSEQ_1:def_7;
A22: i in dom tt by A4, A16, A18, FINSEQ_3:25;
then A23: ((apply (v1,t)) $^ (apply (v2,(v1 ast t)))) . i = tt . i by A3, FINSEQ_1:def_7;
A24: tt . (i + 1) = (apply (v1,t)) . (i + 1) by A1, A20, FINSEQ_1:def_7;
A25: tt . i = (apply (v1,t)) . i by A1, A22, FINSEQ_1:def_7;
A26: i in dom v1 by A16, A18, FINSEQ_3:25;
then  (v1 ^ v2) . i = v1 . i by FINSEQ_1:def_7;
hence  ((apply (v1,t)) $^ (apply (v2,(v1 ast t)))) . (i + 1) = a ast t9 by A14, A15, A26, A23, A25, A21, A24, Def19; ::_thesis: verum
end;
supposeA27: i = len v1 ; ::_thesis: ((apply (v1,t)) $^ (apply (v2,(v1 ast t)))) . (b1 + 1) = b2 ast b3
 1 <= len (apply (v2,(v1 ast t))) by A12, NAT_1:11;
then  1 in dom (apply (v2,(v1 ast t))) by FINSEQ_3:25;
then A28: ((apply (v1,t)) $^ (apply (v2,(v1 ast t)))) . (i + 1) = (apply (v2,(v1 ast t))) . 1 by A3, A4, A27, FINSEQ_1:def_7;
A29: i in dom tt by A4, A16, A27, FINSEQ_3:25;
then A30: ((apply (v1,t)) $^ (apply (v2,(v1 ast t)))) . i = tt . i by A3, FINSEQ_1:def_7;
A31: tt . i = (apply (v1,t)) . i by A1, A29, FINSEQ_1:def_7;
A32: i in dom v1 by A16, A27, FINSEQ_3:25;
then  (v1 ^ v2) . i = v1 . i by FINSEQ_1:def_7;
then  a ast t9 = v1 ast t by A14, A15, A27, A32, A30, A31, Def19;
hence  ((apply (v1,t)) $^ (apply (v2,(v1 ast t)))) . (i + 1) = a ast t9 by A28, Def19; ::_thesis: verum
end;
suppose i > len v1 ; ::_thesis: ((apply (v1,t)) $^ (apply (v2,(v1 ast t)))) . (b1 + 1) = b2 ast b3
then  i >= (len v1) + 1 by NAT_1:13;
then consider j being Nat such that
A33: i = ((len v1) + 1) + j by NAT_1:10;
A34: (1 + j) + 1 >= 1 by NAT_1:11;
A35: ((j + 1) + (len v1)) + 1 = ((j + 1) + 1) + (len v1) ;
A36: 1 + j >= 1 by NAT_1:11;
A37: i = (j + 1) + (len v1) by A33;
then A38: 1 + j <= len v2 by A17, A11, XREAL_1:6;
then  (1 + j) + 0 <= (len v2) + 1 by XREAL_1:7;
then  j + 1 in dom (apply (v2,(v1 ast t))) by A12, A36, FINSEQ_3:25;
then A39: ((apply (v1,t)) $^ (apply (v2,(v1 ast t)))) . i = (apply (v2,(v1 ast t))) . (j + 1) by A3, A4, A37, FINSEQ_1:def_7;
 (1 + j) + 1 <= (len v2) + 1 by A38, XREAL_1:7;
then  (j + 1) + 1 in dom (apply (v2,(v1 ast t))) by A12, A34, FINSEQ_3:25;
then A40: ((apply (v1,t)) $^ (apply (v2,(v1 ast t)))) . (i + 1) = (apply (v2,(v1 ast t))) . ((j + 1) + 1) by A3, A4, A33, A35, FINSEQ_1:def_7;
A41: j + 1 in dom v2 by A36, A38, FINSEQ_3:25;
then  (v1 ^ v2) . i = v2 . (j + 1) by A37, FINSEQ_1:def_7;
hence  ((apply (v1,t)) $^ (apply (v2,(v1 ast t)))) . (i + 1) = a ast t9 by A14, A15, A41, A39, A40, Def19; ::_thesis: verum
end;
end;
end;
 len (apply (v2,(v1 ast t))) = (len v2) + 1 by Def19;
then  len ((apply (v1,t)) $^ (apply (v2,(v1 ast t)))) = (len tt) + ((len v2) + 1) by A3, FINSEQ_1:22
.= ((len v1) + (len v2)) + 1 by A4
.= (len (v1 ^ v2)) + 1 by FINSEQ_1:22 ;
hence  apply ((v1 ^ v2),t) = (apply (v1,t)) $^ (apply (v2,(v1 ast t))) by A3, A5, A10, Def19; ::_thesis: verum
end;

theorem Th35: :: ABCMIZ_0:35
for T being non empty reflexive transitive non void TA-structure
for t being type of T
for v1, v2 being FinSequence of the adjectives of T
for i being Nat st i in dom v1 holds
(apply ((v1 ^ v2),t)) . i = (apply (v1,t)) . i
proof
let T be non empty reflexive transitive non void TA-structure ; ::_thesis: for t being type of T
for v1, v2 being FinSequence of the adjectives of T
for i being Nat st i in dom v1 holds
(apply ((v1 ^ v2),t)) . i = (apply (v1,t)) . i
let t be type of T; ::_thesis: for v1, v2 being FinSequence of the adjectives of T
for i being Nat st i in dom v1 holds
(apply ((v1 ^ v2),t)) . i = (apply (v1,t)) . i
let v1, v2 be FinSequence of the adjectives of T; ::_thesis: for i being Nat st i in dom v1 holds
(apply ((v1 ^ v2),t)) . i = (apply (v1,t)) . i
set v = v1 ^ v2;
consider tt being FinSequence of the carrier of T, q being Element of T such that
A1: apply (v1,t) = tt ^ <*q*> by HILBERT2:4;
let i be Nat; ::_thesis: ( i in dom v1 implies (apply ((v1 ^ v2),t)) . i = (apply (v1,t)) . i )
A2: len (apply (v1,t)) = (len v1) + 1 by Def19;
assume A3: i in dom v1 ; ::_thesis: (apply ((v1 ^ v2),t)) . i = (apply (v1,t)) . i
then A4: i >= 1 by FINSEQ_3:25;
 len <*q*> = 1 by FINSEQ_1:39;
then  (len v1) + 1 = (len tt) + 1 by A2, A1, FINSEQ_1:22;
then  i <= len tt by A3, FINSEQ_3:25;
then A5: i in dom tt by A4, FINSEQ_3:25;
apply ((v1 ^ v2),t) = (apply (v1,t)) $^ (apply (v2,(v1 ast t))) by Th34
.= tt ^ (apply (v2,(v1 ast t))) by A1, REWRITE1:2 ;
then  (apply ((v1 ^ v2),t)) . i = tt . i by A5, FINSEQ_1:def_7;
hence  (apply ((v1 ^ v2),t)) . i = (apply (v1,t)) . i by A1, A5, FINSEQ_1:def_7; ::_thesis: verum
end;

theorem Th36: :: ABCMIZ_0:36
for T being non empty reflexive transitive non void TA-structure
for t being type of T
for v1, v2 being FinSequence of the adjectives of T holds (apply ((v1 ^ v2),t)) . ((len v1) + 1) = v1 ast t
proof
let T be non empty reflexive transitive non void TA-structure ; ::_thesis: for t being type of T
for v1, v2 being FinSequence of the adjectives of T holds (apply ((v1 ^ v2),t)) . ((len v1) + 1) = v1 ast t
let t be type of T; ::_thesis: for v1, v2 being FinSequence of the adjectives of T holds (apply ((v1 ^ v2),t)) . ((len v1) + 1) = v1 ast t
let v1, v2 be FinSequence of the adjectives of T; ::_thesis: (apply ((v1 ^ v2),t)) . ((len v1) + 1) = v1 ast t
set v = v1 ^ v2;
A1: len (apply (v2,(v1 ast t))) = (len v2) + 1 by Def19;
A2: apply ((v1 ^ v2),t) = (apply (v1,t)) $^ (apply (v2,(v1 ast t))) by Th34;
 len (apply (v1,t)) = (len v1) + 1 by Def19;
then  (apply ((v1 ^ v2),t)) . (((len v1) + 1) + 0) = (apply (v2,(v1 ast t))) . (0 + 1) by A1, A2, Th33;
hence  (apply ((v1 ^ v2),t)) . ((len v1) + 1) = v1 ast t by Def19; ::_thesis: verum
end;

theorem Th37: :: ABCMIZ_0:37
for T being non empty reflexive transitive non void TA-structure
for t being type of T
for v1, v2 being FinSequence of the adjectives of T holds v2 ast (v1 ast t) = (v1 ^ v2) ast t
proof
let T be non empty reflexive transitive non void TA-structure ; ::_thesis: for t being type of T
for v1, v2 being FinSequence of the adjectives of T holds v2 ast (v1 ast t) = (v1 ^ v2) ast t
let t be type of T; ::_thesis: for v1, v2 being FinSequence of the adjectives of T holds v2 ast (v1 ast t) = (v1 ^ v2) ast t
let v1, v2 be FinSequence of the adjectives of T; ::_thesis: v2 ast (v1 ast t) = (v1 ^ v2) ast t
set v = v1 ^ v2;
consider tt being FinSequence of the carrier of T, q being Element of T such that
A1: apply (v1,t) = tt ^ <*q*> by HILBERT2:4;
A2: len (apply (v1,t)) = (len v1) + 1 by Def19;
 len <*q*> = 1 by FINSEQ_1:39;
then A3: (len v1) + 1 = (len tt) + 1 by A2, A1, FINSEQ_1:22;
A4: (len v2) + 1 >= 1 by NAT_1:11;
 len (apply (v2,(v1 ast t))) = (len v2) + 1 by Def19;
then A5: (len v2) + 1 in dom (apply (v2,(v1 ast t))) by A4, FINSEQ_3:25;
apply ((v1 ^ v2),t) = (apply (v1,t)) $^ (apply (v2,(v1 ast t))) by Th34
.= tt ^ (apply (v2,(v1 ast t))) by A1, REWRITE1:2 ;
hence v2 ast (v1 ast t) = (apply ((v1 ^ v2),t)) . ((len tt) + ((len v2) + 1)) by A5, FINSEQ_1:def_7
.= (apply ((v1 ^ v2),t)) . (((len v1) + (len v2)) + 1) by A3
.= (v1 ^ v2) ast t by FINSEQ_1:22 ;
::_thesis: verum
end;

definition
let T be non empty reflexive transitive non void TA-structure ;
let t be type of T;
let v be FinSequence of the adjectives of T;
predv is_applicable_to t means :Def21: :: ABCMIZ_0:def 21
 for i being Nat
for a being adjective of T
for s being type of T st i in dom v & a = v . i & s = (apply (v,t)) . i holds
a is_applicable_to s;
end;

:: deftheorem Def21 defines is_applicable_to ABCMIZ_0:def_21_:_
 for T being non empty reflexive transitive non void TA-structure
for t being type of T
for v being FinSequence of the adjectives of T holds
( v is_applicable_to t iff for i being Nat
for a being adjective of T
for s being type of T st i in dom v & a = v . i & s = (apply (v,t)) . i holds
a is_applicable_to s );

theorem :: ABCMIZ_0:38
for T being non empty reflexive transitive non void TA-structure
for t being type of T holds <*> the adjectives of T is_applicable_to t
proof
let T be non empty reflexive transitive non void TA-structure ; ::_thesis: for t being type of T holds <*> the adjectives of T is_applicable_to t
let t be type of T; ::_thesis: <*> the adjectives of T is_applicable_to t
let i be Nat; :: according to ABCMIZ_0:def_21 ::_thesis: for a being adjective of T
for s being type of T st i in dom (<*> the adjectives of T) & a = (<*> the adjectives of T) . i & s = (apply ((<*> the adjectives of T),t)) . i holds
a is_applicable_to s
thus  for a being adjective of T
for s being type of T st i in dom (<*> the adjectives of T) & a = (<*> the adjectives of T) . i & s = (apply ((<*> the adjectives of T),t)) . i holds
a is_applicable_to s ; ::_thesis: verum
end;

theorem :: ABCMIZ_0:39
for T being non empty reflexive transitive non void TA-structure
for t being type of T
for a being adjective of T holds
( a is_applicable_to t iff <*a*> is_applicable_to t )
proof
let T be non empty reflexive transitive non void TA-structure ; ::_thesis: for t being type of T
for a being adjective of T holds
( a is_applicable_to t iff <*a*> is_applicable_to t )
let t be type of T; ::_thesis: for a being adjective of T holds
( a is_applicable_to t iff <*a*> is_applicable_to t )
let a be adjective of T; ::_thesis: ( a is_applicable_to t iff <*a*> is_applicable_to t )
set v = <*a*>;
A1: <*a*> . 1 = a by FINSEQ_1:40;
hereby  ::_thesis: ( <*a*> is_applicable_to t implies a is_applicable_to t )
assume A2: a is_applicable_to t ; ::_thesis: <*a*> is_applicable_to t
thus  <*a*> is_applicable_to t ::_thesis: verum
proof
let i be Nat; :: according to ABCMIZ_0:def_21 ::_thesis: for a being adjective of T
for s being type of T st i in dom <*a*> & a = <*a*> . i & s = (apply (<*a*>,t)) . i holds
a is_applicable_to s
let b be adjective of T; ::_thesis: for s being type of T st i in dom <*a*> & b = <*a*> . i & s = (apply (<*a*>,t)) . i holds
b is_applicable_to s
let s be type of T; ::_thesis: ( i in dom <*a*> & b = <*a*> . i & s = (apply (<*a*>,t)) . i implies b is_applicable_to s )
assume  i in dom <*a*> ; ::_thesis: ( not b = <*a*> . i or not s = (apply (<*a*>,t)) . i or b is_applicable_to s )
then  i in Seg 1 by FINSEQ_1:38;
then A3: i = 1 by FINSEQ_1:2, TARSKI:def_1;
then  <*a*> . i = a by FINSEQ_1:40;
hence  ( not b = <*a*> . i or not s = (apply (<*a*>,t)) . i or b is_applicable_to s ) by A2, A3, Def19; ::_thesis: verum
end;
end;
assume A4: for i being Nat
for a9 being adjective of T
for s being type of T st i in dom <*a*> & a9 = <*a*> . i & s = (apply (<*a*>,t)) . i holds
a9 is_applicable_to s ; :: according to ABCMIZ_0:def_21 ::_thesis: a is_applicable_to t
 len <*a*> = 1 by FINSEQ_1:40;
then A5: 1 in dom <*a*> by FINSEQ_3:25;
 (apply (<*a*>,t)) . 1 = t by Def19;
hence  a is_applicable_to t by A4, A5, A1; ::_thesis: verum
end;

theorem Th40: :: ABCMIZ_0:40
for T being non empty reflexive transitive non void TA-structure
for t being type of T
for v1, v2 being FinSequence of the adjectives of T st v1 ^ v2 is_applicable_to t holds
( v1 is_applicable_to t & v2 is_applicable_to v1 ast t )
proof
let T be non empty reflexive transitive non void TA-structure ; ::_thesis: for t being type of T
for v1, v2 being FinSequence of the adjectives of T st v1 ^ v2 is_applicable_to t holds
( v1 is_applicable_to t & v2 is_applicable_to v1 ast t )
let t be type of T; ::_thesis: for v1, v2 being FinSequence of the adjectives of T st v1 ^ v2 is_applicable_to t holds
( v1 is_applicable_to t & v2 is_applicable_to v1 ast t )
let v1, v2 be FinSequence of the adjectives of T; ::_thesis: ( v1 ^ v2 is_applicable_to t implies ( v1 is_applicable_to t & v2 is_applicable_to v1 ast t ) )
set v = v1 ^ v2;
A1: apply ((v1 ^ v2),t) = (apply (v1,t)) $^ (apply (v2,(v1 ast t))) by Th34;
A2: len (apply (v2,(v1 ast t))) = (len v2) + 1 by Def19;
assume A3: for i being Nat
for a being adjective of T
for s being type of T st i in dom (v1 ^ v2) & a = (v1 ^ v2) . i & s = (apply ((v1 ^ v2),t)) . i holds
a is_applicable_to s ; :: according to ABCMIZ_0:def_21 ::_thesis: ( v1 is_applicable_to t & v2 is_applicable_to v1 ast t )
hereby  :: according to ABCMIZ_0:def_21 ::_thesis: v2 is_applicable_to v1 ast t
A4: dom v1 c= dom (v1 ^ v2) by FINSEQ_1:26;
let i be Nat; ::_thesis: for a being adjective of T
for s being type of T st i in dom v1 & a = v1 . i & s = (apply (v1,t)) . i holds
a is_applicable_to s
let a be adjective of T; ::_thesis: for s being type of T st i in dom v1 & a = v1 . i & s = (apply (v1,t)) . i holds
a is_applicable_to s
let s be type of T; ::_thesis: ( i in dom v1 & a = v1 . i & s = (apply (v1,t)) . i implies a is_applicable_to s )
assume that
A5: i in dom v1 and
A6: a = v1 . i and
A7: s = (apply (v1,t)) . i ; ::_thesis: a is_applicable_to s
A8: a = (v1 ^ v2) . i by A5, A6, FINSEQ_1:def_7;
 s = (apply ((v1 ^ v2),t)) . i by A5, A7, Th35;
hence  a is_applicable_to s by A3, A5, A4, A8; ::_thesis: verum
end;
let i be Nat; :: according to ABCMIZ_0:def_21 ::_thesis: for a being adjective of T
for s being type of T st i in dom v2 & a = v2 . i & s = (apply (v2,(v1 ast t))) . i holds
a is_applicable_to s
let a be adjective of T; ::_thesis: for s being type of T st i in dom v2 & a = v2 . i & s = (apply (v2,(v1 ast t))) . i holds
a is_applicable_to s
let s be type of T; ::_thesis: ( i in dom v2 & a = v2 . i & s = (apply (v2,(v1 ast t))) . i implies a is_applicable_to s )
assume that
A9: i in dom v2 and
A10: a = v2 . i and
A11: s = (apply (v2,(v1 ast t))) . i ; ::_thesis: a is_applicable_to s
A12: a = (v1 ^ v2) . ((len v1) + i) by A9, A10, FINSEQ_1:def_7;
 i >= 1 by A9, FINSEQ_3:25;
then consider j being Nat such that
A13: i = 1 + j by NAT_1:10;
 i <= len v2 by A9, FINSEQ_3:25;
then  j < len v2 by A13, NAT_1:13;
then A14: j < len (apply (v2,(v1 ast t))) by A2, NAT_1:13;
 len (apply (v1,t)) = (len v1) + 1 by Def19;
then  (len v1) + i = (len (apply (v1,t))) + j by A13;
then  s = (apply ((v1 ^ v2),t)) . ((len v1) + i) by A11, A1, A13, A14, Th33;
hence  a is_applicable_to s by A3, A9, A12, FINSEQ_1:28; ::_thesis: verum
end;

theorem Th41: :: ABCMIZ_0:41
for T being reflexive transitive antisymmetric with_suprema Noetherian non void adj-structured TA-structure
for t being type of T
for v being FinSequence of the adjectives of T st v is_applicable_to t holds
for i1, i2 being Nat st 1 <= i1 & i1 <= i2 & i2 <= (len v) + 1 holds
for t1, t2 being type of T st t1 = (apply (v,t)) . i1 & t2 = (apply (v,t)) . i2 holds
t2 <= t1
proof
let T be reflexive transitive antisymmetric with_suprema Noetherian non void adj-structured TA-structure ; ::_thesis: for t being type of T
for v being FinSequence of the adjectives of T st v is_applicable_to t holds
for i1, i2 being Nat st 1 <= i1 & i1 <= i2 & i2 <= (len v) + 1 holds
for t1, t2 being type of T st t1 = (apply (v,t)) . i1 & t2 = (apply (v,t)) . i2 holds
t2 <= t1
let t be type of T; ::_thesis: for v being FinSequence of the adjectives of T st v is_applicable_to t holds
for i1, i2 being Nat st 1 <= i1 & i1 <= i2 & i2 <= (len v) + 1 holds
for t1, t2 being type of T st t1 = (apply (v,t)) . i1 & t2 = (apply (v,t)) . i2 holds
t2 <= t1
let v be FinSequence of the adjectives of T; ::_thesis: ( v is_applicable_to t implies for i1, i2 being Nat st 1 <= i1 & i1 <= i2 & i2 <= (len v) + 1 holds
for t1, t2 being type of T st t1 = (apply (v,t)) . i1 & t2 = (apply (v,t)) . i2 holds
t2 <= t1 )
assume A1: for i being Nat
for a being adjective of T
for s being type of T st i in dom v & a = v . i & s = (apply (v,t)) . i holds
a is_applicable_to s ; :: according to ABCMIZ_0:def_21 ::_thesis: for i1, i2 being Nat st 1 <= i1 & i1 <= i2 & i2 <= (len v) + 1 holds
for t1, t2 being type of T st t1 = (apply (v,t)) . i1 & t2 = (apply (v,t)) . i2 holds
t2 <= t1
let i1, i2 be Nat; ::_thesis: ( 1 <= i1 & i1 <= i2 & i2 <= (len v) + 1 implies for t1, t2 being type of T st t1 = (apply (v,t)) . i1 & t2 = (apply (v,t)) . i2 holds
t2 <= t1 )
assume that
A2: 1 <= i1 and
A3: i1 <= i2 and
A4: i2 <= (len v) + 1 ; ::_thesis: for t1, t2 being type of T st t1 = (apply (v,t)) . i1 & t2 = (apply (v,t)) . i2 holds
t2 <= t1
consider j being Nat such that
A5: i2 = i1 + j by A3, NAT_1:10;
let s1, s2 be type of T; ::_thesis: ( s1 = (apply (v,t)) . i1 & s2 = (apply (v,t)) . i2 implies s2 <= s1 )
defpred S1[ Element of NAT ] means ( i1 + $1 <= len (apply (v,t)) implies for s being type of T st s = (apply (v,t)) . (i1 + $1) holds
s <= s1 );
A6: len (apply (v,t)) = (len v) + 1 by Def19;
A7: for i being Element of NAT st S1[i] holds
S1[i + 1]
proof
let i be Element of NAT ; ::_thesis: ( S1[i] implies S1[i + 1] )
assume that
A8: S1[i] and
A9: i1 + (i + 1) <= len (apply (v,t)) ; ::_thesis: for s being type of T st s = (apply (v,t)) . (i1 + (i + 1)) holds
s <= s1
 i1 <= i1 + i by NAT_1:11;
then A10: 1 <= i1 + i by A2, XXREAL_0:2;
A11: i1 + (i + 1) = (i1 + i) + 1 ;
then  i1 + i <= len v by A6, A9, XREAL_1:6;
then A12: i1 + i in dom v by A10, FINSEQ_3:25;
then  v . (i1 + i) in rng v by FUNCT_1:3;
then reconsider a = v . (i1 + i) as adjective of T ;
 i1 + i < (len v) + 1 by A6, A9, A11, NAT_1:13;
then  i1 + i in dom (apply (v,t)) by A6, A10, FINSEQ_3:25;
then  (apply (v,t)) . (i1 + i) in rng (apply (v,t)) by FUNCT_1:3;
then reconsider s = (apply (v,t)) . (i1 + i) as type of T ;
A13: (apply (v,t)) . ((i1 + i) + 1) = a ast s by A12, Def19;
A14: a ast s <= s by A1, A12, Th20;
 s <= s1 by A8, A9, A11, NAT_1:13;
hence  for s being type of T st s = (apply (v,t)) . (i1 + (i + 1)) holds
s <= s1 by A13, A14, YELLOW_0:def_2; ::_thesis: verum
end;
A15: j in NAT by ORDINAL1:def_12;
assume that
A16: s1 = (apply (v,t)) . i1 and
A17: s2 = (apply (v,t)) . i2 ; ::_thesis: s2 <= s1
A18: S1[ 0 ] by A16;
 for i being Element of NAT holds S1[i] from NAT_1:sch_1(A18, A7);
hence  s2 <= s1 by A4, A5, A15, A6, A17; ::_thesis: verum
end;

theorem Th42: :: ABCMIZ_0:42
for T being reflexive transitive antisymmetric with_suprema Noetherian non void adj-structured TA-structure
for t being type of T
for v being FinSequence of the adjectives of T st v is_applicable_to t holds
for s being type of T st s in rng (apply (v,t)) holds
( v ast t <= s & s <= t )
proof
let T be reflexive transitive antisymmetric with_suprema Noetherian non void adj-structured TA-structure ; ::_thesis: for t being type of T
for v being FinSequence of the adjectives of T st v is_applicable_to t holds
for s being type of T st s in rng (apply (v,t)) holds
( v ast t <= s & s <= t )
let t be type of T; ::_thesis: for v being FinSequence of the adjectives of T st v is_applicable_to t holds
for s being type of T st s in rng (apply (v,t)) holds
( v ast t <= s & s <= t )
let v be FinSequence of the adjectives of T; ::_thesis: ( v is_applicable_to t implies for s being type of T st s in rng (apply (v,t)) holds
( v ast t <= s & s <= t ) )
assume A1: v is_applicable_to t ; ::_thesis: for s being type of T st s in rng (apply (v,t)) holds
( v ast t <= s & s <= t )
A2: len (apply (v,t)) = (len v) + 1 by Def19;
let s be type of T; ::_thesis: ( s in rng (apply (v,t)) implies ( v ast t <= s & s <= t ) )
assume  s in rng (apply (v,t)) ; ::_thesis: ( v ast t <= s & s <= t )
then consider x being set  such that
A3: x in dom (apply (v,t)) and
A4: s = (apply (v,t)) . x by FUNCT_1:def_3;
reconsider x = x as Element of NAT by A3;
A5: x <= len (apply (v,t)) by A3, FINSEQ_3:25;
A6: (apply (v,t)) . 1 = t by Def19;
 x >= 1 by A3, FINSEQ_3:25;
hence  ( v ast t <= s & s <= t ) by A1, A4, A5, A2, A6, Th41; ::_thesis: verum
end;

theorem Th43: :: ABCMIZ_0:43
for T being reflexive transitive antisymmetric with_suprema Noetherian non void adj-structured TA-structure
for t being type of T
for v being FinSequence of the adjectives of T st v is_applicable_to t holds
v ast t <= t
proof
let T be reflexive transitive antisymmetric with_suprema Noetherian non void adj-structured TA-structure ; ::_thesis: for t being type of T
for v being FinSequence of the adjectives of T st v is_applicable_to t holds
v ast t <= t
let t be type of T; ::_thesis: for v being FinSequence of the adjectives of T st v is_applicable_to t holds
v ast t <= t
let v be FinSequence of the adjectives of T; ::_thesis: ( v is_applicable_to t implies v ast t <= t )
assume A1: v is_applicable_to t ; ::_thesis: v ast t <= t
A2: (len v) + 1 >= 1 by NAT_1:11;
 len (apply (v,t)) = (len v) + 1 by Def19;
then  (len v) + 1 in dom (apply (v,t)) by A2, FINSEQ_3:25;
then  (apply (v,t)) . ((len v) + 1) in rng (apply (v,t)) by FUNCT_1:3;
hence  v ast t <= t by A1, Th42; ::_thesis: verum
end;

theorem Th44: :: ABCMIZ_0:44
for T being reflexive transitive antisymmetric with_suprema Noetherian non void adj-structured TA-structure
for t being type of T
for v being FinSequence of the adjectives of T st v is_applicable_to t holds
rng v c= adjs (v ast t)
proof
let T be reflexive transitive antisymmetric with_suprema Noetherian non void adj-structured TA-structure ; ::_thesis: for t being type of T
for v being FinSequence of the adjectives of T st v is_applicable_to t holds
rng v c= adjs (v ast t)
let t be type of T; ::_thesis: for v being FinSequence of the adjectives of T st v is_applicable_to t holds
rng v c= adjs (v ast t)
let v be FinSequence of the adjectives of T; ::_thesis: ( v is_applicable_to t implies rng v c= adjs (v ast t) )
assume A1: v is_applicable_to t ; ::_thesis: rng v c= adjs (v ast t)
let a be set ; :: according to TARSKI:def_3 ::_thesis: ( not a in rng v or a in adjs (v ast t) )
assume A2: a in rng v ; ::_thesis: a in adjs (v ast t)
then consider x being set  such that
A3: x in dom v and
A4: a = v . x by FUNCT_1:def_3;
reconsider a = a as adjective of T by A2;
reconsider x = x as Element of NAT by A3;
A5: x >= 1 by A3, FINSEQ_3:25;
then A6: x + 1 >= 1 by NAT_1:13;
A7: len (apply (v,t)) = (len v) + 1 by Def19;
A8: x <= len v by A3, FINSEQ_3:25;
then  x + 1 <= len (apply (v,t)) by A7, XREAL_1:6;
then  x + 1 in dom (apply (v,t)) by A6, FINSEQ_3:25;
then A9: (apply (v,t)) . (x + 1) in rng (apply (v,t)) by FUNCT_1:3;
 x < len (apply (v,t)) by A8, A7, NAT_1:13;
then  x in dom (apply (v,t)) by A5, FINSEQ_3:25;
then  (apply (v,t)) . x in rng (apply (v,t)) by FUNCT_1:3;
then reconsider s = (apply (v,t)) . x as type of T ;
 a ast s = (apply (v,t)) . (x + 1) by A3, A4, Def19;
then  a ast s >= v ast t by A1, A9, Th42;
then A10: adjs (a ast s) c= adjs (v ast t) by Th10;
 a is_applicable_to s by A1, A3, A4, Def21;
then  a in adjs (a ast s) by Th21;
hence  a in adjs (v ast t) by A10; ::_thesis: verum
end;

theorem Th45: :: ABCMIZ_0:45
for T being reflexive transitive antisymmetric with_suprema Noetherian non void adj-structured TA-structure
for t being type of T
for v being FinSequence of the adjectives of T st v is_applicable_to t holds
for A being Subset of the adjectives of T st A = rng v holds
A is_applicable_to t
proof
let T be reflexive transitive antisymmetric with_suprema Noetherian non void adj-structured TA-structure ; ::_thesis: for t being type of T
for v being FinSequence of the adjectives of T st v is_applicable_to t holds
for A being Subset of the adjectives of T st A = rng v holds
A is_applicable_to t
let t be type of T; ::_thesis: for v being FinSequence of the adjectives of T st v is_applicable_to t holds
for A being Subset of the adjectives of T st A = rng v holds
A is_applicable_to t
let v be FinSequence of the adjectives of T; ::_thesis: ( v is_applicable_to t implies for A being Subset of the adjectives of T st A = rng v holds
A is_applicable_to t )
assume A1: v is_applicable_to t ; ::_thesis: for A being Subset of the adjectives of T st A = rng v holds
A is_applicable_to t
then A2: rng v c= adjs (v ast t) by Th44;
 v ast t <= t by A1, Th43;
hence  for A being Subset of the adjectives of T st A = rng v holds
A is_applicable_to t by A2, Def16; ::_thesis: verum
end;

theorem Th46: :: ABCMIZ_0:46
for T being reflexive transitive antisymmetric with_suprema Noetherian non void adj-structured TA-structure
for t being type of T
for v1, v2 being FinSequence of the adjectives of T st v1 is_applicable_to t & rng v2 c= rng v1 holds
for s being type of T st s in rng (apply (v2,t)) holds
v1 ast t <= s
proof
let T be reflexive transitive antisymmetric with_suprema Noetherian non void adj-structured TA-structure ; ::_thesis: for t being type of T
for v1, v2 being FinSequence of the adjectives of T st v1 is_applicable_to t & rng v2 c= rng v1 holds
for s being type of T st s in rng (apply (v2,t)) holds
v1 ast t <= s
let t be type of T; ::_thesis: for v1, v2 being FinSequence of the adjectives of T st v1 is_applicable_to t & rng v2 c= rng v1 holds
for s being type of T st s in rng (apply (v2,t)) holds
v1 ast t <= s
let v, v9 be FinSequence of the adjectives of T; ::_thesis: ( v is_applicable_to t & rng v9 c= rng v implies for s being type of T st s in rng (apply (v9,t)) holds
v ast t <= s )
assume that
A1: v is_applicable_to t and
A2: rng v9 c= rng v ; ::_thesis: for s being type of T st s in rng (apply (v9,t)) holds
v ast t <= s
defpred S1[ Nat] means ( $1 <= len (apply (v9,t)) implies for s being type of T st s = (apply (v9,t)) . $1 holds
v ast t <= s );
A3: for i being non empty Nat st S1[i] holds
S1[i + 1]
proof
A4: rng v c= adjs (v ast t) by A1, Th44;
let i be non empty Nat; ::_thesis: ( S1[i] implies S1[i + 1] )
assume that
A5: S1[i] and
A6: i + 1 <= len (apply (v9,t)) ; ::_thesis: for s being type of T st s = (apply (v9,t)) . (i + 1) holds
v ast t <= s
A7: 0 + 1 <= i by NAT_1:13;
A8: len (apply (v9,t)) = (len v9) + 1 by Def19;
then  i < (len v9) + 1 by A6, NAT_1:13;
then  i in dom (apply (v9,t)) by A8, A7, FINSEQ_3:25;
then  (apply (v9,t)) . i in rng (apply (v9,t)) by FUNCT_1:3;
then reconsider s = (apply (v9,t)) . i as type of T ;
A9: v ast t <= s by A5, A6, NAT_1:13;
 i <= len v9 by A6, A8, XREAL_1:6;
then A10: i in dom v9 by A7, FINSEQ_3:25;
then A11: v9 . i in rng v9 by FUNCT_1:3;
then reconsider a = v9 . i as adjective of T ;
A12: a in rng v by A2, A11;
 (apply (v9,t)) . (i + 1) = a ast s by A10, Def19;
hence  for s being type of T st s = (apply (v9,t)) . (i + 1) holds
v ast t <= s by A12, A4, A9, Th23; ::_thesis: verum
end;
 (apply (v9,t)) . 1 = t by Def19;
then A13: S1[1] by A1, Th43;
A14: for i being non empty Nat holds S1[i] from NAT_1:sch_10(A13, A3);
let s be type of T; ::_thesis: ( s in rng (apply (v9,t)) implies v ast t <= s )
assume  s in rng (apply (v9,t)) ; ::_thesis: v ast t <= s
then consider x being set  such that
A15: x in dom (apply (v9,t)) and
A16: s = (apply (v9,t)) . x by FUNCT_1:def_3;
A17: x in Seg (len (apply (v9,t))) by A15, FINSEQ_1:def_3;
reconsider x = x as Element of NAT by A15;
reconsider x = x as non empty Element of NAT by A17, FINSEQ_1:1;
 x <= len (apply (v9,t)) by A15, FINSEQ_3:25;
hence  v ast t <= s by A16, A14; ::_thesis: verum
end;

theorem Th47: :: ABCMIZ_0:47
for T being reflexive transitive antisymmetric with_suprema Noetherian non void adj-structured TA-structure
for t being type of T
for v1, v2 being FinSequence of the adjectives of T st v1 ^ v2 is_applicable_to t holds
v2 ^ v1 is_applicable_to t
proof
let T be reflexive transitive antisymmetric with_suprema Noetherian non void adj-structured TA-structure ; ::_thesis: for t being type of T
for v1, v2 being FinSequence of the adjectives of T st v1 ^ v2 is_applicable_to t holds
v2 ^ v1 is_applicable_to t
let t be type of T; ::_thesis: for v1, v2 being FinSequence of the adjectives of T st v1 ^ v2 is_applicable_to t holds
v2 ^ v1 is_applicable_to t
let v1, v2 be FinSequence of the adjectives of T; ::_thesis: ( v1 ^ v2 is_applicable_to t implies v2 ^ v1 is_applicable_to t )
A1: rng (v1 ^ v2) = (rng v1) \/ (rng v2) by FINSEQ_1:31;
assume A2: v1 ^ v2 is_applicable_to t ; ::_thesis: v2 ^ v1 is_applicable_to t
then A3: rng (v1 ^ v2) c= adjs ((v1 ^ v2) ast t) by Th44;
let i be Nat; :: according to ABCMIZ_0:def_21 ::_thesis: for a being adjective of T
for s being type of T st i in dom (v2 ^ v1) & a = (v2 ^ v1) . i & s = (apply ((v2 ^ v1),t)) . i holds
a is_applicable_to s
let a be adjective of T; ::_thesis: for s being type of T st i in dom (v2 ^ v1) & a = (v2 ^ v1) . i & s = (apply ((v2 ^ v1),t)) . i holds
a is_applicable_to s
let s be type of T; ::_thesis: ( i in dom (v2 ^ v1) & a = (v2 ^ v1) . i & s = (apply ((v2 ^ v1),t)) . i implies a is_applicable_to s )
assume that
A4: i in dom (v2 ^ v1) and
A5: a = (v2 ^ v1) . i and
A6: s = (apply ((v2 ^ v1),t)) . i ; ::_thesis: a is_applicable_to s
A7: a in rng (v2 ^ v1) by A4, A5, FUNCT_1:3;
A8: len (apply ((v2 ^ v1),t)) = (len (v2 ^ v1)) + 1 by Def19;
A9: rng (v2 ^ v1) = (rng v1) \/ (rng v2) by FINSEQ_1:31;
 i <= len (v2 ^ v1) by A4, FINSEQ_3:25;
then A10: i < (len (v2 ^ v1)) + 1 by NAT_1:13;
 i >= 1 by A4, FINSEQ_3:25;
then  i in dom (apply ((v2 ^ v1),t)) by A10, A8, FINSEQ_3:25;
then  s in rng (apply ((v2 ^ v1),t)) by A6, FUNCT_1:3;
then  (v1 ^ v2) ast t <= s by A2, A1, A9, Th46;
hence  a is_applicable_to s by A1, A9, A7, A3, Th23; ::_thesis: verum
end;

theorem :: ABCMIZ_0:48
for T being reflexive transitive antisymmetric with_suprema Noetherian non void adj-structured TA-structure
for t being type of T
for v1, v2 being FinSequence of the adjectives of T st v1 ^ v2 is_applicable_to t holds
(v1 ^ v2) ast t = (v2 ^ v1) ast t
proof
let T be reflexive transitive antisymmetric with_suprema Noetherian non void adj-structured TA-structure ; ::_thesis: for t being type of T
for v1, v2 being FinSequence of the adjectives of T st v1 ^ v2 is_applicable_to t holds
(v1 ^ v2) ast t = (v2 ^ v1) ast t
let t be type of T; ::_thesis: for v1, v2 being FinSequence of the adjectives of T st v1 ^ v2 is_applicable_to t holds
(v1 ^ v2) ast t = (v2 ^ v1) ast t
let v1, v2 be FinSequence of the adjectives of T; ::_thesis: ( v1 ^ v2 is_applicable_to t implies (v1 ^ v2) ast t = (v2 ^ v1) ast t )
assume A1: v1 ^ v2 is_applicable_to t ; ::_thesis: (v1 ^ v2) ast t = (v2 ^ v1) ast t
A2: len (v1 ^ v2) = (len v1) + (len v2) by FINSEQ_1:22;
A3: rng (v1 ^ v2) = (rng v1) \/ (rng v2) by FINSEQ_1:31;
A4: len (v2 ^ v1) = (len v1) + (len v2) by FINSEQ_1:22;
A5: (len (v1 ^ v2)) + 1 >= 1 by NAT_1:11;
A6: rng (v2 ^ v1) = (rng v1) \/ (rng v2) by FINSEQ_1:31;
 len (apply ((v2 ^ v1),t)) = (len (v2 ^ v1)) + 1 by Def19;
then  (len (v1 ^ v2)) + 1 in dom (apply ((v2 ^ v1),t)) by A2, A4, A5, FINSEQ_3:25;
then  (v2 ^ v1) ast t in rng (apply ((v2 ^ v1),t)) by A2, A4, FUNCT_1:3;
then A7: (v1 ^ v2) ast t <= (v2 ^ v1) ast t by A1, A3, A6, Th46;
 len (apply ((v1 ^ v2),t)) = (len (v1 ^ v2)) + 1 by Def19;
then  (len (v1 ^ v2)) + 1 in dom (apply ((v1 ^ v2),t)) by A5, FINSEQ_3:25;
then  (v1 ^ v2) ast t in rng (apply ((v1 ^ v2),t)) by FUNCT_1:3;
then  (v2 ^ v1) ast t <= (v1 ^ v2) ast t by A1, A3, A6, Th46, Th47;
hence  (v1 ^ v2) ast t = (v2 ^ v1) ast t by A7, YELLOW_0:def_3; ::_thesis: verum
end;

theorem Th49: :: ABCMIZ_0:49
for T being reflexive transitive antisymmetric with_suprema Noetherian adj-structured TA-structure
for t being type of T
for A being Subset of the adjectives of T st A is_applicable_to t holds
A ast t <= t
proof
let T be reflexive transitive antisymmetric with_suprema Noetherian adj-structured TA-structure ; ::_thesis: for t being type of T
for A being Subset of the adjectives of T st A is_applicable_to t holds
A ast t <= t
let t be type of T; ::_thesis: for A being Subset of the adjectives of T st A is_applicable_to t holds
A ast t <= t
let a be Subset of the adjectives of T; ::_thesis: ( a is_applicable_to t implies a ast t <= t )
assume  a is_applicable_to t ; ::_thesis: a ast t <= t
then  (types a) /\ (downarrow t) is Ideal of T by Th26;
then  sup ((types a) /\ (downarrow t)) in (types a) /\ (downarrow t) by Th1;
then  a ast t in downarrow t by XBOOLE_0:def_4;
hence  a ast t <= t by WAYBEL_0:17; ::_thesis: verum
end;

theorem Th50: :: ABCMIZ_0:50
for T being reflexive transitive antisymmetric with_suprema Noetherian adj-structured TA-structure
for t being type of T
for A being Subset of the adjectives of T st A is_applicable_to t holds
A c= adjs (A ast t)
proof
let T be reflexive transitive antisymmetric with_suprema Noetherian adj-structured TA-structure ; ::_thesis: for t being type of T
for A being Subset of the adjectives of T st A is_applicable_to t holds
A c= adjs (A ast t)
let t be type of T; ::_thesis: for A being Subset of the adjectives of T st A is_applicable_to t holds
A c= adjs (A ast t)
let a be Subset of the adjectives of T; ::_thesis: ( a is_applicable_to t implies a c= adjs (a ast t) )
assume  a is_applicable_to t ; ::_thesis: a c= adjs (a ast t)
then  (types a) /\ (downarrow t) is Ideal of T by Th26;
then  sup ((types a) /\ (downarrow t)) in (types a) /\ (downarrow t) by Th1;
then  a ast t in types a by XBOOLE_0:def_4;
hence  a c= adjs (a ast t) by Th14; ::_thesis: verum
end;

theorem :: ABCMIZ_0:51
for T being reflexive transitive antisymmetric with_suprema Noetherian adj-structured TA-structure
for t being type of T
for A being Subset of the adjectives of T st A is_applicable_to t holds
A ast t in types A
proof
let T be reflexive transitive antisymmetric with_suprema Noetherian adj-structured TA-structure ; ::_thesis: for t being type of T
for A being Subset of the adjectives of T st A is_applicable_to t holds
A ast t in types A
let t be type of T; ::_thesis: for A being Subset of the adjectives of T st A is_applicable_to t holds
A ast t in types A
let a be Subset of the adjectives of T; ::_thesis: ( a is_applicable_to t implies a ast t in types a )
assume  a is_applicable_to t ; ::_thesis: a ast t in types a
then  (types a) /\ (downarrow t) is Ideal of T by Th26;
then  sup ((types a) /\ (downarrow t)) in (types a) /\ (downarrow t) by Th1;
hence  a ast t in types a by XBOOLE_0:def_4; ::_thesis: verum
end;

theorem Th52: :: ABCMIZ_0:52
for T being reflexive transitive antisymmetric with_suprema Noetherian adj-structured TA-structure
for t being type of T
for A being Subset of the adjectives of T
for t9 being type of T st t9 <= t & A c= adjs t9 holds
( A is_applicable_to t & t9 <= A ast t )
proof
let T be reflexive transitive antisymmetric with_suprema Noetherian adj-structured TA-structure ; ::_thesis: for t being type of T
for A being Subset of the adjectives of T
for t9 being type of T st t9 <= t & A c= adjs t9 holds
( A is_applicable_to t & t9 <= A ast t )
let t be type of T; ::_thesis: for A being Subset of the adjectives of T
for t9 being type of T st t9 <= t & A c= adjs t9 holds
( A is_applicable_to t & t9 <= A ast t )
let a be Subset of the adjectives of T; ::_thesis: for t9 being type of T st t9 <= t & a c= adjs t9 holds
( a is_applicable_to t & t9 <= a ast t )
let t9 be type of T; ::_thesis: ( t9 <= t & a c= adjs t9 implies ( a is_applicable_to t & t9 <= a ast t ) )
assume that
A1: t9 <= t and
A2: a c= adjs t9 ; ::_thesis: ( a is_applicable_to t & t9 <= a ast t )
A3: t9 in downarrow t by A1, WAYBEL_0:17;
thus  a is_applicable_to t ::_thesis: t9 <= a ast t
proof
take  t9 ; :: according to ABCMIZ_0:def_16 ::_thesis: ( a c= adjs t9 & t9 <= t )
thus  ( a c= adjs t9 & t9 <= t ) by A1, A2; ::_thesis: verum
end;
then  (types a) /\ (downarrow t) is Ideal of T by Th26;
then  ex_sup_of (types a) /\ (downarrow t),T by Th1;
then A4: a ast t is_>=_than (types a) /\ (downarrow t) by YELLOW_0:30;
 t9 in types a by A2, Th14;
then  t9 in (types a) /\ (downarrow t) by A3, XBOOLE_0:def_4;
hence  t9 <= a ast t by A4, LATTICE3:def_9; ::_thesis: verum
end;

theorem :: ABCMIZ_0:53
for T being reflexive transitive antisymmetric with_suprema Noetherian adj-structured TA-structure
for t being type of T
for A being Subset of the adjectives of T st A c= adjs t holds
( A is_applicable_to t & A ast t = t )
proof
let T be reflexive transitive antisymmetric with_suprema Noetherian adj-structured TA-structure ; ::_thesis: for t being type of T
for A being Subset of the adjectives of T st A c= adjs t holds
( A is_applicable_to t & A ast t = t )
let t be type of T; ::_thesis: for A being Subset of the adjectives of T st A c= adjs t holds
( A is_applicable_to t & A ast t = t )
let a be Subset of the adjectives of T; ::_thesis: ( a c= adjs t implies ( a is_applicable_to t & a ast t = t ) )
assume A1: a c= adjs t ; ::_thesis: ( a is_applicable_to t & a ast t = t )
hence  a is_applicable_to t by Th52; ::_thesis: a ast t = t
then A2: a ast t <= t by Th49;
 t <= a ast t by A1, Th52;
hence  a ast t = t by A2, YELLOW_0:def_3; ::_thesis: verum
end;

theorem Th54: :: ABCMIZ_0:54
for T being TA-structure
for t being type of T
for A, B being Subset of the adjectives of T st A is_applicable_to t & B c= A holds
B is_applicable_to t
proof
let T be TA-structure ; ::_thesis: for t being type of T
for A, B being Subset of the adjectives of T st A is_applicable_to t & B c= A holds
B is_applicable_to t
let t be type of T; ::_thesis: for A, B being Subset of the adjectives of T st A is_applicable_to t & B c= A holds
B is_applicable_to t
let A, B be Subset of the adjectives of T; ::_thesis: ( A is_applicable_to t & B c= A implies B is_applicable_to t )
given t9 being type of T such that A1: A c= adjs t9 and
A2: t9 <= t ; :: according to ABCMIZ_0:def_16 ::_thesis: ( not B c= A or B is_applicable_to t )
assume A3: B c= A ; ::_thesis: B is_applicable_to t
take  t9 ; :: according to ABCMIZ_0:def_16 ::_thesis: ( B c= adjs t9 & t9 <= t )
thus  ( B c= adjs t9 & t9 <= t ) by A1, A2, A3, XBOOLE_1:1; ::_thesis: verum
end;

theorem Th55: :: ABCMIZ_0:55
for T being reflexive transitive antisymmetric with_suprema Noetherian non void adj-structured TA-structure
for t being type of T
for a being adjective of T
for A, B being Subset of the adjectives of T st B = A \/ {a} & B is_applicable_to t holds
a ast (A ast t) = B ast t
proof
let T be reflexive transitive antisymmetric with_suprema Noetherian non void adj-structured TA-structure ; ::_thesis: for t being type of T
for a being adjective of T
for A, B being Subset of the adjectives of T st B = A \/ {a} & B is_applicable_to t holds
a ast (A ast t) = B ast t
let t be type of T; ::_thesis: for a being adjective of T
for A, B being Subset of the adjectives of T st B = A \/ {a} & B is_applicable_to t holds
a ast (A ast t) = B ast t
let a be adjective of T; ::_thesis: for A, B being Subset of the adjectives of T st B = A \/ {a} & B is_applicable_to t holds
a ast (A ast t) = B ast t
let A, B be Subset of the adjectives of T; ::_thesis: ( B = A \/ {a} & B is_applicable_to t implies a ast (A ast t) = B ast t )
assume that
A1: B = A \/ {a} and
A2: B is_applicable_to t ; ::_thesis: a ast (A ast t) = B ast t
A3: A is_applicable_to t by A1, A2, Th54, XBOOLE_1:7;
A4: {a} c= B by A1, XBOOLE_1:7;
A5: A c= B by A1, XBOOLE_1:7;
 (types a) /\ (downarrow (A ast t)) = (types B) /\ (downarrow t)
proof
thus  (types a) /\ (downarrow (A ast t)) c= (types B) /\ (downarrow t) :: according to XBOOLE_0:def_10 ::_thesis: (types B) /\ (downarrow t) c= (types a) /\ (downarrow (A ast t))
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in (types a) /\ (downarrow (A ast t)) or x in (types B) /\ (downarrow t) )
assume A6: x in (types a) /\ (downarrow (A ast t)) ; ::_thesis: x in (types B) /\ (downarrow t)
then reconsider t9 = x as type of T ;
 x in types a by A6, XBOOLE_0:def_4;
then  a in adjs t9 by Th13;
then A7: {a} c= adjs t9 by ZFMISC_1:31;
 x in downarrow (A ast t) by A6, XBOOLE_0:def_4;
then A8: t9 <= A ast t by WAYBEL_0:17;
then A9: adjs (A ast t) c= adjs t9 by Th10;
 A ast t <= t by A3, Th49;
then  t9 <= t by A8, YELLOW_0:def_2;
then A10: t9 in downarrow t by WAYBEL_0:17;
 A c= adjs (A ast t) by A3, Th50;
then  A c= adjs t9 by A9, XBOOLE_1:1;
then  B c= adjs t9 by A1, A7, XBOOLE_1:8;
then  t9 in types B by Th14;
hence  x in (types B) /\ (downarrow t) by A10, XBOOLE_0:def_4; ::_thesis: verum
end;
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in (types B) /\ (downarrow t) or x in (types a) /\ (downarrow (A ast t)) )
assume A11: x in (types B) /\ (downarrow t) ; ::_thesis: x in (types a) /\ (downarrow (A ast t))
then reconsider t9 = x as type of T ;
 x in downarrow t by A11, XBOOLE_0:def_4;
then A12: t9 <= t by WAYBEL_0:17;
 x in types B by A11, XBOOLE_0:def_4;
then A13: B c= adjs t9 by Th14;
then  A c= adjs t9 by A5, XBOOLE_1:1;
then  t9 <= A ast t by A12, Th52;
then A14: t9 in downarrow (A ast t) by WAYBEL_0:17;
 a in B by A4, ZFMISC_1:31;
then  t9 in types a by A13, Th13;
hence  x in (types a) /\ (downarrow (A ast t)) by A14, XBOOLE_0:def_4; ::_thesis: verum
end;
hence  a ast (A ast t) = B ast t ; ::_thesis: verum
end;

theorem Th56: :: ABCMIZ_0:56
for T being reflexive transitive antisymmetric with_suprema Noetherian non void adj-structured TA-structure
for t being type of T
for v being FinSequence of the adjectives of T st v is_applicable_to t holds
for A being Subset of the adjectives of T st A = rng v holds
v ast t = A ast t
proof
let T be reflexive transitive antisymmetric with_suprema Noetherian non void adj-structured TA-structure ; ::_thesis: for t being type of T
for v being FinSequence of the adjectives of T st v is_applicable_to t holds
for A being Subset of the adjectives of T st A = rng v holds
v ast t = A ast t
defpred S1[ Element of NAT ] means  for t being type of T
for v being FinSequence of the adjectives of T st $1 = len v & v is_applicable_to t holds
for A being Subset of the adjectives of T st A = rng v holds
v ast t = A ast t;
let t be type of T; ::_thesis: for v being FinSequence of the adjectives of T st v is_applicable_to t holds
for A being Subset of the adjectives of T st A = rng v holds
v ast t = A ast t
let v be FinSequence of the adjectives of T; ::_thesis: ( v is_applicable_to t implies for A being Subset of the adjectives of T st A = rng v holds
v ast t = A ast t )
A1: now__::_thesis:_for_n_being_Element_of_NAT_st_S1[n]_holds_
S1[n_+_1]
let n be Element of NAT ; ::_thesis: ( S1[n] implies S1[n + 1] )
assume A2: S1[n] ; ::_thesis: S1[n + 1]
now__::_thesis:_for_t_being_type_of_T
for_v_being_FinSequence_of_the_adjectives_of_T_st_n_+_1_=_len_v_&_v_is_applicable_to_t_holds_
for_A_being_Subset_of_the_adjectives_of_T_st_A_=_rng_v_holds_
v_ast_t_=_A_ast_t
let t be type of T; ::_thesis: for v being FinSequence of the adjectives of T st n + 1 = len v & v is_applicable_to t holds
for A being Subset of the adjectives of T st A = rng v holds
v ast t = A ast t
let v be FinSequence of the adjectives of T; ::_thesis: ( n + 1 = len v & v is_applicable_to t implies for A being Subset of the adjectives of T st A = rng v holds
v ast t = A ast t )
assume that
A3: n + 1 = len v and
A4: v is_applicable_to t ; ::_thesis: for A being Subset of the adjectives of T st A = rng v holds
v ast t = A ast t
consider v1 being FinSequence of the adjectives of T, a being Element of the adjectives of T such that
A5: v = v1 ^ <*a*> by A3, FINSEQ_2:19;
reconsider B = rng v1 as Subset of the adjectives of T ;
reconsider a = a as adjective of T ;
 len <*a*> = 1 by FINSEQ_1:40;
then A6: len v = (len v1) + 1 by A5, FINSEQ_1:22;
 v1 is_applicable_to t by A4, A5, Th40;
then A7: v1 ast t = B ast t by A2, A3, A6;
let A be Subset of the adjectives of T; ::_thesis: ( A = rng v implies v ast t = A ast t )
assume A8: A = rng v ; ::_thesis: v ast t = A ast t
then A9: A = B \/ (rng <*a*>) by A5, FINSEQ_1:31
.= B \/ {a} by FINSEQ_1:38 ;
thus v ast t = <*a*> ast (v1 ast t) by A5, Th37
.= a ast (B ast t) by A7, Th31
.= A ast t by A4, A8, A9, Th45, Th55 ; ::_thesis: verum
end;
hence  S1[n + 1] ; ::_thesis: verum
end;
A10: S1[ 0 ]
proof
let t be type of T; ::_thesis: for v being FinSequence of the adjectives of T st 0 = len v & v is_applicable_to t holds
for A being Subset of the adjectives of T st A = rng v holds
v ast t = A ast t
let v be FinSequence of the adjectives of T; ::_thesis: ( 0 = len v & v is_applicable_to t implies for A being Subset of the adjectives of T st A = rng v holds
v ast t = A ast t )
assume A11: 0 = len v ; ::_thesis: ( not v is_applicable_to t or for A being Subset of the adjectives of T st A = rng v holds
v ast t = A ast t )
then  v = <*> the adjectives of T ;
then A12: rng v = {} the adjectives of T ;
 v ast t = t by A11, Def19;
hence  ( not v is_applicable_to t or for A being Subset of the adjectives of T st A = rng v holds
v ast t = A ast t ) by A12, Th27; ::_thesis: verum
end;
 for n being Element of NAT holds S1[n] from NAT_1:sch_1(A10, A1);
hence  ( v is_applicable_to t implies for A being Subset of the adjectives of T st A = rng v holds
v ast t = A ast t ) ; ::_thesis: verum
end;

begin

definition
let T be non empty non void TA-structure ;
func sub T ->  Function of the adjectives of T, the carrier of T means :Def22: :: ABCMIZ_0:def 22
 for a being adjective of T holds it . a = sup ((types a) \/ (types (non- a)));
existence
 ex b1 being Function of the adjectives of T, the carrier of T st
for a being adjective of T holds b1 . a = sup ((types a) \/ (types (non- a)))
proof
deffunc H1( Element of the adjectives of T) ->  Element of the carrier of T = sup ((types $1) \/ (types (non- $1)));
consider f being Function of the adjectives of T, the carrier of T such that
A1: for a being Element of the adjectives of T holds f . a = H1(a) from FUNCT_2:sch_4();
take  f ; ::_thesis: for a being adjective of T holds f . a = sup ((types a) \/ (types (non- a)))
thus  for a being adjective of T holds f . a = sup ((types a) \/ (types (non- a))) by A1; ::_thesis: verum
end;
uniqueness
 for b1, b2 being Function of the adjectives of T, the carrier of T st ( for a being adjective of T holds b1 . a = sup ((types a) \/ (types (non- a))) ) & ( for a being adjective of T holds b2 . a = sup ((types a) \/ (types (non- a))) ) holds
b1 = b2
proof
let f1, f2 be Function of the adjectives of T, the carrier of T; ::_thesis: ( ( for a being adjective of T holds f1 . a = sup ((types a) \/ (types (non- a))) ) & ( for a being adjective of T holds f2 . a = sup ((types a) \/ (types (non- a))) ) implies f1 = f2 )
assume that
A2: for a being adjective of T holds f1 . a = sup ((types a) \/ (types (non- a))) and
A3: for a being adjective of T holds f2 . a = sup ((types a) \/ (types (non- a))) ; ::_thesis: f1 = f2
now__::_thesis:_for_a_being_Element_of_the_adjectives_of_T_holds_f1_._a_=_f2_._a
let a be Element of the adjectives of T; ::_thesis: f1 . a = f2 . a
reconsider b = a as adjective of T ;
thus f1 . a = sup ((types b) \/ (types (non- b))) by A2
.= f2 . a by A3 ; ::_thesis: verum
end;
hence  f1 = f2 by FUNCT_2:63; ::_thesis: verum
end;
end;

:: deftheorem Def22 defines sub ABCMIZ_0:def_22_:_
 for T being non empty non void TA-structure
for b2 being Function of the adjectives of T, the carrier of T holds
( b2 = sub T iff for a being adjective of T holds b2 . a = sup ((types a) \/ (types (non- a))) );

definition
attrc1 is strict ;
struct TAS-structure  ->  TA-structure ;
aggrTAS-structure(# carrier, adjectives, InternalRel, non-op, adj-map, sub-map #) ->  TAS-structure ;
sel sub-map c1 ->  Function of the adjectives of c1, the carrier of c1;
end;

registration
cluster1 -element reflexive non void strict for TAS-structure ;
existence
 ex b1 being TAS-structure st
( not b1 is void & b1 is reflexive & b1 is 1 -element & b1 is strict )
proof
set P = the 1 -element reflexive non void TA-structure ;
set s = the Function of the adjectives of the 1 -element reflexive non void TA-structure , the carrier of the 1 -element reflexive non void TA-structure ;
take T = TAS-structure(# the carrier of the 1 -element reflexive non void TA-structure , the adjectives of the 1 -element reflexive non void TA-structure , the InternalRel of the 1 -element reflexive non void TA-structure , the non-op of the 1 -element reflexive non void TA-structure , the adj-map of the 1 -element reflexive non void TA-structure , the Function of the adjectives of the 1 -element reflexive non void TA-structure , the carrier of the 1 -element reflexive non void TA-structure #); ::_thesis: ( not T is void & T is reflexive & T is 1 -element & T is strict )
 the carrier of the 1 -element reflexive non void TA-structure is 1 -element ;
 RelStr(# the carrier of the 1 -element reflexive non void TA-structure , the InternalRel of the 1 -element reflexive non void TA-structure #) = RelStr(# the carrier of T, the InternalRel of T #) ;
hence  ( not T is void & T is reflexive & T is 1 -element & T is strict ) by Def4, STRUCT_0:def_19, WAYBEL_8:12; ::_thesis: verum
end;
end;

definition
let T be non empty non void TAS-structure ;
let a be adjective of T;
func sub a ->  type of T equals :: ABCMIZ_0:def 23
 the sub-map of T . a;
coherence
 the sub-map of T . a is type of T ;
end;

:: deftheorem  defines sub ABCMIZ_0:def_23_:_
 for T being non empty non void TAS-structure
for a being adjective of T holds sub a = the sub-map of T . a;

definition
let T be non empty non void TAS-structure ;
attrT is non-absorbing  means :: ABCMIZ_0:def 24
 the sub-map of T * the non-op of T = the sub-map of T;
attrT is subjected  means :: ABCMIZ_0:def 25
 for a being adjective of T holds
( (types a) \/ (types (non- a)) is_<=_than sub a & ( types a <> {} & types (non- a) <> {} implies sub a = sup ((types a) \/ (types (non- a))) ) );
end;

:: deftheorem  defines non-absorbing ABCMIZ_0:def_24_:_
 for T being non empty non void TAS-structure holds
( T is non-absorbing iff the sub-map of T * the non-op of T = the sub-map of T );

:: deftheorem  defines subjected ABCMIZ_0:def_25_:_
 for T being non empty non void TAS-structure holds
( T is subjected iff for a being adjective of T holds
( (types a) \/ (types (non- a)) is_<=_than sub a & ( types a <> {} & types (non- a) <> {} implies sub a = sup ((types a) \/ (types (non- a))) ) ) );

definition
let T be non empty non void TAS-structure ;
redefine attr T is non-absorbing  means :: ABCMIZ_0:def 26
 for a being adjective of T holds sub (non- a) = sub a;
compatibility
 ( T is non-absorbing iff for a being adjective of T holds sub (non- a) = sub a )
proof
thus  ( T is non-absorbing implies for a being adjective of T holds sub (non- a) = sub a ) ::_thesis: ( ( for a being adjective of T holds sub (non- a) = sub a ) implies T is non-absorbing )
proof
assume A1: the sub-map of T * the non-op of T = the sub-map of T ; :: according to ABCMIZ_0:def_24 ::_thesis: for a being adjective of T holds sub (non- a) = sub a
let a be adjective of T; ::_thesis: sub (non- a) = sub a
thus  sub (non- a) = sub a by A1, FUNCT_2:15; ::_thesis: verum
end;
assume A2: for a being adjective of T holds sub (non- a) = sub a ; ::_thesis: T is non-absorbing
now__::_thesis:_for_x_being_Element_of_the_adjectives_of_T_holds_(_the_sub-map_of_T_*_the_non-op_of_T)_._x_=_the_sub-map_of_T_._x
let x be Element of the adjectives of T; ::_thesis: ( the sub-map of T * the non-op of T) . x = the sub-map of T . x
reconsider a = x as adjective of T ;
thus ( the sub-map of T * the non-op of T) . x = sub (non- a) by FUNCT_2:15
.= sub a by A2
.= the sub-map of T . x ; ::_thesis: verum
end;
hence  the sub-map of T * the non-op of T = the sub-map of T by FUNCT_2:63; :: according to ABCMIZ_0:def_24 ::_thesis: verum
end;
end;

:: deftheorem  defines non-absorbing ABCMIZ_0:def_26_:_
 for T being non empty non void TAS-structure holds
( T is non-absorbing iff for a being adjective of T holds sub (non- a) = sub a );

definition
let T be non empty non void TAS-structure ;
let t be Element of T;
let a be adjective of T;
preda is_properly_applicable_to t means :Def27: :: ABCMIZ_0:def 27
( t <= sub a & a is_applicable_to t );
end;

:: deftheorem Def27 defines is_properly_applicable_to ABCMIZ_0:def_27_:_
 for T being non empty non void TAS-structure
for t being Element of T
for a being adjective of T holds
( a is_properly_applicable_to t iff ( t <= sub a & a is_applicable_to t ) );

definition
let T be non empty reflexive transitive non void TAS-structure ;
let t be type of T;
let v be FinSequence of the adjectives of T;
predv is_properly_applicable_to t means :Def28: :: ABCMIZ_0:def 28
 for i being Nat
for a being adjective of T
for s being type of T st i in dom v & a = v . i & s = (apply (v,t)) . i holds
a is_properly_applicable_to s;
end;

:: deftheorem Def28 defines is_properly_applicable_to ABCMIZ_0:def_28_:_
 for T being non empty reflexive transitive non void TAS-structure
for t being type of T
for v being FinSequence of the adjectives of T holds
( v is_properly_applicable_to t iff for i being Nat
for a being adjective of T
for s being type of T st i in dom v & a = v . i & s = (apply (v,t)) . i holds
a is_properly_applicable_to s );

theorem Th57: :: ABCMIZ_0:57
for T being non empty reflexive transitive non void TAS-structure
for t being type of T
for v being FinSequence of the adjectives of T st v is_properly_applicable_to t holds
v is_applicable_to t
proof
let T be non empty reflexive transitive non void TAS-structure ; ::_thesis: for t being type of T
for v being FinSequence of the adjectives of T st v is_properly_applicable_to t holds
v is_applicable_to t
let t be type of T; ::_thesis: for v being FinSequence of the adjectives of T st v is_properly_applicable_to t holds
v is_applicable_to t
let v be FinSequence of the adjectives of T; ::_thesis: ( v is_properly_applicable_to t implies v is_applicable_to t )
assume A1: for i being Nat
for a being adjective of T
for s being type of T st i in dom v & a = v . i & s = (apply (v,t)) . i holds
a is_properly_applicable_to s ; :: according to ABCMIZ_0:def_28 ::_thesis: v is_applicable_to t
let i be Nat; :: according to ABCMIZ_0:def_21 ::_thesis: for a being adjective of T
for s being type of T st i in dom v & a = v . i & s = (apply (v,t)) . i holds
a is_applicable_to s
let a be adjective of T; ::_thesis: for s being type of T st i in dom v & a = v . i & s = (apply (v,t)) . i holds
a is_applicable_to s
let s be type of T; ::_thesis: ( i in dom v & a = v . i & s = (apply (v,t)) . i implies a is_applicable_to s )
assume that
A2: i in dom v and
A3: a = v . i and
A4: s = (apply (v,t)) . i ; ::_thesis: a is_applicable_to s
 a is_properly_applicable_to s by A1, A2, A3, A4;
hence  a is_applicable_to s by Def27; ::_thesis: verum
end;

theorem :: ABCMIZ_0:58
for T being non empty reflexive transitive non void TAS-structure
for t being type of T holds <*> the adjectives of T is_properly_applicable_to t
proof
let T be non empty reflexive transitive non void TAS-structure ; ::_thesis: for t being type of T holds <*> the adjectives of T is_properly_applicable_to t
let t be type of T; ::_thesis: <*> the adjectives of T is_properly_applicable_to t
let i be Nat; :: according to ABCMIZ_0:def_28 ::_thesis: for a being adjective of T
for s being type of T st i in dom (<*> the adjectives of T) & a = (<*> the adjectives of T) . i & s = (apply ((<*> the adjectives of T),t)) . i holds
a is_properly_applicable_to s
thus  for a being adjective of T
for s being type of T st i in dom (<*> the adjectives of T) & a = (<*> the adjectives of T) . i & s = (apply ((<*> the adjectives of T),t)) . i holds
a is_properly_applicable_to s ; ::_thesis: verum
end;

theorem :: ABCMIZ_0:59
for T being non empty reflexive transitive non void TAS-structure
for t being type of T
for a being adjective of T holds
( a is_properly_applicable_to t iff <*a*> is_properly_applicable_to t )
proof
let T be non empty reflexive transitive non void TAS-structure ; ::_thesis: for t being type of T
for a being adjective of T holds
( a is_properly_applicable_to t iff <*a*> is_properly_applicable_to t )
let t be type of T; ::_thesis: for a being adjective of T holds
( a is_properly_applicable_to t iff <*a*> is_properly_applicable_to t )
let a be adjective of T; ::_thesis: ( a is_properly_applicable_to t iff <*a*> is_properly_applicable_to t )
set v = <*a*>;
A1: <*a*> . 1 = a by FINSEQ_1:40;
hereby  ::_thesis: ( <*a*> is_properly_applicable_to t implies a is_properly_applicable_to t )
assume A2: a is_properly_applicable_to t ; ::_thesis: <*a*> is_properly_applicable_to t
thus  <*a*> is_properly_applicable_to t ::_thesis: verum
proof
let i be Nat; :: according to ABCMIZ_0:def_28 ::_thesis: for a being adjective of T
for s being type of T st i in dom <*a*> & a = <*a*> . i & s = (apply (<*a*>,t)) . i holds
a is_properly_applicable_to s
let b be adjective of T; ::_thesis: for s being type of T st i in dom <*a*> & b = <*a*> . i & s = (apply (<*a*>,t)) . i holds
b is_properly_applicable_to s
let s be type of T; ::_thesis: ( i in dom <*a*> & b = <*a*> . i & s = (apply (<*a*>,t)) . i implies b is_properly_applicable_to s )
assume  i in dom <*a*> ; ::_thesis: ( not b = <*a*> . i or not s = (apply (<*a*>,t)) . i or b is_properly_applicable_to s )
then  i in Seg 1 by FINSEQ_1:38;
then A3: i = 1 by FINSEQ_1:2, TARSKI:def_1;
then  <*a*> . i = a by FINSEQ_1:40;
hence  ( not b = <*a*> . i or not s = (apply (<*a*>,t)) . i or b is_properly_applicable_to s ) by A2, A3, Def19; ::_thesis: verum
end;
end;
assume A4: for i being Nat
for a9 being adjective of T
for s being type of T st i in dom <*a*> & a9 = <*a*> . i & s = (apply (<*a*>,t)) . i holds
a9 is_properly_applicable_to s ; :: according to ABCMIZ_0:def_28 ::_thesis: a is_properly_applicable_to t
 len <*a*> = 1 by FINSEQ_1:40;
then A5: 1 in dom <*a*> by FINSEQ_3:25;
 (apply (<*a*>,t)) . 1 = t by Def19;
hence  a is_properly_applicable_to t by A4, A5, A1; ::_thesis: verum
end;

theorem Th60: :: ABCMIZ_0:60
for T being non empty reflexive transitive non void TAS-structure
for t being type of T
for v1, v2 being FinSequence of the adjectives of T st v1 ^ v2 is_properly_applicable_to t holds
( v1 is_properly_applicable_to t & v2 is_properly_applicable_to v1 ast t )
proof
let T be non empty reflexive transitive non void TAS-structure ; ::_thesis: for t being type of T
for v1, v2 being FinSequence of the adjectives of T st v1 ^ v2 is_properly_applicable_to t holds
( v1 is_properly_applicable_to t & v2 is_properly_applicable_to v1 ast t )
let t be type of T; ::_thesis: for v1, v2 being FinSequence of the adjectives of T st v1 ^ v2 is_properly_applicable_to t holds
( v1 is_properly_applicable_to t & v2 is_properly_applicable_to v1 ast t )
let v1, v2 be FinSequence of the adjectives of T; ::_thesis: ( v1 ^ v2 is_properly_applicable_to t implies ( v1 is_properly_applicable_to t & v2 is_properly_applicable_to v1 ast t ) )
set v = v1 ^ v2;
A1: apply ((v1 ^ v2),t) = (apply (v1,t)) $^ (apply (v2,(v1 ast t))) by Th34;
A2: len (apply (v2,(v1 ast t))) = (len v2) + 1 by Def19;
assume A3: for i being Nat
for a being adjective of T
for s being type of T st i in dom (v1 ^ v2) & a = (v1 ^ v2) . i & s = (apply ((v1 ^ v2),t)) . i holds
a is_properly_applicable_to s ; :: according to ABCMIZ_0:def_28 ::_thesis: ( v1 is_properly_applicable_to t & v2 is_properly_applicable_to v1 ast t )
hereby  :: according to ABCMIZ_0:def_28 ::_thesis: v2 is_properly_applicable_to v1 ast t
A4: dom v1 c= dom (v1 ^ v2) by FINSEQ_1:26;
let i be Nat; ::_thesis: for a being adjective of T
for s being type of T st i in dom v1 & a = v1 . i & s = (apply (v1,t)) . i holds
a is_properly_applicable_to s
let a be adjective of T; ::_thesis: for s being type of T st i in dom v1 & a = v1 . i & s = (apply (v1,t)) . i holds
a is_properly_applicable_to s
let s be type of T; ::_thesis: ( i in dom v1 & a = v1 . i & s = (apply (v1,t)) . i implies a is_properly_applicable_to s )
assume that
A5: i in dom v1 and
A6: a = v1 . i and
A7: s = (apply (v1,t)) . i ; ::_thesis: a is_properly_applicable_to s
A8: a = (v1 ^ v2) . i by A5, A6, FINSEQ_1:def_7;
 s = (apply ((v1 ^ v2),t)) . i by A5, A7, Th35;
hence  a is_properly_applicable_to s by A3, A5, A4, A8; ::_thesis: verum
end;
let i be Nat; :: according to ABCMIZ_0:def_28 ::_thesis: for a being adjective of T
for s being type of T st i in dom v2 & a = v2 . i & s = (apply (v2,(v1 ast t))) . i holds
a is_properly_applicable_to s
let a be adjective of T; ::_thesis: for s being type of T st i in dom v2 & a = v2 . i & s = (apply (v2,(v1 ast t))) . i holds
a is_properly_applicable_to s
let s be type of T; ::_thesis: ( i in dom v2 & a = v2 . i & s = (apply (v2,(v1 ast t))) . i implies a is_properly_applicable_to s )
assume that
A9: i in dom v2 and
A10: a = v2 . i and
A11: s = (apply (v2,(v1 ast t))) . i ; ::_thesis: a is_properly_applicable_to s
A12: a = (v1 ^ v2) . ((len v1) + i) by A9, A10, FINSEQ_1:def_7;
 i >= 1 by A9, FINSEQ_3:25;
then consider j being Nat such that
A13: i = 1 + j by NAT_1:10;
 i <= len v2 by A9, FINSEQ_3:25;
then  j < len v2 by A13, NAT_1:13;
then A14: j < len (apply (v2,(v1 ast t))) by A2, NAT_1:13;
 len (apply (v1,t)) = (len v1) + 1 by Def19;
then  (len v1) + i = (len (apply (v1,t))) + j by A13;
then  s = (apply ((v1 ^ v2),t)) . ((len v1) + i) by A11, A1, A13, A14, Th33;
hence  a is_properly_applicable_to s by A3, A9, A12, FINSEQ_1:28; ::_thesis: verum
end;

theorem Th61: :: ABCMIZ_0:61
for T being non empty reflexive transitive non void TAS-structure
for t being type of T
for v1, v2 being FinSequence of the adjectives of T st v1 is_properly_applicable_to t & v2 is_properly_applicable_to v1 ast t holds
v1 ^ v2 is_properly_applicable_to t
proof
let T be non empty reflexive transitive non void TAS-structure ; ::_thesis: for t being type of T
for v1, v2 being FinSequence of the adjectives of T st v1 is_properly_applicable_to t & v2 is_properly_applicable_to v1 ast t holds
v1 ^ v2 is_properly_applicable_to t
let t be type of T; ::_thesis: for v1, v2 being FinSequence of the adjectives of T st v1 is_properly_applicable_to t & v2 is_properly_applicable_to v1 ast t holds
v1 ^ v2 is_properly_applicable_to t
let v1, v2 be FinSequence of the adjectives of T; ::_thesis: ( v1 is_properly_applicable_to t & v2 is_properly_applicable_to v1 ast t implies v1 ^ v2 is_properly_applicable_to t )
set v = v1 ^ v2;
assume A1: for i being Nat
for a being adjective of T
for s being type of T st i in dom v1 & a = v1 . i & s = (apply (v1,t)) . i holds
a is_properly_applicable_to s ; :: according to ABCMIZ_0:def_28 ::_thesis: ( not v2 is_properly_applicable_to v1 ast t or v1 ^ v2 is_properly_applicable_to t )
assume A2: for i being Nat
for a being adjective of T
for s being type of T st i in dom v2 & a = v2 . i & s = (apply (v2,(v1 ast t))) . i holds
a is_properly_applicable_to s ; :: according to ABCMIZ_0:def_28 ::_thesis: v1 ^ v2 is_properly_applicable_to t
A3: apply ((v1 ^ v2),t) = (apply (v1,t)) $^ (apply (v2,(v1 ast t))) by Th34;
let i be Nat; :: according to ABCMIZ_0:def_28 ::_thesis: for a being adjective of T
for s being type of T st i in dom (v1 ^ v2) & a = (v1 ^ v2) . i & s = (apply ((v1 ^ v2),t)) . i holds
a is_properly_applicable_to s
let a be adjective of T; ::_thesis: for s being type of T st i in dom (v1 ^ v2) & a = (v1 ^ v2) . i & s = (apply ((v1 ^ v2),t)) . i holds
a is_properly_applicable_to s
let s be type of T; ::_thesis: ( i in dom (v1 ^ v2) & a = (v1 ^ v2) . i & s = (apply ((v1 ^ v2),t)) . i implies a is_properly_applicable_to s )
assume that
A4: i in dom (v1 ^ v2) and
A5: a = (v1 ^ v2) . i and
A6: s = (apply ((v1 ^ v2),t)) . i ; ::_thesis: a is_properly_applicable_to s
A7: i >= 1 by A4, FINSEQ_3:25;
A8: i <= len (v1 ^ v2) by A4, FINSEQ_3:25;
percases ( i <= len v1 or i > len v1 ) ;
suppose i <= len v1 ; ::_thesis: a is_properly_applicable_to s
then A9: i in dom v1 by A7, FINSEQ_3:25;
then A10: a = v1 . i by A5, FINSEQ_1:def_7;
 s = (apply (v1,t)) . i by A6, A9, Th35;
hence  a is_properly_applicable_to s by A1, A9, A10; ::_thesis: verum
end;
suppose i > len v1 ; ::_thesis: a is_properly_applicable_to s
then  i >= 1 + (len v1) by NAT_1:13;
then consider j being Nat such that
A11: i = ((len v1) + 1) + j by NAT_1:10;
A12: len (apply (v2,(v1 ast t))) = (len v2) + 1 by Def19;
A13: len (v1 ^ v2) = (len v1) + (len v2) by FINSEQ_1:22;
A14: len (apply (v1,t)) = (len v1) + 1 by Def19;
 i = (len v1) + (j + 1) by A11;
then A15: j + 1 <= len v2 by A8, A13, XREAL_1:6;
then  j < len v2 by NAT_1:13;
then  j < len (apply (v2,(v1 ast t))) by A12, NAT_1:13;
then A16: s = (apply (v2,(v1 ast t))) . (1 + j) by A6, A3, A11, A14, Th33;
 j + 1 >= 1 by NAT_1:11;
then A17: j + 1 in dom v2 by A15, FINSEQ_3:25;
 (len v1) + (j + 1) = (len (apply (v1,t))) + j by A14;
then  a = v2 . (1 + j) by A5, A11, A17, FINSEQ_1:def_7;
hence  a is_properly_applicable_to s by A2, A17, A16; ::_thesis: verum
end;
end;
end;

definition
let T be non empty reflexive transitive non void TAS-structure ;
let t be type of T;
let A be Subset of the adjectives of T;
predA is_properly_applicable_to t means :Def29: :: ABCMIZ_0:def 29
 ex s being FinSequence of the adjectives of T st
( rng s = A & s is_properly_applicable_to t );
end;

:: deftheorem Def29 defines is_properly_applicable_to ABCMIZ_0:def_29_:_
 for T being non empty reflexive transitive non void TAS-structure
for t being type of T
for A being Subset of the adjectives of T holds
( A is_properly_applicable_to t iff ex s being FinSequence of the adjectives of T st
( rng s = A & s is_properly_applicable_to t ) );

theorem Th62: :: ABCMIZ_0:62
for T being non empty reflexive transitive non void TAS-structure
for t being type of T
for A being Subset of the adjectives of T st A is_properly_applicable_to t holds
A is finite
proof
let T be non empty reflexive transitive non void TAS-structure ; ::_thesis: for t being type of T
for A being Subset of the adjectives of T st A is_properly_applicable_to t holds
A is finite
let t be type of T; ::_thesis: for A being Subset of the adjectives of T st A is_properly_applicable_to t holds
A is finite
let A be Subset of the adjectives of T; ::_thesis: ( A is_properly_applicable_to t implies A is finite )
assume  ex s being FinSequence of the adjectives of T st
( rng s = A & s is_properly_applicable_to t ) ; :: according to ABCMIZ_0:def_29 ::_thesis: A is finite
hence  A is finite ; ::_thesis: verum
end;

theorem Th63: :: ABCMIZ_0:63
for T being non empty reflexive transitive non void TAS-structure
for t being type of T holds {} the adjectives of T is_properly_applicable_to t
proof
let T be non empty reflexive transitive non void TAS-structure ; ::_thesis: for t being type of T holds {} the adjectives of T is_properly_applicable_to t
let t be type of T; ::_thesis: {} the adjectives of T is_properly_applicable_to t
take s = <*> the adjectives of T; :: according to ABCMIZ_0:def_29 ::_thesis: ( rng s = {} the adjectives of T & s is_properly_applicable_to t )
thus  rng s = {} the adjectives of T ; ::_thesis: s is_properly_applicable_to t
let i be Nat; :: according to ABCMIZ_0:def_28 ::_thesis: for a being adjective of T
for s being type of T st i in dom s & a = s . i & s = (apply (s,t)) . i holds
a is_properly_applicable_to s
thus  for a being adjective of T
for s being type of T st i in dom s & a = s . i & s = (apply (s,t)) . i holds
a is_properly_applicable_to s ; ::_thesis: verum
end;

scheme :: ABCMIZ_0:sch 1
MinimalFiniteSet{ P1[ set ] } :
 ex A being finite set st
( P1[A] & ( for B being set st B c= A & P1[B] holds
B = A ) )
provided
A1: ex A being finite set st P1[A]
proof
consider A being finite set  such that
A2: P1[A] by A1;
defpred S1[ set , set ] means $1 c= $2;
consider Y being set  such that
A3: for x being set holds
( x in Y iff ( x in bool A & P1[x] ) ) from XBOOLE_0:sch_1();
 A c= A ;
then reconsider Y = Y as non empty set by A2, A3;
 Y c= bool A
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in Y or x in bool A )
thus  ( not x in Y or x in bool A ) by A3; ::_thesis: verum
end;
then reconsider Y = Y as non empty finite set ;
A4: for x, y being Element of Y st S1[x,y] & S1[y,x] holds
x = y by XBOOLE_0:def_10;
A5: for x, y, z being Element of Y st S1[x,y] & S1[y,z] holds
S1[x,z] by XBOOLE_1:1;
A6: for X being set st X c= Y & ( for x, y being Element of Y st x in X & y in X & not S1[x,y] holds
S1[y,x] ) holds
ex y being Element of Y st
for x being Element of Y st x in X holds
S1[y,x]
proof
let X be set ; ::_thesis: ( X c= Y & ( for x, y being Element of Y st x in X & y in X & not S1[x,y] holds
S1[y,x] ) implies ex y being Element of Y st
for x being Element of Y st x in X holds
S1[y,x] )
assume that
A7: X c= Y and
A8: for x, y being Element of Y st x in X & y in X & not S1[x,y] holds
S1[y,x] ; ::_thesis: ex y being Element of Y st
for x being Element of Y st x in X holds
S1[y,x]
percases ( X = {} or X <> {} ) ;
supposeA9: X = {} ; ::_thesis: ex y being Element of Y st
for x being Element of Y st x in X holds
S1[y,x]
set y = the Element of Y;
take  the Element of Y ; ::_thesis: for x being Element of Y st x in X holds
S1[ the Element of Y,x]
thus  for x being Element of Y st x in X holds
S1[ the Element of Y,x] by A9; ::_thesis: verum
end;
supposeA10: X <> {} ; ::_thesis: ex y being Element of Y st
for x being Element of Y st x in X holds
S1[y,x]
set x0 = the Element of X;
 the Element of X in X by A10;
then reconsider x0 = the Element of X as Element of Y by A7;
deffunc H1( set ) ->  set = card  {  y where y is Element of Y : ( y in X & y c< $1 )  }  ;
consider f being Function such that
A11: ( dom f = X & ( for x being set st x in X holds
f . x = H1(x) ) ) from FUNCT_1:sch_3();
defpred S2[ Nat] means  ex x being Element of Y st
( x in X & $1 = f . x );
A12: for k being Nat st k <> 0 & S2[k] holds
ex n being Nat st
( n < k & S2[n] )
proof
let k be Nat; ::_thesis: ( k <> 0 & S2[k] implies ex n being Nat st
( n < k & S2[n] ) )
assume A13: k <> 0 ; ::_thesis: ( not S2[k] or ex n being Nat st
( n < k & S2[n] ) )
given x being Element of Y such that A14: x in X and
A15: k = f . x ; ::_thesis: ex n being Nat st
( n < k & S2[n] )
set fx =  {  a where a is Element of Y : ( a in X & a c< x )  }  ;
  {  a where a is Element of Y : ( a in X & a c< x )  }  c= Y
proof
let a be set ; :: according to TARSKI:def_3 ::_thesis: ( not a in  {  a where a is Element of Y : ( a in X & a c< x )  }  or a in Y )
assume  a in  {  a where a is Element of Y : ( a in X & a c< x )  }  ; ::_thesis: a in Y
then  ex z being Element of Y st
( a = z & z in X & z c< x ) ;
hence  a in Y ; ::_thesis: verum
end;
then reconsider fx =  {  a where a is Element of Y : ( a in X & a c< x )  }  as finite set ;
A16: k = card fx by A11, A14, A15;
set A =  {  z where z is Element of Y : ( z in X & z c< x )  }  ;
reconsider A =  {  z where z is Element of Y : ( z in X & z c< x )  }  as non empty set by A11, A13, A14, A15, CARD_1:27;
set z = the Element of A;
 the Element of A in A ;
then consider y being Element of Y such that
A17: the Element of A = y and
A18: y in X and
A19: y c< x ;
set fx0 =  {  a where a is Element of Y : ( a in X & a c< y )  }  ;
  {  a where a is Element of Y : ( a in X & a c< y )  }  c= Y
proof
let a be set ; :: according to TARSKI:def_3 ::_thesis: ( not a in  {  a where a is Element of Y : ( a in X & a c< y )  }  or a in Y )
assume  a in  {  a where a is Element of Y : ( a in X & a c< y )  }  ; ::_thesis: a in Y
then  ex z being Element of Y st
( a = z & z in X & z c< y ) ;
hence  a in Y ; ::_thesis: verum
end;
then reconsider fx0 =  {  a where a is Element of Y : ( a in X & a c< y )  }  as finite set ;
reconsider n = card fx0 as Element of NAT ;
take  n ; ::_thesis: ( n < k & S2[n] )
 for a being Element of Y holds
( not y = a or not a in X or not a c< y ) ;
then A20: not y in fx0 ;
A21: y in fx by A17;
A22: fx0 c= fx
proof
let a be set ; :: according to TARSKI:def_3 ::_thesis: ( not a in fx0 or a in fx )
assume  a in fx0 ; ::_thesis: a in fx
then consider b being Element of Y such that
A23: a = b and
A24: b in X and
A25: b c< y ;
 b c< x by A19, A25, XBOOLE_1:56;
hence  a in fx by A23, A24; ::_thesis: verum
end;
then  card fx0 c= card fx by CARD_1:11;
then  n <= k by A16, NAT_1:39;
hence  n < k by A16, A22, A21, A20, PRE_POLY:8, XXREAL_0:1; ::_thesis: S2[n]
take  y ; ::_thesis: ( y in X & n = f . y )
thus  ( y in X & n = f . y ) by A11, A18; ::_thesis: verum
end;
set fx0 =  {  y where y is Element of Y : ( y in X & y c< x0 )  }  ;
  {  y where y is Element of Y : ( y in X & y c< x0 )  }  c= Y
proof
let a be set ; :: according to TARSKI:def_3 ::_thesis: ( not a in  {  y where y is Element of Y : ( y in X & y c< x0 )  }  or a in Y )
assume  a in  {  y where y is Element of Y : ( y in X & y c< x0 )  }  ; ::_thesis: a in Y
then  ex y being Element of Y st
( a = y & y in X & y c< x0 ) ;
hence  a in Y ; ::_thesis: verum
end;
then reconsider fx0 =  {  y where y is Element of Y : ( y in X & y c< x0 )  }  as finite set ;
 f . x0 = card fx0 by A10, A11;
then A26: ex n being Nat st S2[n] by A10;
 S2[ 0 ] from NAT_1:sch_7(A26, A12);
then consider y being Element of Y such that
A27: y in X and
A28: 0 = f . y ;
take  y ; ::_thesis: for x being Element of Y st x in X holds
S1[y,x]
let x be Element of Y; ::_thesis: ( x in X implies S1[y,x] )
assume A29: x in X ; ::_thesis: S1[y,x]
then  ( x c= y or y c= x ) by A8, A27;
then  ( x c< y or y c= x ) by XBOOLE_0:def_8;
then A30: ( x in  {  z where z is Element of Y : ( z in X & z c< y )  }  or y c= x ) by A29;
 f . y = card  {  z where z is Element of Y : ( z in X & z c< y )  }  by A11, A27;
hence  S1[y,x] by A28, A30; ::_thesis: verum
end;
end;
end;
A31: for x being Element of Y holds S1[x,x] ;
consider x being Element of Y such that
A32: for y being Element of Y st x <> y holds
not S1[y,x] from ORDERS_1:sch_2(A31, A4, A5, A6);
 x in bool A by A3;
then reconsider x = x as finite set ;
take  x ; ::_thesis: ( P1[x] & ( for B being set st B c= x & P1[B] holds
B = x ) )
thus  P1[x] by A3; ::_thesis: for B being set st B c= x & P1[B] holds
B = x
let B be set ; ::_thesis: ( B c= x & P1[B] implies B = x )
assume that
A33: B c= x and
A34: P1[B] ; ::_thesis: B = x
 x in bool A by A3;
then  B c= A by A33, XBOOLE_1:1;
then  B in Y by A3, A34;
hence  B = x by A32, A33; ::_thesis: verum
end;

theorem Th64: :: ABCMIZ_0:64
for T being non empty reflexive transitive non void TAS-structure
for t being type of T
for A being Subset of the adjectives of T st A is_properly_applicable_to t holds
ex B being Subset of the adjectives of T st
( B c= A & B is_properly_applicable_to t & A ast t = B ast t & ( for C being Subset of the adjectives of T st C c= B & C is_properly_applicable_to t & A ast t = C ast t holds
C = B ) )
proof
let T be non empty reflexive transitive non void TAS-structure ; ::_thesis: for t being type of T
for A being Subset of the adjectives of T st A is_properly_applicable_to t holds
ex B being Subset of the adjectives of T st
( B c= A & B is_properly_applicable_to t & A ast t = B ast t & ( for C being Subset of the adjectives of T st C c= B & C is_properly_applicable_to t & A ast t = C ast t holds
C = B ) )
let t be type of T; ::_thesis: for A being Subset of the adjectives of T st A is_properly_applicable_to t holds
ex B being Subset of the adjectives of T st
( B c= A & B is_properly_applicable_to t & A ast t = B ast t & ( for C being Subset of the adjectives of T st C c= B & C is_properly_applicable_to t & A ast t = C ast t holds
C = B ) )
let A be Subset of the adjectives of T; ::_thesis: ( A is_properly_applicable_to t implies ex B being Subset of the adjectives of T st
( B c= A & B is_properly_applicable_to t & A ast t = B ast t & ( for C being Subset of the adjectives of T st C c= B & C is_properly_applicable_to t & A ast t = C ast t holds
C = B ) ) )
defpred S1[ set ] means  ex B being Subset of the adjectives of T st
( $1 = B & $1 c= A & B is_properly_applicable_to t & A ast t = B ast t );
assume A1: A is_properly_applicable_to t ; ::_thesis: ex B being Subset of the adjectives of T st
( B c= A & B is_properly_applicable_to t & A ast t = B ast t & ( for C being Subset of the adjectives of T st C c= B & C is_properly_applicable_to t & A ast t = C ast t holds
C = B ) )
then  A is finite by Th62;
then A2: ex a being finite set st S1[a] by A1;
consider B being finite set  such that
A3: S1[B] and
A4: for C being set st C c= B & S1[C] holds
C = B from ABCMIZ_0:sch_1(A2);
reconsider B = B as Subset of the adjectives of T by A3;
take  B ; ::_thesis: ( B c= A & B is_properly_applicable_to t & A ast t = B ast t & ( for C being Subset of the adjectives of T st C c= B & C is_properly_applicable_to t & A ast t = C ast t holds
C = B ) )
thus  ( B c= A & B is_properly_applicable_to t & A ast t = B ast t ) by A3; ::_thesis: for C being Subset of the adjectives of T st C c= B & C is_properly_applicable_to t & A ast t = C ast t holds
C = B
let C be Subset of the adjectives of T; ::_thesis: ( C c= B & C is_properly_applicable_to t & A ast t = C ast t implies C = B )
assume A5: C c= B ; ::_thesis: ( not C is_properly_applicable_to t or not A ast t = C ast t or C = B )
then  C c= A by A3, XBOOLE_1:1;
hence  ( not C is_properly_applicable_to t or not A ast t = C ast t or C = B ) by A4, A5; ::_thesis: verum
end;

definition
let T be non empty reflexive transitive non void TAS-structure ;
attrT is commutative  means :Def30: :: ABCMIZ_0:def 30
 for t1, t2 being type of T
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 );
end;

:: deftheorem Def30 defines commutative ABCMIZ_0:def_30_:_
 for T being non empty reflexive transitive non void TAS-structure holds
( T is commutative iff for t1, t2 being type of T
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 ) );

registration
cluster non empty trivial finite 1 -element reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded V139() connected up-complete /\-complete Noetherian Mizar-widening-like non void involutive without_fixpoints consistent adj-structured adjs-typed strict non-absorbing subjected commutative for TAS-structure ;
existence
 ex b1 being 1 -element reflexive transitive antisymmetric complete upper-bounded non void strict TAS-structure st
( b1 is Mizar-widening-like & b1 is involutive & b1 is without_fixpoints & b1 is consistent & b1 is adj-structured & b1 is adjs-typed & b1 is non-absorbing & b1 is subjected & b1 is commutative )
proof
set P = the 1 -element 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 the 1 -element reflexive complete Mizar-widening-like non void involutive without_fixpoints strict consistent adj-structured adjs-typed TA-structure , the adjectives of the 1 -element reflexive complete Mizar-widening-like non void involutive without_fixpoints strict consistent adj-structured adjs-typed TA-structure , the InternalRel of the 1 -element reflexive complete Mizar-widening-like non void involutive without_fixpoints strict consistent adj-structured adjs-typed TA-structure , the non-op of the 1 -element reflexive complete Mizar-widening-like non void involutive without_fixpoints strict consistent adj-structured adjs-typed TA-structure , the adj-map of the 1 -element reflexive complete Mizar-widening-like non void involutive without_fixpoints strict consistent adj-structured adjs-typed TA-structure ,(sub the 1 -element reflexive complete Mizar-widening-like non void involutive without_fixpoints strict consistent adj-structured adjs-typed TA-structure ) #);
 the carrier of the 1 -element reflexive complete Mizar-widening-like non void involutive without_fixpoints strict consistent adj-structured adjs-typed TA-structure is 1 -element ;
 RelStr(# the carrier of the 1 -element reflexive complete Mizar-widening-like non void involutive without_fixpoints strict consistent adj-structured adjs-typed TA-structure , the InternalRel of the 1 -element reflexive complete Mizar-widening-like non void involutive without_fixpoints strict consistent adj-structured adjs-typed TA-structure #) = RelStr(# the carrier of TAS-structure(# the carrier of the 1 -element reflexive complete Mizar-widening-like non void involutive without_fixpoints strict consistent adj-structured adjs-typed TA-structure , the adjectives of the 1 -element reflexive complete Mizar-widening-like non void involutive without_fixpoints strict consistent adj-structured adjs-typed TA-structure , the InternalRel of the 1 -element reflexive complete Mizar-widening-like non void involutive without_fixpoints strict consistent adj-structured adjs-typed TA-structure , the non-op of the 1 -element reflexive complete Mizar-widening-like non void involutive without_fixpoints strict consistent adj-structured adjs-typed TA-structure , the adj-map of the 1 -element reflexive complete Mizar-widening-like non void involutive without_fixpoints strict consistent adj-structured adjs-typed TA-structure ,(sub the 1 -element reflexive complete Mizar-widening-like non void involutive without_fixpoints strict consistent adj-structured adjs-typed TA-structure ) #), the InternalRel of TAS-structure(# the carrier of the 1 -element reflexive complete Mizar-widening-like non void involutive without_fixpoints strict consistent adj-structured adjs-typed TA-structure , the adjectives of the 1 -element reflexive complete Mizar-widening-like non void involutive without_fixpoints strict consistent adj-structured adjs-typed TA-structure , the InternalRel of the 1 -element reflexive complete Mizar-widening-like non void involutive without_fixpoints strict consistent adj-structured adjs-typed TA-structure , the non-op of the 1 -element reflexive complete Mizar-widening-like non void involutive without_fixpoints strict consistent adj-structured adjs-typed TA-structure , the adj-map of the 1 -element reflexive complete Mizar-widening-like non void involutive without_fixpoints strict consistent adj-structured adjs-typed TA-structure ,(sub the 1 -element reflexive complete Mizar-widening-like non void involutive without_fixpoints strict consistent adj-structured adjs-typed TA-structure ) #) #) ;
then reconsider T = TAS-structure(# the carrier of the 1 -element reflexive complete Mizar-widening-like non void involutive without_fixpoints strict consistent adj-structured adjs-typed TA-structure , the adjectives of the 1 -element reflexive complete Mizar-widening-like non void involutive without_fixpoints strict consistent adj-structured adjs-typed TA-structure , the InternalRel of the 1 -element reflexive complete Mizar-widening-like non void involutive without_fixpoints strict consistent adj-structured adjs-typed TA-structure , the non-op of the 1 -element reflexive complete Mizar-widening-like non void involutive without_fixpoints strict consistent adj-structured adjs-typed TA-structure , the adj-map of the 1 -element reflexive complete Mizar-widening-like non void involutive without_fixpoints strict consistent adj-structured adjs-typed TA-structure ,(sub the 1 -element reflexive complete Mizar-widening-like non void involutive without_fixpoints strict consistent adj-structured adjs-typed TA-structure ) #) as 1 -element reflexive non void strict TAS-structure by Def4, STRUCT_0:def_19, 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 the 1 -element reflexive complete Mizar-widening-like non void involutive without_fixpoints strict consistent adj-structured adjs-typed TA-structure , the non-op of the 1 -element reflexive complete Mizar-widening-like non void involutive without_fixpoints strict consistent adj-structured adjs-typed TA-structure #) = 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 )
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 the 1 -element reflexive complete Mizar-widening-like non void involutive without_fixpoints strict consistent adj-structured adjs-typed TA-structure ;
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;
A1: RelStr(# the carrier of the 1 -element reflexive complete Mizar-widening-like non void involutive without_fixpoints strict consistent adj-structured adjs-typed TA-structure , the InternalRel of the 1 -element reflexive complete Mizar-widening-like non void involutive without_fixpoints strict consistent adj-structured adjs-typed TA-structure #) = RelStr(# the carrier of T, the InternalRel of T #) ;
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 the 1 -element reflexive complete Mizar-widening-like non void involutive without_fixpoints strict consistent adj-structured adjs-typed TA-structure ;
A2: types (non- a) = types (non- b) by Th11;
 types a = types b by Th11;
then  sup ((types a) \/ (types (non- a))) = sup ((types b) \/ (types (non- b))) by A1, A2, 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 that
 a is_properly_applicable_to t1 and
 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 Th63; ::_thesis: A ast (t1 "\/" t2) = t2
thus  A ast (t1 "\/" t2) = t2 by STRUCT_0:def_10; ::_thesis: verum
end;
end;

theorem Th65: :: ABCMIZ_0:65
for T being reflexive transitive antisymmetric with_suprema Noetherian non void adj-structured TAS-structure
for t being type of T
for A being Subset of the adjectives of T st A is_properly_applicable_to t holds
ex s being one-to-one FinSequence of the adjectives of T st
( rng s = A & s is_properly_applicable_to t )
proof
let T be reflexive transitive antisymmetric with_suprema Noetherian non void adj-structured TAS-structure ; ::_thesis: for t being type of T
for A being Subset of the adjectives of T st A is_properly_applicable_to t holds
ex s being one-to-one FinSequence of the adjectives of T st
( rng s = A & s is_properly_applicable_to t )
let t be type of T; ::_thesis: for A being Subset of the adjectives of T st A is_properly_applicable_to t holds
ex s being one-to-one FinSequence of the adjectives of T st
( rng s = A & s is_properly_applicable_to t )
let A be Subset of the adjectives of T; ::_thesis: ( A is_properly_applicable_to t implies ex s being one-to-one FinSequence of the adjectives of T st
( rng s = A & s is_properly_applicable_to t ) )
given s9 being FinSequence of the adjectives of T such that A1: rng s9 = A and
A2: s9 is_properly_applicable_to t ; :: according to ABCMIZ_0:def_29 ::_thesis: ex s being one-to-one FinSequence of the adjectives of T st
( rng s = A & s is_properly_applicable_to t )
defpred S1[ Nat] means  ex s being FinSequence of the adjectives of T st
( $1 = len s & rng s = A & s is_properly_applicable_to t );
 len s9 = len s9 ;
then A3: ex k being Nat st S1[k] by A1, A2;
consider k being Nat such that
A4: S1[k] and
A5: for n being Nat st S1[n] holds
k <= n from NAT_1:sch_5(A3);
consider s being FinSequence of the adjectives of T such that
A6: k = len s and
A7: rng s = A and
A8: s is_properly_applicable_to t by A4;
 s is one-to-one
proof
let x, y be set ; :: according to FUNCT_1:def_4 ::_thesis: ( not x in dom s or not y in dom s or not s . x = s . y or x = y )
assume that
A9: x in dom s and
A10: y in dom s and
A11: s . x = s . y and
A12: x <> y ; ::_thesis: contradiction
reconsider x = x, y = y as Element of NAT by A9, A10;
 ( x < y or x > y ) by A12, XXREAL_0:1;
then consider x, y being Element of NAT  such that
A13: x in dom s and
A14: y in dom s and
A15: x < y and
A16: s . x = s . y by A9, A10, A11;
A17: x >= 1 by A13, FINSEQ_3:25;
 y >= 1 by A14, FINSEQ_3:25;
then consider i being Nat such that
A18: y = 1 + i by NAT_1:10;
reconsider i = i as Element of NAT by ORDINAL1:def_12;
reconsider s1 = s | (Seg i) as FinSequence of the adjectives of T by FINSEQ_1:18;
A19: y <= len s by A14, FINSEQ_3:25;
then  i <= len s by A18, NAT_1:13;
then A20: len s1 = i by FINSEQ_1:17;
 x <= i by A15, A18, NAT_1:13;
then A21: x in dom s1 by A20, A17, FINSEQ_3:25;
 s1 c= s by TREES_1:def_1;
then consider s2 being FinSequence such that
A22: s = s1 ^ s2 by TREES_1:1;
reconsider s2 = s2 as FinSequence of the adjectives of T by A22, FINSEQ_1:36;
A23: len s = (len s1) + (len s2) by A22, FINSEQ_1:22;
then A24: len s2 >= 1 by A18, A19, A20, XREAL_1:6;
then A25: 1 in dom s2 by FINSEQ_3:25;
reconsider s21 = s2 | (Seg 1) as FinSequence of the adjectives of T by FINSEQ_1:18;
 s21 c= s2 by TREES_1:def_1;
then consider s22 being FinSequence such that
A26: s2 = s21 ^ s22 by TREES_1:1;
reconsider s22 = s22 as FinSequence of the adjectives of T by A26, FINSEQ_1:36;
A27: len s21 = 1 by A24, FINSEQ_1:17;
then A28: s21 = <*(s21 . 1)*> by FINSEQ_1:40;
then A29: rng s21 = {(s21 . 1)} by FINSEQ_1:39;
then reconsider a = s21 . 1 as adjective of T by ZFMISC_1:31;
A30: rng s2 = (rng s21) \/ (rng s22) by A26, FINSEQ_1:31;
a = s2 . 1 by A28, A26, FINSEQ_1:41
.= s . y by A18, A22, A20, A25, FINSEQ_1:def_7 ;
then  a = s1 . x by A16, A22, A21, FINSEQ_1:def_7;
then A31: a in rng s1 by A21, FUNCT_1:3;
then  rng s21 c= rng s1 by A29, ZFMISC_1:31;
then  (rng s1) \/ (rng s21) = rng s1 by XBOOLE_1:12;
then A32: rng (s1 ^ s22) = ((rng s1) \/ (rng s21)) \/ (rng s22) by FINSEQ_1:31;
A33: s2 is_properly_applicable_to s1 ast t by A8, A22, Th60;
A34: s1 is_properly_applicable_to t by A8, A22, A23, Th60;
then  rng s1 c= adjs (s1 ast t) by Th44, Th57;
then s1 ast t = a ast (s1 ast t) by A31, Th24
.= s21 ast (s1 ast t) by A28, Th31 ;
then  s22 is_properly_applicable_to s1 ast t by A26, A33, Th60;
then A35: s1 ^ s22 is_properly_applicable_to t by A34, Th61;
A36: len s2 = (len s21) + (len s22) by A26, FINSEQ_1:22;
 rng s = (rng s1) \/ (rng s2) by A22, FINSEQ_1:31;
then  k <= len (s1 ^ s22) by A5, A7, A35, A32, A30, XBOOLE_1:4;
then  k <= (len s1) + (len s22) by FINSEQ_1:22;
then  (len s21) + (len s22) <= 0 + (len s22) by A6, A23, A36, XREAL_1:6;
hence  contradiction by A27, XREAL_1:6; ::_thesis: verum
end;
hence  ex s being one-to-one FinSequence of the adjectives of T st
( rng s = A & s is_properly_applicable_to t ) by A7, A8; ::_thesis: verum
end;

begin

definition
let T be non empty reflexive transitive non void TAS-structure ;
funcT @-->  ->  Relation of T means :Def31: :: ABCMIZ_0:def 31
 for t1, t2 being type of T holds
( [t1,t2] in it iff ex a being adjective of T st
( not a in adjs t2 & a is_properly_applicable_to t2 & a ast t2 = t1 ) );
existence
 ex b1 being Relation of T st
for t1, t2 being type of T holds
( [t1,t2] in b1 iff ex a being adjective of T st
( not a in adjs t2 & a is_properly_applicable_to t2 & a ast t2 = t1 ) )
proof
defpred S1[ Element of T, Element of T] means  ex a being adjective of T st
( not a in adjs $2 & a is_properly_applicable_to $2 & a ast $2 = $1 );
consider R being Relation of the carrier of T such that
A1: for t1, t2 being Element of T holds
( [t1,t2] in R iff S1[t1,t2] ) from RELSET_1:sch_2();
reconsider R = R as Relation of T ;
take  R ; ::_thesis: for t1, t2 being type of T holds
( [t1,t2] in R iff ex a being adjective of T st
( not a in adjs t2 & a is_properly_applicable_to t2 & a ast t2 = t1 ) )
thus  for t1, t2 being type of T holds
( [t1,t2] in R iff ex a being adjective of T st
( not a in adjs t2 & a is_properly_applicable_to t2 & a ast t2 = t1 ) ) by A1; ::_thesis: verum
end;
uniqueness
 for b1, b2 being Relation of T st ( for t1, t2 being type of T holds
( [t1,t2] in b1 iff ex a being adjective of T st
( not a in adjs t2 & a is_properly_applicable_to t2 & a ast t2 = t1 ) ) ) & ( for t1, t2 being type of T holds
( [t1,t2] in b2 iff ex a being adjective of T st
( not a in adjs t2 & a is_properly_applicable_to t2 & a ast t2 = t1 ) ) ) holds
b1 = b2
proof
let R1, R2 be Relation of T; ::_thesis: ( ( for t1, t2 being type of T holds
( [t1,t2] in R1 iff ex a being adjective of T st
( not a in adjs t2 & a is_properly_applicable_to t2 & a ast t2 = t1 ) ) ) & ( for t1, t2 being type of T holds
( [t1,t2] in R2 iff ex a being adjective of T st
( not a in adjs t2 & a is_properly_applicable_to t2 & a ast t2 = t1 ) ) ) implies R1 = R2 )
assume that
A2: for t1, t2 being type of T holds
( [t1,t2] in R1 iff ex a being adjective of T st
( not a in adjs t2 & a is_properly_applicable_to t2 & a ast t2 = t1 ) ) and
A3: for t1, t2 being type of T holds
( [t1,t2] in R2 iff ex a being adjective of T st
( not a in adjs t2 & a is_properly_applicable_to t2 & a ast t2 = t1 ) ) ; ::_thesis: R1 = R2
let t1, t2 be Element of T; :: according to RELSET_1:def_2 ::_thesis: ( ( not [t1,t2] in R1 or [t1,t2] in R2 ) & ( not [t1,t2] in R2 or [t1,t2] in R1 ) )
 ( [t1,t2] in R1 iff ex a being adjective of T st
( not a in adjs t2 & a is_properly_applicable_to t2 & a ast t2 = t1 ) ) by A2;
hence  ( [t1,t2] in R1 iff [t1,t2] in R2 ) by A3; ::_thesis: verum
end;
end;

:: deftheorem Def31 defines @--> ABCMIZ_0:def_31_:_
 for T being non empty reflexive transitive non void TAS-structure
for b2 being Relation of T holds
( b2 = T @--> iff for t1, t2 being type of T holds
( [t1,t2] in b2 iff ex a being adjective of T st
( not a in adjs t2 & a is_properly_applicable_to t2 & a ast t2 = t1 ) ) );

theorem Th66: :: ABCMIZ_0:66
for T being reflexive transitive antisymmetric with_suprema Noetherian non void adj-structured TAS-structure holds T @--> c= the InternalRel of T
proof
let T be non empty reflexive transitive antisymmetric with_suprema Noetherian non void adj-structured TAS-structure ; ::_thesis: T @--> c= the InternalRel of T
let t1, t2 be Element of T; :: according to RELSET_1:def_1 ::_thesis: ( not [t1,t2] in T @--> or [t1,t2] in the InternalRel of T )
reconsider q1 = t1, q2 = t2 as type of T ;
assume  [t1,t2] in T @--> ; ::_thesis: [t1,t2] in the InternalRel of T
then consider a being adjective of T such that
 not a in adjs q2 and
A1: a is_properly_applicable_to q2 and
A2: a ast q2 = q1 by Def31;
 a is_applicable_to q2 by A1, Def27;
then  q1 <= q2 by A2, Th20;
hence  [t1,t2] in the InternalRel of T by ORDERS_2:def_5; ::_thesis: verum
end;

scheme :: ABCMIZ_0:sch 2
RedInd{ F1() ->  non empty set , P1[ set , set ], F2() ->  Relation of F1() } :
 for x, y being Element of F1() st F2() reduces x,y holds
P1[x,y]
provided
A1: for x, y being Element of F1() st [x,y] in F2() holds
P1[x,y] and
A2: for x being Element of F1() holds P1[x,x] and
A3: for x, y, z being Element of F1() st P1[x,y] & P1[y,z] holds
P1[x,z]
proof
let x, y be Element of F1(); ::_thesis: ( F2() reduces x,y implies P1[x,y] )
given p being RedSequence of F2() such that A4: p . 1 = x and
A5: p . (len p) = y ; :: according to REWRITE1:def_3 ::_thesis: P1[x,y]
defpred S1[ Element of NAT ] means ( 1 + $1 <= len p implies P1[x,p . (1 + $1)] );
A6: now__::_thesis:_for_i_being_Element_of_NAT_st_S1[i]_holds_
S1[i_+_1]
let i be Element of NAT ; ::_thesis: ( S1[i] implies S1[i + 1] )
assume A7: S1[i] ; ::_thesis: S1[i + 1]
now__::_thesis:_(_1_+_(i_+_1)_<=_len_p_implies_P1[x,p_._(1_+_(i_+_1))]_)
A8: i + 1 >= 1 by NAT_1:11;
assume A9: 1 + (i + 1) <= len p ; ::_thesis: P1[x,p . (1 + (i + 1))]
 1 + (i + 1) >= 1 by NAT_1:11;
then A10: 1 + (i + 1) in dom p by A9, FINSEQ_3:25;
 i + 1 < len p by A9, NAT_1:13;
then  i + 1 in dom p by A8, FINSEQ_3:25;
then A11: [(p . (i + 1)),(p . (1 + (i + 1)))] in F2() by A10, REWRITE1:def_2;
then A12: p . (1 + (i + 1)) in F1() by ZFMISC_1:87;
A13: p . (i + 1) in F1() by A11, ZFMISC_1:87;
then  P1[p . (i + 1),p . (1 + (i + 1))] by A1, A11, A12;
hence  P1[x,p . (1 + (i + 1))] by A3, A7, A9, A13, A12, NAT_1:13; ::_thesis: verum
end;
hence  S1[i + 1] ; ::_thesis: verum
end;
A14: S1[ 0 ] by A2, A4;
A15: for n being Element of NAT holds S1[n] from NAT_1:sch_1(A14, A6);
 len p >= 0 + 1 by NAT_1:13;
then consider n being Nat such that
A16: len p = 1 + n by NAT_1:10;
 n in NAT by ORDINAL1:def_12;
hence  P1[x,y] by A5, A16, A15; ::_thesis: verum
end;

theorem Th67: :: ABCMIZ_0:67
for T being reflexive transitive antisymmetric with_suprema Noetherian non void adj-structured TAS-structure
for t1, t2 being type of T st T @--> reduces t1,t2 holds
t1 <= t2
proof
let T be non empty reflexive transitive antisymmetric with_suprema Noetherian non void adj-structured TAS-structure ; ::_thesis: for t1, t2 being type of T st T @--> reduces t1,t2 holds
t1 <= t2
let t1, t2 be type of T; ::_thesis: ( T @--> reduces t1,t2 implies t1 <= t2 )
set R = T @--> ;
defpred S1[ Element of T, Element of T] means $1 <= $2;
A1: for x, y, z being Element of T st S1[x,y] & S1[y,z] holds
S1[x,z] by YELLOW_0:def_2;
A2: now__::_thesis:_for_x,_y_being_Element_of_T_st_[x,y]_in_T_@-->_holds_
S1[x,y]
let x, y be Element of T; ::_thesis: ( [x,y] in T @--> implies S1[x,y] )
 T @--> c= the InternalRel of T by Th66;
hence  ( [x,y] in T @--> implies S1[x,y] ) by ORDERS_2:def_5; ::_thesis: verum
end;
A3: for x being Element of T holds S1[x,x] ;
 for x, y being Element of T st T @--> reduces x,y holds
S1[x,y] from ABCMIZ_0:sch_2(A2, A3, A1);
hence  ( T @--> reduces t1,t2 implies t1 <= t2 ) ; ::_thesis: verum
end;

theorem Th68: :: ABCMIZ_0:68
for T being reflexive transitive antisymmetric with_suprema Noetherian non void adj-structured TAS-structure holds T @--> is irreflexive
proof
let T be reflexive transitive antisymmetric with_suprema Noetherian non void adj-structured TAS-structure ; ::_thesis: T @--> is irreflexive
set R = T @--> ;
let x be set ; :: according to RELAT_2:def_2,RELAT_2:def_10 ::_thesis: ( not x in field (T @-->) or not [x,x] in T @--> )
assume  x in field (T @-->) ; ::_thesis: not [x,x] in T @-->
assume A1: [x,x] in T @--> ; ::_thesis: contradiction
then reconsider x = x as type of T by ZFMISC_1:87;
consider a being adjective of T such that
A2: not a in adjs x and
A3: a is_properly_applicable_to x and
A4: a ast x = x by A1, Def31;
 a is_applicable_to x by A3, Def27;
hence  contradiction by A2, A4, Th21; ::_thesis: verum
end;

theorem Th69: :: ABCMIZ_0:69
for T being reflexive transitive antisymmetric with_suprema Noetherian non void adj-structured TAS-structure holds T @--> is strongly-normalizing
proof
let T be non empty reflexive transitive antisymmetric with_suprema Noetherian non void adj-structured TAS-structure ; ::_thesis: T @--> is strongly-normalizing
set R = T @--> ;
set Q = the InternalRel of T;
A1: field (T @-->) c= field the InternalRel of T by Th66, RELAT_1:16;
A2: T @--> c= the InternalRel of T by Th66;
 T @--> is co-well_founded
proof
let Y be set ; :: according to REWRITE1:def_16 ::_thesis: ( not Y c= field (T @-->) or Y = {} or ex b1 being set st
( b1 in Y & ( for b2 being set holds
( not b2 in Y or b1 = b2 or not [b1,b2] in T @--> ) ) ) )
assume that
A3: Y c= field (T @-->) and
A4: Y <> {} ; ::_thesis: ex b1 being set st
( b1 in Y & ( for b2 being set holds
( not b2 in Y or b1 = b2 or not [b1,b2] in T @--> ) ) )
 Y c= field the InternalRel of T by A1, A3, XBOOLE_1:1;
then consider a being set  such that
A5: a in Y and
A6: for b being set st b in Y & a <> b holds
not [a,b] in the InternalRel of T by A4, REWRITE1:def_16;
take  a ; ::_thesis: ( a in Y & ( for b1 being set holds
( not b1 in Y or a = b1 or not [a,b1] in T @--> ) ) )
thus  ( a in Y & ( for b1 being set holds
( not b1 in Y or a = b1 or not [a,b1] in T @--> ) ) ) by A2, A5, A6; ::_thesis: verum
end;
then  T @--> is co-well_founded irreflexive Relation by Th68;
hence  T @--> is strongly-normalizing ; ::_thesis: verum
end;

theorem Th70: :: ABCMIZ_0:70
for T being reflexive transitive antisymmetric with_suprema Noetherian non void adj-structured TAS-structure
for t being type of T
for A being finite Subset of the adjectives of T st ( for C being Subset of the adjectives of T st C c= A & C is_properly_applicable_to t & A ast t = C ast t holds
C = A ) holds
for s being one-to-one FinSequence of the adjectives of T st rng s = A & s is_properly_applicable_to t holds
for i being Nat st 1 <= i & i <= len s holds
[((apply (s,t)) . (i + 1)),((apply (s,t)) . i)] in T @-->
proof
let T be reflexive transitive antisymmetric with_suprema Noetherian non void adj-structured TAS-structure ; ::_thesis: for t being type of T
for A being finite Subset of the adjectives of T st ( for C being Subset of the adjectives of T st C c= A & C is_properly_applicable_to t & A ast t = C ast t holds
C = A ) holds
for s being one-to-one FinSequence of the adjectives of T st rng s = A & s is_properly_applicable_to t holds
for i being Nat st 1 <= i & i <= len s holds
[((apply (s,t)) . (i + 1)),((apply (s,t)) . i)] in T @-->
let t be type of T; ::_thesis: for A being finite Subset of the adjectives of T st ( for C being Subset of the adjectives of T st C c= A & C is_properly_applicable_to t & A ast t = C ast t holds
C = A ) holds
for s being one-to-one FinSequence of the adjectives of T st rng s = A & s is_properly_applicable_to t holds
for i being Nat st 1 <= i & i <= len s holds
[((apply (s,t)) . (i + 1)),((apply (s,t)) . i)] in T @-->
let A be finite Subset of the adjectives of T; ::_thesis: ( ( for C being Subset of the adjectives of T st C c= A & C is_properly_applicable_to t & A ast t = C ast t holds
C = A ) implies for s being one-to-one FinSequence of the adjectives of T st rng s = A & s is_properly_applicable_to t holds
for i being Nat st 1 <= i & i <= len s holds
[((apply (s,t)) . (i + 1)),((apply (s,t)) . i)] in T @--> )
assume A1: for C being Subset of the adjectives of T st C c= A & C is_properly_applicable_to t & A ast t = C ast t holds
C = A ; ::_thesis: for s being one-to-one FinSequence of the adjectives of T st rng s = A & s is_properly_applicable_to t holds
for i being Nat st 1 <= i & i <= len s holds
[((apply (s,t)) . (i + 1)),((apply (s,t)) . i)] in T @-->
let s be one-to-one FinSequence of the adjectives of T; ::_thesis: ( rng s = A & s is_properly_applicable_to t implies for i being Nat st 1 <= i & i <= len s holds
[((apply (s,t)) . (i + 1)),((apply (s,t)) . i)] in T @--> )
assume that
A2: rng s = A and
A3: s is_properly_applicable_to t ; ::_thesis: for i being Nat st 1 <= i & i <= len s holds
[((apply (s,t)) . (i + 1)),((apply (s,t)) . i)] in T @-->
let j be Nat; ::_thesis: ( 1 <= j & j <= len s implies [((apply (s,t)) . (j + 1)),((apply (s,t)) . j)] in T @--> )
assume that
A4: 1 <= j and
A5: j <= len s ; ::_thesis: [((apply (s,t)) . (j + 1)),((apply (s,t)) . j)] in T @-->
A6: len (apply (s,t)) = (len s) + 1 by Def19;
 j < (len s) + 1 by A5, NAT_1:13;
then  j in dom (apply (s,t)) by A6, A4, FINSEQ_3:25;
then  (apply (s,t)) . j in rng (apply (s,t)) by FUNCT_1:3;
then reconsider tt = (apply (s,t)) . j as type of T ;
A7: j in dom s by A4, A5, FINSEQ_3:25;
then  s . j in rng s by FUNCT_1:3;
then reconsider a = s . j as adjective of T ;
A8: (apply (s,t)) . (j + 1) = a ast tt by A7, Def19;
A9: not a in adjs tt
proof
assume A10: a in adjs tt ; ::_thesis: contradiction
consider i being Nat such that
A11: j = 1 + i by A4, NAT_1:10;
reconsider i = i as Element of NAT by ORDINAL1:def_12;
reconsider s1 = s | (Seg i) as FinSequence of the adjectives of T by FINSEQ_1:18;
 s1 c= s by TREES_1:def_1;
then consider s2 being FinSequence such that
A12: s = s1 ^ s2 by TREES_1:1;
reconsider s2 = s2 as FinSequence of the adjectives of T by A12, FINSEQ_1:36;
A13: len s = (len s1) + (len s2) by A12, FINSEQ_1:22;
then A14: s1 is_properly_applicable_to t by A3, A12, Th60;
reconsider s21 = s2 | (Seg 1) as FinSequence of the adjectives of T by FINSEQ_1:18;
 i <= len s by A5, A11, NAT_1:13;
then A15: len s1 = i by FINSEQ_1:17;
then A16: len s2 >= 1 by A5, A11, A13, XREAL_1:6;
then A17: len s21 = 1 by FINSEQ_1:17;
then A18: s21 = <*(s21 . 1)*> by FINSEQ_1:40;
then A19: rng s21 = {(s21 . 1)} by FINSEQ_1:39;
then reconsider b = s21 . 1 as adjective of T by ZFMISC_1:31;
A20: 1 in dom s2 by A16, FINSEQ_3:25;
 s21 c= s2 by TREES_1:def_1;
then consider s22 being FinSequence such that
A21: s2 = s21 ^ s22 by TREES_1:1;
reconsider s22 = s22 as FinSequence of the adjectives of T by A21, FINSEQ_1:36;
A22: rng s2 = (rng s21) \/ (rng s22) by A21, FINSEQ_1:31;
then A23: rng s22 c= rng s2 by XBOOLE_1:7;
A24: b = s2 . 1 by A18, A21, FINSEQ_1:41
.= a by A11, A12, A15, A20, FINSEQ_1:def_7 ;
then  a in rng s21 by A19, TARSKI:def_1;
then A25: a in rng s2 by A22, XBOOLE_0:def_3;
 s1 ast t = tt by A11, A12, A13, A15, Th36;
then A26: s1 ast t = a ast (s1 ast t) by A10, Th24
.= s21 ast (s1 ast t) by A18, A24, Th31 ;
 s2 is_properly_applicable_to s1 ast t by A3, A12, Th60;
then  s22 is_properly_applicable_to s1 ast t by A21, A26, Th60;
then A27: s1 ^ s22 is_properly_applicable_to t by A14, Th61;
reconsider B = rng (s1 ^ s22) as Subset of the adjectives of T ;
A28: B = (rng s1) \/ (rng s22) by FINSEQ_1:31;
A29: A = (rng s1) \/ (rng s2) by A2, A12, FINSEQ_1:31;
s ast t = s2 ast (s1 ast t) by A12, Th37
.= s22 ast (s1 ast t) by A21, A26, Th37
.= (s1 ^ s22) ast t by Th37 ;
then A30: A ast t = (s1 ^ s22) ast t by A2, A3, Th56, Th57
.= B ast t by A27, Th56, Th57 ;
 B is_properly_applicable_to t by A27, Def29;
then  B = A by A1, A30, A28, A29, A23, XBOOLE_1:9;
then A31: a in B by A29, A25, XBOOLE_0:def_3;
percases ( a in rng s1 or a in rng s22 ) by A28, A31, XBOOLE_0:def_3;
suppose a in rng s1 ; ::_thesis: contradiction
then consider x being set  such that
A32: x in dom s1 and
A33: a = s1 . x by FUNCT_1:def_3;
reconsider x = x as Element of NAT by A32;
 x <= len s1 by A32, FINSEQ_3:25;
then A34: x < j by A11, A15, NAT_1:13;
A35: dom s1 c= dom s by A12, FINSEQ_1:26;
 s . x = a by A12, A32, A33, FINSEQ_1:def_7;
hence  contradiction by A7, A32, A35, A34, FUNCT_1:def_4; ::_thesis: verum
end;
suppose a in rng s22 ; ::_thesis: contradiction
then consider x being set  such that
A36: x in dom s22 and
A37: a = s22 . x by FUNCT_1:def_3;
reconsider x = x as Element of NAT by A36;
A38: 1 + x in dom s2 by A17, A21, A36, FINSEQ_1:28;
 x >= 0 + 1 by A36, FINSEQ_3:25;
then A39: j + x > j + 0 by XREAL_1:6;
 s2 . (1 + x) = a by A17, A21, A36, A37, FINSEQ_1:def_7;
then A40: s . (i + (1 + x)) = a by A12, A15, A38, FINSEQ_1:def_7;
 i + (1 + x) in dom s by A12, A15, A38, FINSEQ_1:28;
hence  contradiction by A7, A11, A39, A40, FUNCT_1:def_4; ::_thesis: verum
end;
end;
end;
 a is_properly_applicable_to tt by A3, A7, Def28;
hence  [((apply (s,t)) . (j + 1)),((apply (s,t)) . j)] in T @--> by A8, A9, Def31; ::_thesis: verum
end;

theorem Th71: :: ABCMIZ_0:71
for T being reflexive transitive antisymmetric with_suprema Noetherian non void adj-structured TAS-structure
for t being type of T
for A being finite Subset of the adjectives of T st ( for C being Subset of the adjectives of T st C c= A & C is_properly_applicable_to t & A ast t = C ast t holds
C = A ) holds
for s being one-to-one FinSequence of the adjectives of T st rng s = A & s is_properly_applicable_to t holds
Rev (apply (s,t)) is RedSequence of T @-->
proof
let T be reflexive transitive antisymmetric with_suprema Noetherian non void adj-structured TAS-structure ; ::_thesis: for t being type of T
for A being finite Subset of the adjectives of T st ( for C being Subset of the adjectives of T st C c= A & C is_properly_applicable_to t & A ast t = C ast t holds
C = A ) holds
for s being one-to-one FinSequence of the adjectives of T st rng s = A & s is_properly_applicable_to t holds
Rev (apply (s,t)) is RedSequence of T @-->
let t be type of T; ::_thesis: for A being finite Subset of the adjectives of T st ( for C being Subset of the adjectives of T st C c= A & C is_properly_applicable_to t & A ast t = C ast t holds
C = A ) holds
for s being one-to-one FinSequence of the adjectives of T st rng s = A & s is_properly_applicable_to t holds
Rev (apply (s,t)) is RedSequence of T @-->
let A be finite Subset of the adjectives of T; ::_thesis: ( ( for C being Subset of the adjectives of T st C c= A & C is_properly_applicable_to t & A ast t = C ast t holds
C = A ) implies for s being one-to-one FinSequence of the adjectives of T st rng s = A & s is_properly_applicable_to t holds
Rev (apply (s,t)) is RedSequence of T @--> )
assume A1: for C being Subset of the adjectives of T st C c= A & C is_properly_applicable_to t & A ast t = C ast t holds
C = A ; ::_thesis: for s being one-to-one FinSequence of the adjectives of T st rng s = A & s is_properly_applicable_to t holds
Rev (apply (s,t)) is RedSequence of T @-->
let s be one-to-one FinSequence of the adjectives of T; ::_thesis: ( rng s = A & s is_properly_applicable_to t implies Rev (apply (s,t)) is RedSequence of T @--> )
assume that
A2: rng s = A and
A3: s is_properly_applicable_to t ; ::_thesis: Rev (apply (s,t)) is RedSequence of T @-->
A4: len (Rev (apply (s,t))) = len (apply (s,t)) by FINSEQ_5:def_3;
hence  len (Rev (apply (s,t))) > 0 ; :: according to REWRITE1:def_2 ::_thesis: for b1 being Element of NAT holds
( not b1 in dom (Rev (apply (s,t))) or not b1 + 1 in dom (Rev (apply (s,t))) or [((Rev (apply (s,t))) . b1),((Rev (apply (s,t))) . (b1 + 1))] in T @--> )
let i be Element of NAT ; ::_thesis: ( not i in dom (Rev (apply (s,t))) or not i + 1 in dom (Rev (apply (s,t))) or [((Rev (apply (s,t))) . i),((Rev (apply (s,t))) . (i + 1))] in T @--> )
assume that
A5: i in dom (Rev (apply (s,t))) and
A6: i + 1 in dom (Rev (apply (s,t))) ; ::_thesis: [((Rev (apply (s,t))) . i),((Rev (apply (s,t))) . (i + 1))] in T @-->
A7: len (apply (s,t)) = (len s) + 1 by Def19;
then A8: (Rev (apply (s,t))) . i = (apply (s,t)) . ((((len s) + 1) - i) + 1) by A5, FINSEQ_5:def_3;
 i + 1 <= (len s) + 1 by A4, A7, A6, FINSEQ_3:25;
then consider j being Nat such that
A9: (len s) + 1 = (i + 1) + j by NAT_1:10;
A10: (Rev (apply (s,t))) . (i + 1) = (apply (s,t)) . ((((len s) + 1) - (i + 1)) + 1) by A7, A6, FINSEQ_5:def_3;
A11: i >= 1 by A5, FINSEQ_3:25;
 len s = i + j by A9;
then A12: j + 1 <= len s by A11, XREAL_1:6;
 j + 1 >= 1 by NAT_1:11;
hence  [((Rev (apply (s,t))) . i),((Rev (apply (s,t))) . (i + 1))] in T @--> by A1, A2, A3, A8, A10, A9, A12, Th70; ::_thesis: verum
end;

theorem Th72: :: ABCMIZ_0:72
for T being reflexive transitive antisymmetric with_suprema Noetherian non void adj-structured TAS-structure
for t being type of T
for A being finite Subset of the adjectives of T st A is_properly_applicable_to t holds
T @--> reduces A ast t,t
proof
let T be reflexive transitive antisymmetric with_suprema Noetherian non void adj-structured TAS-structure ; ::_thesis: for t being type of T
for A being finite Subset of the adjectives of T st A is_properly_applicable_to t holds
T @--> reduces A ast t,t
set R = T @--> ;
let t be type of T; ::_thesis: for A being finite Subset of the adjectives of T st A is_properly_applicable_to t holds
T @--> reduces A ast t,t
let A be finite Subset of the adjectives of T; ::_thesis: ( A is_properly_applicable_to t implies T @--> reduces A ast t,t )
assume  A is_properly_applicable_to t ; ::_thesis: T @--> reduces A ast t,t
then consider A9 being Subset of the adjectives of T such that
 A9 c= A and
A1: A9 is_properly_applicable_to t and
A2: A ast t = A9 ast t and
A3: for C being Subset of the adjectives of T st C c= A9 & C is_properly_applicable_to t & A ast t = C ast t holds
C = A9 by Th64;
consider s being one-to-one FinSequence of the adjectives of T such that
A4: rng s = A9 and
A5: s is_properly_applicable_to t by A1, Th65;
reconsider p = Rev (apply (s,t)) as RedSequence of T @--> by A2, A3, A4, A5, Th71;
take  p ; :: according to REWRITE1:def_3 ::_thesis: ( p . 1 = A ast t & p . (len p) = t )
thus p . 1 = (apply (s,t)) . (len (apply (s,t))) by FINSEQ_5:62
.= s ast t by Def19
.= A ast t by A2, A4, A5, Th56, Th57 ; ::_thesis: p . (len p) = t
thus p . (len p) = p . (len (apply (s,t))) by FINSEQ_5:def_3
.= (apply (s,t)) . 1 by FINSEQ_5:62
.= t by Def19 ; ::_thesis: verum
end;

theorem Th73: :: ABCMIZ_0:73
for X being non empty set
for R being Relation of X
for r being RedSequence of R st r . 1 in X holds
r is FinSequence of X
proof
let X be non empty set ; ::_thesis: for R being Relation of X
for r being RedSequence of R st r . 1 in X holds
r is FinSequence of X
let R be Relation of X; ::_thesis: for r being RedSequence of R st r . 1 in X holds
r is FinSequence of X
let p be RedSequence of R; ::_thesis: ( p . 1 in X implies p is FinSequence of X )
assume A1: p . 1 in X ; ::_thesis: p is FinSequence of X
let x be set ; :: according to TARSKI:def_3,FINSEQ_1:def_4 ::_thesis: ( not x in rng p or x in X )
assume  x in rng p ; ::_thesis: x in X
then consider i being set  such that
A2: i in dom p and
A3: x = p . i by FUNCT_1:def_3;
reconsider i = i as Element of NAT by A2;
A4: i >= 1 by A2, FINSEQ_3:25;
percases ( i = 1 or i > 1 ) by A4, XXREAL_0:1;
suppose i = 1 ; ::_thesis: x in X
hence  x in X by A1, A3; ::_thesis: verum
end;
suppose i > 1 ; ::_thesis: x in X
then  i >= 1 + 1 by NAT_1:13;
then consider j being Nat such that
A5: i = (1 + 1) + j by NAT_1:10;
A6: i = (j + 1) + 1 by A5;
A7: j + 1 >= 1 by NAT_1:11;
 i <= len p by A2, FINSEQ_3:25;
then  j + 1 < len p by A6, NAT_1:13;
then  j + 1 in dom p by A7, FINSEQ_3:25;
then  [(p . (j + 1)),x] in R by A2, A3, A6, REWRITE1:def_2;
hence  x in X by ZFMISC_1:87; ::_thesis: verum
end;
end;
end;

theorem Th74: :: ABCMIZ_0:74
for X being non empty set
for R being Relation of X
for x being Element of X
for y being set st R reduces x,y holds
y in X
proof
let X be non empty set ; ::_thesis: for R being Relation of X
for x being Element of X
for y being set st R reduces x,y holds
y in X
let R be Relation of X; ::_thesis: for x being Element of X
for y being set st R reduces x,y holds
y in X
let x be Element of X; ::_thesis: for y being set st R reduces x,y holds
y in X
let y be set ; ::_thesis: ( R reduces x,y implies y in X )
given p being RedSequence of R such that A1: p . 1 = x and
A2: p . (len p) = y ; :: according to REWRITE1:def_3 ::_thesis: y in X
 len p >= 0 + 1 by NAT_1:13;
then  len p in dom p by FINSEQ_3:25;
then A3: y in rng p by A2, FUNCT_1:3;
 p is FinSequence of X by A1, Th73;
then  rng p c= X by FINSEQ_1:def_4;
hence  y in X by A3; ::_thesis: verum
end;

theorem Th75: :: ABCMIZ_0:75
for X being non empty set
for R being Relation of X st R is with_UN_property & R is weakly-normalizing holds
for x being Element of X holds nf (x,R) in X
proof
let X be non empty set ; ::_thesis: for R being Relation of X st R is with_UN_property & R is weakly-normalizing holds
for x being Element of X holds nf (x,R) in X
let R be Relation of X; ::_thesis: ( R is with_UN_property & R is weakly-normalizing implies for x being Element of X holds nf (x,R) in X )
assume A1: ( R is with_UN_property & R is weakly-normalizing ) ; ::_thesis: for x being Element of X holds nf (x,R) in X
let x be Element of X; ::_thesis: nf (x,R) in X
 nf (x,R) is_a_normal_form_of x,R by A1, REWRITE1:54;
then  R reduces x, nf (x,R) by REWRITE1:def_6;
hence  nf (x,R) in X by Th74; ::_thesis: verum
end;

theorem Th76: :: ABCMIZ_0:76
for T being reflexive transitive antisymmetric with_suprema Noetherian non void adj-structured TAS-structure
for t1, t2 being type of T st T @--> reduces t1,t2 holds
ex A being finite Subset of the adjectives of T st
( A is_properly_applicable_to t2 & t1 = A ast t2 )
proof
let T be reflexive transitive antisymmetric with_suprema Noetherian non void adj-structured TAS-structure ; ::_thesis: for t1, t2 being type of T st T @--> reduces t1,t2 holds
ex A being finite Subset of the adjectives of T st
( A is_properly_applicable_to t2 & t1 = A ast t2 )
let t1, t2 be type of T; ::_thesis: ( T @--> reduces t1,t2 implies ex A being finite Subset of the adjectives of T st
( A is_properly_applicable_to t2 & t1 = A ast t2 ) )
set R = T @--> ;
given p being RedSequence of T @-->  such that A1: p . 1 = t1 and
A2: t2 = p . (len p) ; :: according to REWRITE1:def_3 ::_thesis: ex A being finite Subset of the adjectives of T st
( A is_properly_applicable_to t2 & t1 = A ast t2 )
defpred S1[ set , set ] means  ex j being Element of NAT ex a being adjective of T ex t being type of T st
( $2 = a & $1 = j & a ast t = p . j & t = p . (j + 1) & a is_properly_applicable_to t );
A3: len (Rev p) = len p by FINSEQ_5:def_3;
A4: ((len p) - 1) + 1 = len p ;
A5: len p >= 0 + 1 by NAT_1:13;
then consider i being Nat such that
A6: len p = 1 + i by NAT_1:10;
reconsider i = i as Element of NAT by ORDINAL1:def_12;
A7: now__::_thesis:_for_x_being_set_st_x_in_Seg_i_holds_
ex_y_being_set_st_
(_y_in_the_adjectives_of_T_&_S1[x,y]_)
let x be set ; ::_thesis: ( x in Seg i implies ex y being set st
( y in the adjectives of T & S1[x,y] ) )
assume A8: x in Seg i ; ::_thesis: ex y being set st
( y in the adjectives of T & S1[x,y] )
then reconsider j = x as Element of NAT ;
A9: j >= 1 by A8, FINSEQ_1:1;
then A10: 1 <= j + 1 by NAT_1:13;
A11: j <= i by A8, FINSEQ_1:1;
then  j < len p by A6, NAT_1:13;
then A12: j in dom p by A9, FINSEQ_3:25;
 j + 1 <= len p by A6, A11, XREAL_1:6;
then  j + 1 in dom p by A10, FINSEQ_3:25;
then A13: [(p . j),(p . (j + 1))] in T @--> by A12, REWRITE1:def_2;
then reconsider q1 = p . j, q2 = p . (j + 1) as type of T by ZFMISC_1:87;
 ex a being adjective of T st
( not a in adjs q2 & a is_properly_applicable_to q2 & a ast q2 = q1 ) by A13, Def31;
hence  ex y being set st
( y in the adjectives of T & S1[x,y] ) ; ::_thesis: verum
end;
consider f being Function such that
A14: ( dom f = Seg i & rng f c= the adjectives of T ) and
A15: for x being set st x in Seg i holds
S1[x,f . x] from FUNCT_1:sch_5(A7);
 f is FinSequence by A14, FINSEQ_1:def_2;
then reconsider f = f as FinSequence of the adjectives of T by A14, FINSEQ_1:def_4;
A16: len f = i by A14, FINSEQ_1:def_3;
set r = Rev f;
defpred S2[ Element of NAT ] means ( 1 + $1 <= len p implies (Rev p) . (1 + $1) = (apply ((Rev f),t2)) . (1 + $1) );
A17: len (Rev f) = len f by FINSEQ_5:def_3;
A18: now__::_thesis:_for_j_being_Element_of_NAT_st_S2[j]_holds_
S2[j_+_1]
let j be Element of NAT ; ::_thesis: ( S2[j] implies S2[j + 1] )
assume A19: S2[j] ; ::_thesis: S2[j + 1]
now__::_thesis:_(_1_+_(j_+_1)_<=_len_p_implies_(Rev_p)_._(1_+_(j_+_1))_=_(apply_((Rev_f),t2))_._(1_+_(j_+_1))_)
A20: j + 1 >= 1 by NAT_1:11;
assume A21: 1 + (j + 1) <= len p ; ::_thesis: (Rev p) . (1 + (j + 1)) = (apply ((Rev f),t2)) . (1 + (j + 1))
then  j + 1 <= i by A6, XREAL_1:6;
then consider x being Nat such that
A22: i = (j + 1) + x by NAT_1:10;
reconsider x = x as Element of NAT by ORDINAL1:def_12;
A23: (i + 1) - (j + 1) = x + 1 by A22;
 j + 1 < len p by A21, NAT_1:13;
then  j + 1 in dom (Rev p) by A3, A20, FINSEQ_3:25;
then A24: (Rev p) . (j + 1) = p . ((x + 1) + 1) by A6, A23, FINSEQ_5:def_3;
A25: (i + 1) - (1 + (j + 1)) = x by A22;
 1 + (j + 1) >= 1 by NAT_1:11;
then  1 + (j + 1) in dom (Rev p) by A3, A21, FINSEQ_3:25;
then A26: (Rev p) . (1 + (j + 1)) = p . (x + 1) by A6, A25, FINSEQ_5:def_3;
 i = (x + 1) + j by A22;
then A27: i >= x + 1 by NAT_1:11;
 x + 1 >= 1 by NAT_1:11;
then  x + 1 in Seg i by A27;
then consider k being Element of NAT , a being adjective of T, t being type of T such that
A28: f . (x + 1) = a and
A29: x + 1 = k and
A30: a ast t = p . k and
A31: t = p . (k + 1) and
 a is_properly_applicable_to t by A15;
A32: j + 1 >= 1 by NAT_1:11;
 j + 1 <= i by A22, NAT_1:11;
then A33: j + 1 in dom (Rev f) by A17, A16, A32, FINSEQ_3:25;
then (Rev f) . (j + 1) = f . (((len f) - (j + 1)) + 1) by FINSEQ_5:def_3
.= a by A16, A22, A28 ;
hence  (Rev p) . (1 + (j + 1)) = (apply ((Rev f),t2)) . (1 + (j + 1)) by A19, A21, A29, A30, A31, A33, A24, A26, Def19, NAT_1:13; ::_thesis: verum
end;
hence  S2[j + 1] ; ::_thesis: verum
end;
reconsider A = rng f as finite Subset of the adjectives of T ;
take  A ; ::_thesis: ( A is_properly_applicable_to t2 & t1 = A ast t2 )
A34: len (apply ((Rev f),t2)) = (len (Rev f)) + 1 by Def19;
 1 in dom (Rev p) by A5, A3, FINSEQ_3:25;
then  (Rev p) . 1 = t2 by A2, A4, FINSEQ_5:def_3;
then A35: S2[ 0 ] by Def19;
A36: for j being Element of NAT holds S2[j] from NAT_1:sch_1(A35, A18);
now__::_thesis:_for_j_being_Nat_st_1_<=_j_&_j_<=_len_p_holds_
(Rev_p)_._j_=_(apply_((Rev_f),t2))_._j
let j be Nat; ::_thesis: ( 1 <= j & j <= len p implies (Rev p) . j = (apply ((Rev f),t2)) . j )
assume  1 <= j ; ::_thesis: ( j <= len p implies (Rev p) . j = (apply ((Rev f),t2)) . j )
then consider k being Nat such that
A37: j = 1 + k by NAT_1:10;
 k in NAT by ORDINAL1:def_12;
hence  ( j <= len p implies (Rev p) . j = (apply ((Rev f),t2)) . j ) by A36, A37; ::_thesis: verum
end;
then A38: Rev p = apply ((Rev f),t2) by A6, A17, A34, A16, A3, FINSEQ_1:14;
then A39: p = Rev (apply ((Rev f),t2)) ;
A40: Rev f is_properly_applicable_to t2
proof
let j be Nat; :: according to ABCMIZ_0:def_28 ::_thesis: for a being adjective of T
for s being type of T st j in dom (Rev f) & a = (Rev f) . j & s = (apply ((Rev f),t2)) . j holds
a is_properly_applicable_to s
let a be adjective of T; ::_thesis: for s being type of T st j in dom (Rev f) & a = (Rev f) . j & s = (apply ((Rev f),t2)) . j holds
a is_properly_applicable_to s
let s be type of T; ::_thesis: ( j in dom (Rev f) & a = (Rev f) . j & s = (apply ((Rev f),t2)) . j implies a is_properly_applicable_to s )
assume that
A41: j in dom (Rev f) and
A42: a = (Rev f) . j and
A43: s = (apply ((Rev f),t2)) . j ; ::_thesis: a is_properly_applicable_to s
 j <= len (Rev f) by A41, FINSEQ_3:25;
then consider k being Nat such that
A44: len (Rev f) = j + k by NAT_1:10;
A45: len (Rev f) = len f by FINSEQ_5:def_3;
reconsider k = k as Element of NAT by ORDINAL1:def_12;
A46: k + 1 >= 1 by NAT_1:11;
A47: j >= 1 by A41, FINSEQ_3:25;
then  k + 1 <= i by A16, A44, A45, XREAL_1:6;
then  ((len f) - j) + 1 in Seg i by A44, A45, A46;
then consider o being Element of NAT , b being adjective of T, u being type of T such that
A48: f . (((len f) - j) + 1) = b and
A49: ((len f) - j) + 1 = o and
 b ast u = p . o and
A50: u = p . (o + 1) and
A51: b is_properly_applicable_to u by A15;
A52: o + 1 >= 1 by NAT_1:11;
 i + 1 = (k + 1) + j by A17, A16, A44;
then  o + 1 <= len p by A6, A44, A45, A47, A49, XREAL_1:6;
then A53: o + 1 in dom p by A52, FINSEQ_3:25;
A54: a = b by A41, A42, A48, FINSEQ_5:def_3;
 ((len (apply ((Rev f),t2))) - (o + 1)) + 1 = j by A17, A34, A49;
hence  a is_properly_applicable_to s by A39, A43, A50, A51, A53, A54, FINSEQ_5:def_3; ::_thesis: verum
end;
thus  A is_properly_applicable_to t2 ::_thesis: t1 = A ast t2
proof
take  Rev f ; :: according to ABCMIZ_0:def_29 ::_thesis: ( rng (Rev f) = A & Rev f is_properly_applicable_to t2 )
thus  ( rng (Rev f) = A & Rev f is_properly_applicable_to t2 ) by A40, FINSEQ_5:57; ::_thesis: verum
end;
 rng (Rev f) = A by FINSEQ_5:57;
then A ast t2 = (Rev f) ast t2 by A40, Th56, Th57
.= (apply ((Rev f),t2)) . ((len (Rev f)) + 1) ;
hence  t1 = A ast t2 by A1, A34, A3, A38, FINSEQ_5:62; ::_thesis: verum
end;

theorem Th77: :: ABCMIZ_0:77
for T being reflexive transitive antisymmetric with_suprema Noetherian non void adj-structured commutative TAS-structure holds
( T @--> is with_Church-Rosser_property & T @--> is with_UN_property )
proof
let T be non empty reflexive transitive antisymmetric with_suprema Noetherian non void adj-structured commutative TAS-structure ; ::_thesis: ( T @--> is with_Church-Rosser_property & T @--> is with_UN_property )
set R = T @--> ;
 T @--> is locally-confluent
proof
let a, b, c be set ; :: according to REWRITE1:def_24 ::_thesis: ( not [a,b] in T @--> or not [a,c] in T @--> or b,c are_convergent_wrt T @--> )
assume that
A1: [a,b] in T @--> and
A2: [a,c] in T @--> ; ::_thesis: b,c are_convergent_wrt T @-->
reconsider t = a, t1 = b, t2 = c as type of T by A1, A2, ZFMISC_1:87;
consider a2 being adjective of T such that
 not a2 in adjs t1 and
A3: a2 is_properly_applicable_to t1 and
A4: a2 ast t1 = t by A1, Def31;
set tt = t1 "\/" t2;
take  t1 "\/" t2 ; :: according to REWRITE1:def_7 ::_thesis: ( T @--> reduces b,t1 "\/" t2 & T @--> reduces c,t1 "\/" t2 )
consider a3 being adjective of T such that
 not a3 in adjs t2 and
A5: a3 is_properly_applicable_to t2 and
A6: a3 ast t2 = t by A2, Def31;
 a3 is_applicable_to t2 by A5, Def27;
then  t <= t2 by A6, Th20;
then A7: ex B being finite Subset of the adjectives of T st
( B is_properly_applicable_to t1 "\/" t2 & B ast (t1 "\/" t2) = t2 ) by A3, A4, Def30;
 a2 is_applicable_to t1 by A3, Def27;
then  t <= t1 by A4, Th20;
then  ex A being finite Subset of the adjectives of T st
( A is_properly_applicable_to t1 "\/" t2 & A ast (t1 "\/" t2) = t1 ) by A5, A6, Def30;
hence  ( T @--> reduces b,t1 "\/" t2 & T @--> reduces c,t1 "\/" t2 ) by A7, Th72; ::_thesis: verum
end;
then  T @--> is strongly-normalizing locally-confluent Relation by Th69;
hence  ( T @--> is with_Church-Rosser_property & T @--> is with_UN_property ) ; ::_thesis: verum
end;

begin

definition
let T be non empty reflexive transitive antisymmetric with_suprema Noetherian non void adj-structured commutative TAS-structure ;
let t be type of T;
func radix t ->  type of T equals :: ABCMIZ_0:def 32
 nf (t,(T @-->));
coherence
 nf (t,(T @-->)) is type of T
proof
 T @--> is strongly-normalizing with_UN_property with_Church-Rosser_property Relation by Th69, Th77;
hence  nf (t,(T @-->)) is type of T by Th75; ::_thesis: verum
end;
end;

:: deftheorem  defines radix ABCMIZ_0:def_32_:_
 for T being non empty reflexive transitive antisymmetric with_suprema Noetherian non void adj-structured commutative TAS-structure
for t being type of T holds radix t = nf (t,(T @-->));

theorem Th78: :: ABCMIZ_0:78
for T being non empty reflexive transitive antisymmetric with_suprema Noetherian non void adj-structured commutative TAS-structure
for t being type of T holds T @--> reduces t, radix t
proof
let T be non empty reflexive transitive antisymmetric with_suprema Noetherian non void adj-structured commutative TAS-structure ; ::_thesis: for t being type of T holds T @--> reduces t, radix t
let t be type of T; ::_thesis: T @--> reduces t, radix t
set R = T @--> ;
 T @--> is strongly-normalizing with_UN_property with_Church-Rosser_property Relation by Th69, Th77;
then  nf (t,(T @-->)) is_a_normal_form_of t,T @--> by REWRITE1:54;
hence  T @--> reduces t, radix t by REWRITE1:def_6; ::_thesis: verum
end;

theorem :: ABCMIZ_0:79
for T being non empty reflexive transitive antisymmetric with_suprema Noetherian non void adj-structured commutative TAS-structure
for t being type of T holds t <= radix t by Th67, Th78;

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) )
proof
let T be non empty reflexive transitive antisymmetric with_suprema Noetherian non void adj-structured commutative TAS-structure ; ::_thesis: 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) )
let t be type of T; ::_thesis: 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) )
set R = T @--> ;
set AA =  {  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 )  }  ;
A1: T @--> is strongly-normalizing with_UN_property with_Church-Rosser_property Relation by Th69, Th77;
A2: radix t is_>=_than  {  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 )  }
proof
let tt be type of T; :: according to LATTICE3:def_9 ::_thesis: ( not tt in  {  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 )  }  or tt <= radix t )
assume  tt in  {  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 )  }  ; ::_thesis: tt <= radix t
then  ex t9 being type of T st
( tt = t9 & ex A being finite Subset of the adjectives of T st
( A is_properly_applicable_to t9 & A ast t9 = t ) ) ;
then  T @--> reduces t,tt by Th72;
then  t,tt are_convertible_wrt T @--> by REWRITE1:25;
then  nf (t,(T @-->)) = nf (tt,(T @-->)) by A1, REWRITE1:55;
then  nf (t,(T @-->)) is_a_normal_form_of tt,T @--> by A1, REWRITE1:54;
then  T @--> reduces tt, nf (t,(T @-->)) by REWRITE1:def_6;
hence  tt <= radix t by Th67; ::_thesis: verum
end;
 ex A being finite Subset of the adjectives of T st
( A is_properly_applicable_to radix t & A ast (radix t) = t ) by Th76, Th78;
then  radix t in  {  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 )  }  ;
then  for t9 being type of T st t9 is_>=_than  {  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
radix t <= t9 by LATTICE3:def_9;
hence  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) ) by A2, YELLOW_0:30; ::_thesis: verum
end;

theorem Th81: :: ABCMIZ_0:81
for T being non empty reflexive transitive antisymmetric with_suprema Noetherian non void adj-structured commutative TAS-structure
for t1, t2 being type of T
for a being adjective of T st a is_properly_applicable_to t1 & a ast t1 <= radix t2 holds
t1 <= radix t2
proof
let T be non empty reflexive transitive antisymmetric with_suprema Noetherian non void adj-structured commutative TAS-structure ; ::_thesis: for t1, t2 being type of T
for a being adjective of T st a is_properly_applicable_to t1 & a ast t1 <= radix t2 holds
t1 <= radix t2
let t1, t2 be type of T; ::_thesis: for a being adjective of T st a is_properly_applicable_to t1 & a ast t1 <= radix t2 holds
t1 <= radix t2
let a be adjective of T; ::_thesis: ( a is_properly_applicable_to t1 & a ast t1 <= radix t2 implies t1 <= radix t2 )
set R = T @--> ;
set AA =  {  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 = t2 )  }  ;
assume that
A1: a is_properly_applicable_to t1 and
A2: a ast t1 <= radix t2 ; ::_thesis: t1 <= radix t2
consider A being finite Subset of the adjectives of T such that
A3: A is_properly_applicable_to t1 "\/" (radix t2) and
A4: A ast (t1 "\/" (radix t2)) = radix t2 by A1, A2, Def30;
consider v1 being FinSequence of the adjectives of T such that
A5: rng v1 = A and
A6: v1 is_properly_applicable_to t1 "\/" (radix t2) by A3, Def29;
 T @--> is strongly-normalizing with_UN_property with_Church-Rosser_property Relation by Th69, Th77;
then  nf (t2,(T @-->)) is_a_normal_form_of t2,T @--> by REWRITE1:54;
then  T @--> reduces t2, nf (t2,(T @-->)) by REWRITE1:def_6;
then consider B being finite Subset of the adjectives of T such that
A7: B is_properly_applicable_to radix t2 and
A8: t2 = B ast (radix t2) by Th76;
consider v2 being FinSequence of the adjectives of T such that
A9: rng v2 = B and
A10: v2 is_properly_applicable_to radix t2 by A7, Def29;
A11: rng (v1 ^ v2) = A \/ B by A5, A9, FINSEQ_1:31;
A12: radix t2 = v1 ast (t1 "\/" (radix t2)) by A4, A5, A6, Th56, Th57;
then A13: v1 ^ v2 is_properly_applicable_to t1 "\/" (radix t2) by A6, A10, Th61;
then A14: A \/ B is_properly_applicable_to t1 "\/" (radix t2) by A11, Def29;
(A \/ B) ast (t1 "\/" (radix t2)) = (v1 ^ v2) ast (t1 "\/" (radix t2)) by A11, A13, Th56, Th57
.= v2 ast (radix t2) by A12, Th37
.= t2 by A8, A9, A10, Th56, Th57 ;
then  t1 "\/" (radix t2) in  {  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 = t2 )  }  by A14;
then  t1 "\/" (radix t2) <= "\/" ( {  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 = t2 )  }  ,T) by Th80, YELLOW_4:1;
then A15: t1 "\/" (radix t2) <= radix t2 by Th80;
 t1 "\/" (radix t2) >= t1 by YELLOW_0:22;
hence  t1 <= radix t2 by A15, YELLOW_0:def_2; ::_thesis: verum
end;

theorem :: ABCMIZ_0:82
for T being non empty reflexive transitive antisymmetric with_suprema Noetherian non void adj-structured commutative TAS-structure
for t1, t2 being type of T st t1 <= t2 holds
radix t1 <= radix t2
proof
let T be non empty reflexive transitive antisymmetric with_suprema Noetherian non void adj-structured commutative TAS-structure ; ::_thesis: for t1, t2 being type of T st t1 <= t2 holds
radix t1 <= radix t2
set R = T @--> ;
let t1, t2 be type of T; ::_thesis: ( t1 <= t2 implies radix t1 <= radix t2 )
assume A1: t1 <= t2 ; ::_thesis: radix t1 <= radix t2
 t2 <= radix t2 by Th67, Th78;
then A2: t1 <= radix t2 by A1, YELLOW_0:def_2;
set X = the carrier of T;
defpred S1[ Element of the carrier of T, Element of the carrier of T] means ( $1 <= radix t2 implies $2 <= radix t2 );
A3: for x, y, z being Element of the carrier of T st S1[x,y] & S1[y,z] holds
S1[x,z] ;
A4: now__::_thesis:_for_x,_y_being_Element_of_the_carrier_of_T_st_[x,y]_in_T_@-->_holds_
S1[x,y]
let x, y be Element of the carrier of T; ::_thesis: ( [x,y] in T @--> implies S1[x,y] )
reconsider t1 = x, t2 = y as type of T ;
assume  [x,y] in T @--> ; ::_thesis: S1[x,y]
then  ex a being adjective of T st
( not a in adjs t2 & a is_properly_applicable_to t2 & a ast t2 = t1 ) by Def31;
hence  S1[x,y] by Th81; ::_thesis: verum
end;
A5: for x being Element of the carrier of T holds S1[x,x] ;
 for x, y being Element of T st T @--> reduces x,y holds
S1[x,y] from ABCMIZ_0:sch_2(A4, A5, A3);
hence  radix t1 <= radix t2 by A2, Th78; ::_thesis: verum
end;

theorem :: ABCMIZ_0:83
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 a being adjective of T st a is_properly_applicable_to t holds
radix (a ast t) = radix t
proof
let T be non empty reflexive transitive antisymmetric with_suprema Noetherian non void adj-structured commutative TAS-structure ; ::_thesis: for t being type of T
for a being adjective of T st a is_properly_applicable_to t holds
radix (a ast t) = radix t
let t be type of T; ::_thesis: for a being adjective of T st a is_properly_applicable_to t holds
radix (a ast t) = radix t
let a be adjective of T; ::_thesis: ( a is_properly_applicable_to t implies radix (a ast t) = radix t )
A1: ( a in adjs t or not a in adjs t ) ;
assume  a is_properly_applicable_to t ; ::_thesis: radix (a ast t) = radix t
then  ( a ast t = t or [(a ast t),t] in T @--> ) by A1, Def31, Th24;
then  T @--> reduces a ast t,t by REWRITE1:12, REWRITE1:15;
then A2: a ast t,t are_convertible_wrt T @--> by REWRITE1:25;
 T @--> is strongly-normalizing with_UN_property with_Church-Rosser_property Relation by Th69, Th77;
hence  radix (a ast t) = radix t by A2, REWRITE1:55; ::_thesis: verum
end;