:: 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 ; :: uses REALSET2:def 7
assume E2: for b1 being Element of c1 holds b1 <= b1 ; :: uses YELLOW_0:def 1
let c2 be set ; :: uses LATTICE3:def 12
consider c3 being Element of c1;
take c3 ;
thus c2 is_<=_than c3
proof
let c4 be Element of c1; :: uses 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 :E1: :: ABCMIZ_0:def 1
the InternalRel of a1 is co-well_founded;
end;

:: deftheorem E1 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 ; :: uses REALSET2:def 7
set c2 = the InternalRel of c1;
let c3 be set ; :: uses 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 ;
means :E2: :: 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 ) ) ) ; :: uses 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 ; :: uses 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 E2 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 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 ) ; :: uses 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, E2;
take c3 ; :: uses YELLOW_0:def 5
let c4 be Element of c1; :: uses 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 ; :: uses 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 ; :: uses 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 E1;
end;

theorem E3: :: ABCMIZ_0:1
for b1 being Noetherian sup-Semilattice
for b2 being Ideal of b1 holds
( ex_sup_of b2,b1 & "\/" b2,b1 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 E2;
E6: c2 is_<=_than c3
proof
let c4 be Element of c1; :: uses 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 & "\/" c2,c1 in c2 ) by E4, E6, YELLOW_0:30;
end;

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

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

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

theorem :: 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 ; :: uses ABCMIZ_0:def 4
hence the adjectives of c2 is empty by E5; :: uses ABCMIZ_0:def 4
end;

definition
let c1 be AdjectiveStr ;
let c2 be Element of the adjectives of c1;
func non- a2 -> 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 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 :: 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 ) )
proof
let c1, c2 be AdjectiveStr ;
assume E5: AdjectiveStr the adjectives of c1,the non-op of c1 = AdjectiveStr the adjectives of c2,the non-op of c2 ;
let c3 be adjective of c1;
let c4 be adjective of c2;
assume c3 = c4 ;
hence non- c3 = the non-op of c1 . c4
.= non- c4 by E5 ;

end;

definition
let c1 be AdjectiveStr ;
attr a1 is involutive means :E5: :: 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 E5 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 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 E6: :: 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; :: uses ABCMIZ_0:def 4
hereby :: uses 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; :: uses 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 E7: :: 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 ; :: uses ABCMIZ_0:def 6
let c3 be adjective of c2; :: uses ABCMIZ_0:def 6
reconsider c4 = c3 as adjective of c1 by E8;
non- c3 = non- c4 by E8;
hence non- (non- c3) = non- (non- c4) by E8
.= c3 by E9 ;

end;

theorem E8: :: 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 ; :: uses ABCMIZ_0:def 7
given c3 being adjective of c2 such that E11: non- c3 = c3 ; :: uses 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 E6;
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 E4;
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 a1 -> 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 E4;
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 E7, E8;
thus c4 is strict ;
end;
end;

definition
let c1 be TA-structure ;
let c2 be Element of c1;
func adjs a2 -> 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 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 :: 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 ) )
proof
let c1, c2 be TA-structure ;
assume E9: 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 ;
let c3 be type of c1;
let c4 be type of c2;
( adjs c3 = the adj-map of c1 . c3 & adjs c4 = the adj-map of c2 . c4 ) ;
hence ( c3 = c4 implies adjs c3 = adjs c4 ) by E9;
end;

definition
let c1 be TA-structure ;
attr a1 is consistent means :E9: :: 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 E9 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 E10: :: 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 ) ; :: uses ABCMIZ_0:def 9
let c3 be type of c2; :: uses 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) ~ );
end;

:: deftheorem 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) ~ ) );

