:: ABCMIZ_0 semantic presentation

registration
cluster non empty trivial reflexive -> non empty complete RelStr ;
coherence
for b1 being non empty RelStr holds
( b1 is trivial & b1 is reflexive implies b1 is complete )
proof
let c1 be non empty RelStr ;
assume E1: for b1, b2 being Element of c1 holds b1 = b2 ; :: according to REALSET2:def 7
assume E2: for b1 being Element of c1 holds b1 <= b1 ; :: according to YELLOW_0:def 1
let c2 be set ; :: according to LATTICE3:def 12
consider c3 being Element of c1;
take c3 ;
thus c2 is_<=_than c3
proof
let c4 be Element of c1; :: according to LATTICE3:def 9
c3 = c4 by E1;
hence not ( c4 in c2 & not c4 <= c3 ) by E2;
end;
let c4 be Element of c1;
c3 = c4 by E1;
hence not ( c2 is_<=_than c4 & not c3 <= c4 ) by E2;
end;
end;

definition
let c1 be RelStr ;
mode type is Element of a1;
end;

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

:: deftheorem Def1 defines Noetherian ABCMIZ_0:def 1 :
for b1 being RelStr holds
( b1 is Noetherian iff the InternalRel of b1 is co-well_founded );

registration
cluster non empty trivial -> non empty Noetherian RelStr ;
coherence
for b1 being non empty RelStr holds
( b1 is trivial implies b1 is Noetherian )
proof
let c1 be non empty RelStr ;
assume E2: for b1, b2 being Element of c1 holds b1 = b2 ; :: according to REALSET2:def 7
set c2 = the InternalRel of c1;
let c3 be set ; :: according to REWRITE1:def 16,ABCMIZ_0:def 1
assume E3: c3 c= field the InternalRel of c1 ;
assume c3 <> {} ;
then reconsider c4 = c3 as non empty set ;
consider c5 being Element of c4;
take c5 ;
thus E4: c5 in c3 ;
let c6 be set ;
assume c6 in c3 ;
then ( c5 in field the InternalRel of c1 & c6 in field the InternalRel of c1 & field the InternalRel of c1 c= the carrier of c1 \/ the carrier of c1 ) by E3, E4, RELSET_1:19;
hence not ( not c5 = c6 & [c5,c6] in the InternalRel of c1 ) by E2;
end;
end;

definition
let c1 be non empty RelStr ;
redefine attr a1 is Noetherian means :Def2: :: ABCMIZ_0:def 2
for b1 being non empty Subset of a1 holds
ex b2 being Element of a1 st
( b2 in b1 & ( for b3 being Element of a1 holds
not ( b3 in b1 & b2 < b3 ) ) );
compatibility
( c1 is Noetherian iff for b1 being non empty Subset of c1 holds
ex b2 being Element of c1 st
( b2 in b1 & ( for b3 being Element of c1 holds
not ( b3 in b1 & b2 < b3 ) ) ) )
proof
set c2 = the InternalRel of c1;
thus ( c1 is Noetherian implies for b1 being non empty Subset of c1 holds
ex b2 being Element of c1 st
( b2 in b1 & ( for b3 being Element of c1 holds
not ( b3 in b1 & b2 < b3 ) ) ) )
proof
assume E2: for b1 being set holds
not ( b1 c= field the InternalRel of c1 & b1 <> {} & ( for b2 being set holds
not ( b2 in b1 & ( for b3 being set holds
not ( b3 in b1 & b2 <> b3 & [b2,b3] in the InternalRel of c1 ) ) ) ) ) ; :: according to REWRITE1:def 16,ABCMIZ_0:def 1
let c3 be non empty Subset of c1;
consider c4 being Element of c3;
reconsider c5 = c4 as Element of c1 ;
set c6 = c3 /\ (field the InternalRel of c1);
per cases not ( not c3 misses field the InternalRel of c1 & not c3 meets field the InternalRel of c1 ) ;
suppose E3: c3 misses field the InternalRel of c1 ;
take c5 ;
thus c5 in c3 ;
let c7 be Element of c1;
assume ( c7 in c3 & c5 < c7 ) ;
then c5 <= c7 by ORDERS_2:def 10;
then [c5,c7] in the InternalRel of c1 by ORDERS_2:def 9;
then c5 in field the InternalRel of c1 by RELAT_1:30;
hence not verum by E3, XBOOLE_0:3;
end;
suppose c3 meets field the InternalRel of c1 ;
then ( c3 /\ (field the InternalRel of c1) c= field the InternalRel of c1 & c3 /\ (field the InternalRel of c1) <> {} ) by XBOOLE_0:def 7, XBOOLE_1:17;
then consider c7 being set such that
E3: c7 in c3 /\ (field the InternalRel of c1) and
E4: for b1 being set holds
not ( b1 in c3 /\ (field the InternalRel of c1) & c7 <> b1 & [c7,b1] in the InternalRel of c1 ) by E2;
c7 in c3 by E3, XBOOLE_0:def 3;
then reconsider c8 = c7 as Element of c1 ;
take c8 ;
thus c8 in c3 by E3, XBOOLE_0:def 3;
let c9 be Element of c1;
assume E5: ( c9 in c3 & c8 < c9 ) ;
then ( c8 <= c9 & c8 <> c9 ) by ORDERS_2:def 10;
then E6: [c8,c9] in the InternalRel of c1 by ORDERS_2:def 9;
then c9 in field the InternalRel of c1 by RELAT_1:30;
then c9 in c3 /\ (field the InternalRel of c1) by E5, XBOOLE_0:def 3;
hence not verum by E4, E5, E6;
end;
end;
end;
assume E2: for b1 being non empty Subset of c1 holds
ex b2 being Element of c1 st
( b2 in b1 & ( for b3 being Element of c1 holds
not ( b3 in b1 & b2 < b3 ) ) ) ;
let c3 be set ; :: according to REWRITE1:def 16,ABCMIZ_0:def 1
assume E3: ( c3 c= field the InternalRel of c1 & c3 <> {} ) ;
field the InternalRel of c1 c= the carrier of c1 \/ the carrier of c1 by RELSET_1:19;
then reconsider c4 = c3 as non empty Subset of c1 by E3, XBOOLE_1:1;
consider c5 being Element of c1 such that
E4: c5 in c4 and
E5: for b1 being Element of c1 holds
not ( b1 in c4 & c5 < b1 ) by E2;
take c5 ;
thus c5 in c3 by E4;
let c6 be set ;
assume E6: ( c6 in c3 & c5 <> c6 ) ;
then c6 in c4 ;
then reconsider c7 = c6 as Element of c1 ;
not c5 < c7 by E5, E6;
then not c5 <= c7 by E6, ORDERS_2:def 10;
hence not [c5,c6] in the InternalRel of c1 by ORDERS_2:def 9;
end;
end;

:: deftheorem Def2 defines Noetherian ABCMIZ_0:def 2 :
for b1 being non empty RelStr holds
( b1 is Noetherian iff for b2 being non empty Subset of b1 holds
ex b3 being Element of b1 st
( b3 in b2 & ( for b4 being Element of b1 holds
not ( b4 in b2 & b3 < b4 ) ) ) );

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

:: deftheorem Def3 defines Mizar-widening-like ABCMIZ_0:def 3 :
for b1 being Poset holds
( b1 is Mizar-widening-like iff ( b1 is sup-Semilattice & b1 is Noetherian ) );

registration
cluster Mizar-widening-like -> with_suprema upper-bounded Noetherian RelStr ;
coherence
for b1 being Poset holds
( b1 is Mizar-widening-like implies ( b1 is Noetherian & b1 is with_suprema & b1 is upper-bounded ) )
proof
let c1 be Poset;
assume E3: ( c1 is sup-Semilattice & c1 is Noetherian ) ; :: according to ABCMIZ_0:def 3
hence ( c1 is Noetherian & c1 is with_suprema ) ;
reconsider c2 = c1 as sup-Semilattice by E3;
the carrier of c2 c= the carrier of c2 ;
then consider c3 being Element of c1 such that
c3 in the carrier of c1 and
E4: for b1 being Element of c1 holds
not ( b1 in the carrier of c1 & c3 < b1 ) by E3, Def2;
take c3 ; :: according to YELLOW_0:def 5
let c4 be Element of c1; :: according to LATTICE3:def 9
c3 "\/" c4 in the carrier of c2 ;
then ( c3 "\/" c4 >= c3 & not c3 < c3 "\/" c4 ) by E4, YELLOW_0:22;
then c3 "\/" c4 = c3 by ORDERS_2:def 10;
hence not ( c4 in the carrier of c1 & not c4 <= c3 ) by E3, YELLOW_0:22;
end;
end;