theorem E11: :: 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) ~ ) ; :: uses ABCMIZ_0:def 10
then reconsider c3 = the adj-map of c1 as join-preserving Function of c1,((BoolePoset the adjectives of c1) ~ ) ;
reconsider c4 = c3 as Function of c2,((BoolePoset the adjectives of c2) ~ ) 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) ~ ),the InternalRel of ((BoolePoset the adjectives of c1) ~ ) = RelStr the carrier of ((BoolePoset the adjectives of c2) ~ ),the InternalRel of ((BoolePoset the adjectives of c2) ~ ) ) by E12;
c4 is join-preserving
proof
let c5, c6 be type of c2; :: uses WAYBEL_0:def 35
reconsider c7 = c5, c8 = c6 as type of c1 by E12;
assume E14: ex_sup_of {c5,c6},c2 ; :: uses 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) ~ & "\/" (c3 .: {c7,c8}),((BoolePoset the adjectives of c1) ~ ) = c3 . ("\/" {c7,c8},c1) ) by WAYBEL_0:def 31;
thus ex_sup_of c4 .: {c5,c6},(BoolePoset the adjectives of c2) ~ by E12, E15, WAYBEL_0:def 31;
thus "\/" (c4 .: {c5,c6}),((BoolePoset the adjectives of c2) ~ ) = c4 . ("\/" {c5,c6},c2) 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) ~ ) by E12; :: uses ABCMIZ_0:def 10
end;

definition
let c1 be reflexive transitive antisymmetric with_suprema TA-structure ;
means :E12: :: 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) ~ ) ; :: uses ABCMIZ_0:def 10
then reconsider c2 = the adj-map of c1 as join-preserving Function of c1,((BoolePoset the adjectives of c1) ~ ) ;
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) ~ = 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, RELSET_1:12;
then ( rng the adj-map of c1 c= the carrier of ((BoolePoset the adjectives of c1) ~ ) & 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) ~ ) 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) ~ ) by WAYBEL_6:2; :: uses ABCMIZ_0:def 10
end;
end;

:: deftheorem E12 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 E13: :: 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) ; :: uses 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 a2 -> Subset of a1 means :E14: :: 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 ; :: uses 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 E14 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 a2 -> Subset of a1 means :E15: :: ABCMIZ_0:def 13
for b1 being type of a1 holds
( b1 in a3 iff for b2 being adjective of a1 holds
( b2 in a2 implies b1 in types b2 ) );
existence
ex b1 being Subset of c1 st
for b2 being type of c1 holds
( b2 in b1 iff for b3 being adjective of c1 holds
( b3 in c2 implies b2 in types b3 ) )
proof
defpred S1[ set ] means for b1 being adjective of c1 holds
( b1 in c2 implies a1 in types b1 );
consider c3 being set such that
E15: 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 ; :: uses TARSKI:def 3
thus not ( c4 in c3 & not c4 in the carrier of c1 ) by E15;
end;
then reconsider c4 = c3 as Subset of c1 ;
take c4 ;
thus for b1 being type of c1 holds
( b1 in c4 iff for b2 being adjective of c1 holds
( b2 in c2 implies b1 in types b2 ) ) by E15;
end;
uniqueness
for b1, b2 being Subset of c1 holds
( ( for b3 being type of c1 holds
( b3 in b1 iff for b4 being adjective of c1 holds
( b4 in c2 implies b3 in types b4 ) ) & for b3 being type of c1 holds
( b3 in b2 iff for b4 being adjective of c1 holds
( b4 in c2 implies b3 in types b4 ) ) ) implies ( b1 = b2 ) )
proof
let c3, c4 be Subset of c1;
assume that E15: for b1 being type of c1 holds
( b1 in c3 iff for b2 being adjective of c1 holds
( b2 in c2 implies b1 in types b2 ) )
and E16: for b1 being type of c1 holds
( b1 in c4 iff for b2 being adjective of c1 holds
( b2 in c2 implies b1 in types b2 ) ) ;
now
let c5 be set ;
( c5 in c3 iff ( c5 is type of c1 & for b1 being adjective of c1 holds
( b1 in c2 implies c5 in types b1 ) ) ) by E15;
hence ( c5 in c3 iff c5 in c4 ) by E16;
end;
hence c3 = c4 by TARSKI:2;
end;
end;

:: deftheorem E15 defines types ABCMIZ_0:def 13 :
for b1 being non empty TA-structure
for b2 being Subset of the adjectives of b1
for b3 being Subset of b1 holds
( b3 = types b2 iff for b4 being type of b1 holds
( b4 in b3 iff for b5 being adjective of b1 holds
( b5 in b2 implies b4 in types b5 ) ) );

theorem E16: :: ABCMIZ_0:11
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 =