registration
cluster Noetherian -> upper-bounded Noetherian Mizar-widening-like RelStr ;
coherence
for b1 being sup-Semilattice holds
( b1 is Noetherian implies b1 is Mizar-widening-like )
proof
let c1 be sup-Semilattice;
assume E3: c1 is Noetherian ;
thus c1 is sup-Semilattice ; :: according to ABCMIZ_0:def 3
thus c1 is Noetherian by E3;
end;
end;

registration
cluster complete Noetherian Mizar-widening-like RelStr ;
existence
ex b1 being complete sup-Semilattice st b1 is Mizar-widening-like
proof
consider c1 being trivial LATTICE;
take c1 ;
thus c1 is sup-Semilattice ; :: according to ABCMIZ_0:def 3
thus c1 is Noetherian ;
end;
end;

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

theorem Th1: :: ABCMIZ_0:1
for b1 being Noetherian sup-Semilattice
for b2 being Ideal of b1 holds
( ex_sup_of b2,b1 & sup b2 in b2 )
proof
let c1 be Noetherian sup-Semilattice;
let c2 be Ideal of c1;
consider c3 being Element of c1 such that
E4: c3 in c2 and
E5: for b1 being Element of c1 holds
not ( b1 in c2 & c3 < b1 ) by Def2;
E6: c2 is_<=_than c3
proof
let c4 be Element of c1; :: according to LATTICE3:def 9
assume c4 in c2 ;
then c3 "\/" c4 in c2 by E4, WAYBEL_0:40;
then ( c3 <= c3 "\/" c4 & not c3 < c3 "\/" c4 ) by E5, YELLOW_0:22;
then c3 = c3 "\/" c4 by ORDERS_2:def 10;
hence c4 <= c3 by YELLOW_0:22;
end;
for b1 being Element of c1 holds
( c2 is_<=_than b1 implies c3 <= b1 ) by E4, LATTICE3:def 9;
hence ( ex_sup_of c2,c1 & sup c2 in c2 ) by E4, E6, YELLOW_0:30;
end;

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

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

:: deftheorem Def4 defines void ABCMIZ_0:def 4 :
for b1 being AdjectiveStr holds
( b1 is void iff the adjectives of b1 is empty );

theorem Th2: :: ABCMIZ_0:2
for b1, b2 being AdjectiveStr holds
( the adjectives of b1 = the adjectives of b2 & b1 is void implies b2 is void )
proof
let c1, c2 be AdjectiveStr ;
assume E5: the adjectives of c1 = the adjectives of c2 ;
assume the adjectives of c1 is empty ; :: according to ABCMIZ_0:def 4
hence the adjectives of c2 is empty by E5; :: according to ABCMIZ_0:def 4
end;

definition
let c1 be AdjectiveStr ;
let c2 be Element of the adjectives of c1;
func non- c2 -> adjective of a1 equals :: ABCMIZ_0:def 5
the non-op of a1 . a2;
coherence
the non-op of c1 . c2 is adjective of c1
proof
per cases not ( not the adjectives of c1 is empty & the adjectives of c1 is empty ) ;
suppose the adjectives of c1 is empty ;
then ( c2 = {} & not c2 in the adjectives of c1 & dom the non-op of c1 = the adjectives of c1 ) by FUNCT_2:67, SUBSET_1:def 2;
hence the non-op of c1 . c2 is adjective of c1 by FUNCT_1:def 4;
end;
suppose not the adjectives of c1 is empty ;
hence the non-op of c1 . c2 is adjective of c1 by FUNCT_2:7;
end;
end;
end;
end;

:: deftheorem Def5 defines non- ABCMIZ_0:def 5 :
for b1 being AdjectiveStr
for b2 being Element of the adjectives of b1 holds non- b2 = the non-op of b1 . b2;

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

definition
let c1 be AdjectiveStr ;
attr a1 is involutive means :Def6: :: ABCMIZ_0:def 6
for b1 being adjective of a1 holds non- (non- b1) = b1;
attr a1 is without_fixpoints means :: ABCMIZ_0:def 7
for b1 being adjective of a1 holds
not non- b1 = b1;
end;

:: deftheorem Def6 defines involutive ABCMIZ_0:def 6 :
for b1 being AdjectiveStr holds
( b1 is involutive iff for b2 being adjective of b1 holds non- (non- b2) = b2 );

:: deftheorem Def7 defines without_fixpoints ABCMIZ_0:def 7 :
for b1 being AdjectiveStr holds
( b1 is without_fixpoints iff for b2 being adjective of b1 holds
not non- b2 = b2 );

theorem Th4: :: ABCMIZ_0:4
for b1, b2 being set holds
( b1 <> b2 implies for b3 being AdjectiveStr holds
( the adjectives of b3 = {b1,b2} & the non-op of b3 . b1 = b2 & the non-op of b3 . b2 = b1 implies ( not b3 is void & b3 is involutive & b3 is without_fixpoints ) ) )
proof
let c1, c2 be set ;
assume E7: c1 <> c2 ;
let c3 be AdjectiveStr ;
assume that
E8: the adjectives of c3 = {c1,c2} and
E9: the non-op of c3 . c1 = c2 and
E10: the non-op of c3 . c2 = c1 ;
thus not the adjectives of c3 is empty by E8; :: according to ABCMIZ_0:def 4
hereby :: according to ABCMIZ_0:def 6
let c4 be adjective of c3;
E11: ( c4 = c1 or c4 = c2 ) by E8, TARSKI:def 2;
thus non- (non- c4) = the non-op of c3 . (non- c4)
.= c4 by E9, E10, E11 ;
end;
let c4 be adjective of c3; :: according to ABCMIZ_0:def 7
E11: ( c4 = c1 or c4 = c2 ) by E8, TARSKI:def 2;
assume non- c4 = c4 ;
hence not verum by E7, E9, E10, E11;
end;

theorem Th5: :: ABCMIZ_0:5
for b1, b2 being AdjectiveStr holds
( AdjectiveStr(# the adjectives of b1,the non-op of b1 #) = AdjectiveStr(# the adjectives of b2,the non-op of b2 #) & b1 is involutive implies b2 is involutive )
proof
let c1, c2 be AdjectiveStr ;
assume E8: AdjectiveStr(# the adjectives of c1,the non-op of c1 #) = AdjectiveStr(# the adjectives of c2,the non-op of c2 #) ;
assume E9: for b1 being adjective of c1 holds non- (non- b1) = b1 ; :: according to ABCMIZ_0:def 6
let c3 be adjective of c2; :: according to ABCMIZ_0:def 6
reconsider c4 = c3 as adjective of c1 by E8;
thus non- (non- c3) = non- (non- c4) by E8
.= c3 by E9 ;
end;

theorem Th6: :: ABCMIZ_0:6
for b1, b2 being AdjectiveStr holds
( AdjectiveStr(# the adjectives of b1,the non-op of b1 #) = AdjectiveStr(# the adjectives of b2,the non-op of b2 #) & b1 is without_fixpoints implies b2 is without_fixpoints )
proof
let c1, c2 be AdjectiveStr ;
assume E9: AdjectiveStr(# the adjectives of c1,the non-op of c1 #) = AdjectiveStr(# the adjectives of c2,the non-op of c2 #) ;
assume E10: for b1 being adjective of c1 holds
not non- b1 = b1 ; :: according to ABCMIZ_0:def 7
given c3 being adjective of c2 such that E11: non- c3 = c3 ; :: according to ABCMIZ_0:def 7
reconsider c4 = c3 as adjective of c1 by E9;
non- c4 = c4 by E9, E11;
hence not verum by E10;
end;

registration
cluster strict non void involutive without_fixpoints AdjectiveStr ;
existence
ex b1 being strict AdjectiveStr st
( not b1 is void & b1 is involutive & b1 is without_fixpoints )
proof
reconsider c1 = 0, c2 = 1 as Element of {0,1} by TARSKI:def 2;
reconsider c3 = 0,1 --> c2,c1 as UnOp of {0,1} ;
take AdjectiveStr(# {0,1},c3 #) ;
( 0 <> 1 & c3 . c1 = c2 & c3 . c2 = c1 ) by FUNCT_4:66;
hence ( not AdjectiveStr(# {0,1},c3 #) is void & AdjectiveStr(# {0,1},c3 #) is involutive & AdjectiveStr(# {0,1},c3 #) is without_fixpoints ) by Th4;
end;
end;

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

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

registration
let c1 be non empty set ;
let c2 be set ;
let c3 be Relation of c1;
let c4 be UnOp of c2;
let c5 be Function of c1, Fin c2;
cluster TA-structure(# a1,a2,a3,a4,a5 #) -> non empty ;
coherence
not TA-structure(# c1,c2,c3,c4,c5 #) is empty by STRUCT_0:def 1;
end;

registration
let c1 be set ;
let c2 be non empty set ;
let c3 be Relation of c1;
let c4 be UnOp of c2;
let c5 be Function of c1, Fin c2;
cluster TA-structure(# a1,a2,a3,a4,a5 #) -> non void ;
coherence
not TA-structure(# c1,c2,c3,c4,c5 #) is void by Def4;
end;

registration
cluster non empty trivial reflexive complete Noetherian Mizar-widening-like non void involutive without_fixpoints strict TA-structure ;
existence
ex b1 being TA-structure st
( b1 is trivial & b1 is reflexive & not b1 is empty & not b1 is void & b1 is involutive & b1 is without_fixpoints & b1 is strict )
proof
consider c1 being non empty trivial reflexive RelStr , c2 being non void involutive without_fixpoints AdjectiveStr , c3 being Function of the carrier of c1, Fin the adjectives of c2;
take c4 = TA-structure(# the carrier of c1,the adjectives of c2,the InternalRel of c1,the non-op of c2,c3 #);
thus c4 is trivial by TEX_2:4;
RelStr(# the carrier of c1,the InternalRel of c1 #) = RelStr(# the carrier of c4,the InternalRel of c4 #) ;
hence c4 is reflexive by WAYBEL_8:12;
thus ( not c4 is empty & not c4 is void ) ;
AdjectiveStr(# the adjectives of c2,the non-op of c2 #) = AdjectiveStr(# the adjectives of c4,the non-op of c4 #) ;
hence ( c4 is involutive & c4 is without_fixpoints ) by Th5, Th6;
thus c4 is strict ;
end;
end;

definition
let c1 be TA-structure ;
let c2 be Element of c1;
func adjs c2 -> Subset of the adjectives of a1 equals :: ABCMIZ_0:def 8
the adj-map of a1 . a2;
coherence
the adj-map of c1 . c2 is Subset of the adjectives of c1
proof
per cases not ( not the carrier of c1 is empty & the carrier of c1 is empty ) ;
suppose the carrier of c1 is empty ;
then ( c2 = {} & not c2 in the carrier of c1 & dom the adj-map of c1 = the carrier of c1 ) by FUNCT_2:def 1, SUBSET_1:def 2;
then the adj-map of c1 . c2 = {} the adjectives of c1 by FUNCT_1:def 4;
hence the adj-map of c1 . c2 is Subset of the adjectives of c1 ;
end;
suppose not the carrier of c1 is empty ;
then the adj-map of c1 . c2 in Fin the adjectives of c1 by FUNCT_2:7;
hence the adj-map of c1 . c2 is Subset of the adjectives of c1 by FINSUB_1:32;
end;
end;
end;
end;

:: deftheorem Def8 defines adjs ABCMIZ_0:def 8 :
for b1 being TA-structure
for b2 being Element of b1 holds adjs b2 = the adj-map of b1 . b2;

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

definition
let c1 be TA-structure ;
attr a1 is consistent means :Def9: :: ABCMIZ_0:def 9
for b1 being type of a1
for b2 being adjective of a1 holds
not ( b2 in adjs b1 & non- b2 in adjs b1 );
end;

:: deftheorem Def9 defines consistent ABCMIZ_0:def 9 :
for b1 being TA-structure holds
( b1 is consistent iff for b2 being type of b1
for b3 being adjective of b1 holds
not ( b3 in adjs b2 & non- b3 in adjs b2 ) );

theorem Th8: :: ABCMIZ_0:8
for b1, b2 being TA-structure holds
( TA-structure(# the carrier of b1,the adjectives of b1,the InternalRel of b1,the non-op of b1,the adj-map of b1 #) = TA-structure(# the carrier of b2,the adjectives of b2,the InternalRel of b2,the non-op of b2,the adj-map of b2 #) & b1 is consistent implies b2 is consistent )
proof
let c1, c2 be TA-structure ;
assume that
E11: TA-structure(# the carrier of c1,the adjectives of c1,the InternalRel of c1,the non-op of c1,the adj-map of c1 #) = TA-structure(# the carrier of c2,the adjectives of c2,the InternalRel of c2,the non-op of c2,the adj-map of c2 #) and
E12: for b1 being type of c1
for b2 being adjective of c1 holds
not ( b2 in adjs b1 & non- b2 in adjs b1 ) ; :: according to ABCMIZ_0:def 9
let c3 be type of c2; :: according to ABCMIZ_0:def 9
let c4 be adjective of c2;
reconsider c5 = c3 as type of c1 by E11;
reconsider c6 = c4 as adjective of c1 by E11;
assume c4 in adjs c3 ;
then c6 in adjs c5 by E11;
then not non- c6 in adjs c5 by E12;
then ( AdjectiveStr(# the adjectives of c1,the non-op of c1 #) = AdjectiveStr(# the adjectives of c2,the non-op of c2 #) & not non- c6 in adjs c3 ) by E11;
hence not non- c4 in adjs c3 ;
end;

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

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

theorem Th9: :: ABCMIZ_0:9
for b1, b2 being non empty TA-structure holds
( TA-structure(# the carrier of b1,the adjectives of b1,the InternalRel of b1,the non-op of b1,the adj-map of b1 #) = TA-structure(# the carrier of b2,the adjectives of b2,the InternalRel of b2,the non-op of b2,the adj-map of b2 #) & b1 is adj-structured implies b2 is adj-structured )
proof
let c1, c2 be non empty TA-structure ;
assume E12: TA-structure(# the carrier of c1,the adjectives of c1,the InternalRel of c1,the non-op of c1,the adj-map of c1 #) = TA-structure(# the carrier of c2,the adjectives of c2,the InternalRel of c2,the non-op of c2,the adj-map of c2 #) ;
assume the adj-map of c1 is join-preserving Function of c1,((BoolePoset the adjectives of c1) opp ) ; :: according to ABCMIZ_0:def 10
then reconsider c3 = the adj-map of c1 as join-preserving Function of c1,((BoolePoset the adjectives of c1) opp ) ;
reconsider c4 = c3 as Function of c2,((BoolePoset the adjectives of c2) opp ) by E12;
E13: ( RelStr(# the carrier of c1,the InternalRel of c1 #) = RelStr(# the carrier of c2,the InternalRel of c2 #) & RelStr(# the carrier of ((BoolePoset the adjectives of c1) opp ),the InternalRel of ((BoolePoset the adjectives of c1) opp ) #) = RelStr(# the carrier of ((BoolePoset the adjectives of c2) opp ),the InternalRel of ((BoolePoset the adjectives of c2) opp ) #) ) by E12;
c4 is join-preserving
proof
let c5, c6 be type of c2; :: according to WAYBEL_0:def 35
reconsider c7 = c5, c8 = c6 as type of c1 by E12;
assume E14: ex_sup_of {c5,c6},c2 ; :: according to WAYBEL_0:def 31
then E15: ( ex_sup_of {c7,c8},c1 & c3 preserves_sup_of {c7,c8} ) by E13, WAYBEL_0:def 35, YELLOW_0:14;
then E16: ( ex_sup_of c3 .: {c7,c8},(BoolePoset the adjectives of c1) opp & sup (c3 .: {c7,c8}) = c3 . (sup {c7,c8}) ) by WAYBEL_0:def 31;
thus ex_sup_of c4 .: {c5,c6},(BoolePoset the adjectives of c2) opp by E12, E15, WAYBEL_0:def 31;
thus sup (c4 .: {c5,c6}) = c4 . (sup {c5,c6}) by E13, E14, E16, YELLOW_0:26;
end;
hence the adj-map of c2 is join-preserving Function of c2,((BoolePoset the adjectives of c2) opp ) by E12; :: according to ABCMIZ_0:def 10
end;

definition
let c1 be reflexive transitive antisymmetric with_suprema TA-structure ;
redefine attr a1 is adj-structured means :Def11: :: ABCMIZ_0:def 11
for b1, b2 being type of a1 holds adjs (b1 "\/" b2) = (adjs b1) /\ (adjs b2);
compatibility
( c1 is adj-structured iff for b1, b2 being type of c1 holds adjs (b1 "\/" b2) = (adjs b1) /\ (adjs b2) )
proof
thus ( c1 is adj-structured implies for b1, b2 being type of c1 holds adjs (b1 "\/" b2) = (adjs b1) /\ (adjs b2) )
proof
assume the adj-map of c1 is join-preserving Function of c1,((BoolePoset the adjectives of c1) opp ) ; :: according to ABCMIZ_0:def 10
then reconsider c2 = the adj-map of c1 as join-preserving Function of c1,((BoolePoset the adjectives of c1) opp ) ;
let c3, c4 be type of c1;
thus adjs (c3 "\/" c4) = c2 . (c3 "\/" c4)
.= (c2 . c3) "\/" (c2 . c4) by WAYBEL_6:2
.= (~ (c2 . c3)) "/\" (~ (c2 . c4)) by YELLOW_7:22
.= (~ (c2 . c3)) /\ (~ (c2 . c4)) by YELLOW_1:17
.= (c2 . c3) /\ (~ (c2 . c4))
.= (c2 . c3) /\ (c2 . c4)
.= (adjs c3) /\ (c2 . c4)
.= (adjs c3) /\ (adjs c4) ;
end;
assume E12: for b1, b2 being type of c1 holds adjs (b1 "\/" b2) = (adjs b1) /\ (adjs b2) ;
BoolePoset the adjectives of c1 = InclPoset (bool the adjectives of c1) by YELLOW_1:4
.= RelStr(# (bool the adjectives of c1),(RelIncl (bool the adjectives of c1)) #) by YELLOW_1:def 1 ;
then E13: (BoolePoset the adjectives of c1) opp = RelStr(# (bool the adjectives of c1),((RelIncl (bool the adjectives of c1)) ~ ) #) ;
( rng the adj-map of c1 c= Fin the adjectives of c1 & Fin the adjectives of c1 c= bool the adjectives of c1 ) by FINSUB_1:26;
then ( rng the adj-map of c1 c= the carrier of ((BoolePoset the adjectives of c1) opp ) & dom the adj-map of c1 = the carrier of c1 ) by E13, FUNCT_2:def 1, XBOOLE_1:1;
then reconsider c2 = the adj-map of c1 as Function of c1,((BoolePoset the adjectives of c1) opp ) by FUNCT_2:4;
now
let c3, c4 be type of c1;
thus c2 . (c3 "\/" c4) = adjs (c3 "\/" c4)
.= (adjs c3) /\ (adjs c4) by E12
.= (c2 . c3) /\ (adjs c4)
.= (c2 . c3) /\ (c2 . c4)
.= (~ (c2 . c3)) /\ (c2 . c4)
.= (~ (c2 . c3)) /\ (~ (c2 . c4))
.= (~ (c2 . c3)) "/\" (~ (c2 . c4)) by YELLOW_1:17
.= (c2 . c3) "\/" (c2 . c4) by YELLOW_7:22 ;
end;
hence the adj-map of c1 is join-preserving Function of c1,((BoolePoset the adjectives of c1) opp ) by WAYBEL_6:2; :: according to ABCMIZ_0:def 10
end;
end;

:: deftheorem Def11 defines adj-structured ABCMIZ_0:def 11 :
for b1 being reflexive transitive antisymmetric with_suprema TA-structure holds
( b1 is adj-structured iff for b2, b3 being type of b1 holds adjs (b2 "\/" b3) = (adjs b2) /\ (adjs b3) );

theorem Th10: :: ABCMIZ_0:10
for b1 being reflexive transitive antisymmetric with_suprema TA-structure holds
( b1 is adj-structured implies for b2, b3 being type of b1 holds
( b2 <= b3 implies adjs b3 c= adjs b2 ) )
proof
let c1 be reflexive transitive antisymmetric with_suprema TA-structure ;
assume E14: for b1, b2 being type of c1 holds adjs (b1 "\/" b2) = (adjs b1) /\ (adjs b2) ; :: according to ABCMIZ_0:def 11
let c2, c3 be type of c1;
assume c2 <= c3 ;
then c2 "\/" c3 = c3 by YELLOW_0:24;
then adjs c3 = (adjs c2) /\ (adjs c3) by E14;
hence adjs c3 c= adjs c2 by XBOOLE_1:17;
end;

definition
let c1 be TA-structure ;
let c2 be Element of the adjectives of c1;
func types c2 -> Subset of a1 means :Def12: :: ABCMIZ_0:def 12
for b1 being set holds
( b1 in a3 iff ex b2 being type of a1 st
( b1 = b2 & a2 in adjs b2 ) );
existence
ex b1 being Subset of c1 st
for b2 being set holds
( b2 in b1 iff ex b3 being type of c1 st
( b2 = b3 & c2 in adjs b3 ) )
proof
defpred S1[ set ] means ex b1 being type of c1 st
( a1 = b1 & c2 in adjs b1 );
consider c3 being set such that
E14: for b1 being set holds
( b1 in c3 iff ( b1 in the carrier of c1 & S1[b1] ) ) from XBOOLE_0:sch 1();
 c3 c= the carrier of c1
proof
let c4 be set ; :: according to TARSKI:def 3
thus not ( c4 in c3 & not c4 in the carrier of c1 ) by E14;
end;
then reconsider c4 = c3 as Subset of c1 ;
take c4 ;
let c5 be set ;
thus not ( c5 in c4 & ( for b1 being type of c1 holds
not ( c5 = b1 & c2 in adjs b1 ) ) ) by E14;
given c6 being type of c1 such that E15: ( c5 = c6 & c2 in adjs c6 ) ;
now
assume not c5 in the carrier of c1 ;
then ( the carrier of c1 is empty & dom the adj-map of c1 = the carrier of c1 ) by E15, FUNCT_2:def 1;
then the adj-map of c1 . c6 = {} by FUNCT_1:def 4;
hence not verum by E15;
end;
hence c5 in c4 by E14, E15;
end;
uniqueness
for b1, b2 being Subset of c1 holds
( ( for b3 being set holds
( b3 in b1 iff ex b4 being type of c1 st
( b3 = b4 & c2 in adjs b4 ) ) ) & ( for b3 being set holds
( b3 in b2 iff ex b4 being type of c1 st
( b3 = b4 & c2 in adjs b4 ) ) ) implies b1 = b2 )
proof
defpred S1[ set ] means ex b1 being type of c1 st
( a1 = b1 & c2 in adjs b1 );
let c3, c4 be Subset of c1;
assume that
E14: for b1 being set holds
( b1 in c3 iff S1[b1] ) and
E15: for b1 being set holds
( b1 in c4 iff S1[b1] ) ;
thus c3 = c4 from XBOOLE_0:sch 2(E14, E15);
end;
end;

:: deftheorem Def12 defines types ABCMIZ_0:def 12 :
for b1 being TA-structure
for b2 being Element of the adjectives of b1
for b3 being Subset of b1 holds
( b3 = types b2 iff for b4 being set holds
( b4 in b3 iff ex b5 being type of b1 st
( b4 = b5 & b2 in adjs b5 ) ) );

definition
let c1 be non empty TA-structure ;
let c2 be Subset of the adjectives of c1;
func types</