:: WAYBEL_7 semantic presentation

begin

theorem :: WAYBEL_7:1
for L being ( ( reflexive transitive antisymmetric with_suprema with_infima complete ) ( non empty reflexive transitive antisymmetric lower-bounded upper-bounded bounded up-complete /\-complete non void with_suprema with_infima complete ) LATTICE)
for X, Y being ( ( ) ( ) set ) st X : ( ( ) ( ) set ) c= Y : ( ( ) ( ) set ) holds
( "\/" (X : ( ( ) ( ) set ) ,L : ( ( reflexive transitive antisymmetric with_suprema with_infima complete ) ( non empty reflexive transitive antisymmetric lower-bounded upper-bounded bounded up-complete /\-complete non void with_suprema with_infima complete ) LATTICE) ) : ( ( ) ( ) Element of the carrier of b1 : ( ( reflexive transitive antisymmetric with_suprema with_infima complete ) ( non empty reflexive transitive antisymmetric lower-bounded upper-bounded bounded up-complete /\-complete non void with_suprema with_infima complete ) LATTICE) : ( ( ) ( non empty ) set ) ) <= "\/" (Y : ( ( ) ( ) set ) ,L : ( ( reflexive transitive antisymmetric with_suprema with_infima complete ) ( non empty reflexive transitive antisymmetric lower-bounded upper-bounded bounded up-complete /\-complete non void with_suprema with_infima complete ) LATTICE) ) : ( ( ) ( ) Element of the carrier of b1 : ( ( reflexive transitive antisymmetric with_suprema with_infima complete ) ( non empty reflexive transitive antisymmetric lower-bounded upper-bounded bounded up-complete /\-complete non void with_suprema with_infima complete ) LATTICE) : ( ( ) ( non empty ) set ) ) & "/\" (X : ( ( ) ( ) set ) ,L : ( ( reflexive transitive antisymmetric with_suprema with_infima complete ) ( non empty reflexive transitive antisymmetric lower-bounded upper-bounded bounded up-complete /\-complete non void with_suprema with_infima complete ) LATTICE) ) : ( ( ) ( ) Element of the carrier of b1 : ( ( reflexive transitive antisymmetric with_suprema with_infima complete ) ( non empty reflexive transitive antisymmetric lower-bounded upper-bounded bounded up-complete /\-complete non void with_suprema with_infima complete ) LATTICE) : ( ( ) ( non empty ) set ) ) >= "/\" (Y : ( ( ) ( ) set ) ,L : ( ( reflexive transitive antisymmetric with_suprema with_infima complete ) ( non empty reflexive transitive antisymmetric lower-bounded upper-bounded bounded up-complete /\-complete non void with_suprema with_infima complete ) LATTICE) ) : ( ( ) ( ) Element of the carrier of b1 : ( ( reflexive transitive antisymmetric with_suprema with_infima complete ) ( non empty reflexive transitive antisymmetric lower-bounded upper-bounded bounded up-complete /\-complete non void with_suprema with_infima complete ) LATTICE) : ( ( ) ( non empty ) set ) ) ) ;

theorem :: WAYBEL_7:2
for X being ( ( ) ( ) set ) holds the carrier of (BoolePoset X : ( ( ) ( ) set ) ) : ( ( strict ) ( non empty strict reflexive transitive antisymmetric lower-bounded upper-bounded bounded up-complete /\-complete distributive V134() complemented Boolean non void with_suprema with_infima complete ) RelStr ) : ( ( ) ( non empty ) set ) = bool X : ( ( ) ( ) set ) : ( ( ) ( non empty ) Element of bool (bool b1 : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ;

theorem :: WAYBEL_7:3
for L being ( ( non empty antisymmetric bounded ) ( non empty antisymmetric lower-bounded upper-bounded bounded ) RelStr ) holds
( L : ( ( non empty antisymmetric bounded ) ( non empty antisymmetric lower-bounded upper-bounded bounded ) RelStr ) is trivial iff Top L : ( ( non empty antisymmetric bounded ) ( non empty antisymmetric lower-bounded upper-bounded bounded ) RelStr ) : ( ( ) ( ) Element of the carrier of b1 : ( ( non empty antisymmetric bounded ) ( non empty antisymmetric lower-bounded upper-bounded bounded ) RelStr ) : ( ( ) ( non empty ) set ) ) = Bottom L : ( ( non empty antisymmetric bounded ) ( non empty antisymmetric lower-bounded upper-bounded bounded ) RelStr ) : ( ( ) ( ) Element of the carrier of b1 : ( ( non empty antisymmetric bounded ) ( non empty antisymmetric lower-bounded upper-bounded bounded ) RelStr ) : ( ( ) ( non empty ) set ) ) ) ;

registration
let X be ( ( ) ( ) set ) ;
cluster BoolePoset X : ( ( ) ( ) set ) : ( ( strict ) ( non empty strict reflexive transitive antisymmetric lower-bounded upper-bounded bounded up-complete /\-complete distributive V134() complemented Boolean non void with_suprema with_infima complete ) RelStr ) -> strict Boolean ;
end;

registration
let X be ( ( non empty ) ( non empty ) set ) ;
cluster BoolePoset X : ( ( non empty ) ( non empty ) set ) : ( ( strict ) ( non empty strict reflexive transitive antisymmetric lower-bounded upper-bounded bounded up-complete /\-complete distributive V134() complemented Boolean non void with_suprema with_infima complete ) RelStr ) -> non trivial strict ;
end;

theorem :: WAYBEL_7:4
for L being ( ( non empty reflexive transitive antisymmetric lower-bounded ) ( non empty reflexive transitive antisymmetric lower-bounded non void ) Poset)
for F being ( ( non empty filtered upper ) ( non empty filtered upper ) Filter of L : ( ( non empty reflexive transitive antisymmetric lower-bounded ) ( non empty reflexive transitive antisymmetric lower-bounded non void ) Poset) ) holds
( F : ( ( non empty filtered upper ) ( non empty filtered upper ) Filter of b1 : ( ( non empty reflexive transitive antisymmetric lower-bounded ) ( non empty reflexive transitive antisymmetric lower-bounded non void ) Poset) ) is proper iff not Bottom L : ( ( non empty reflexive transitive antisymmetric lower-bounded ) ( non empty reflexive transitive antisymmetric lower-bounded non void ) Poset) : ( ( ) ( ) Element of the carrier of b1 : ( ( non empty reflexive transitive antisymmetric lower-bounded ) ( non empty reflexive transitive antisymmetric lower-bounded non void ) Poset) : ( ( ) ( non empty ) set ) ) in F : ( ( non empty filtered upper ) ( non empty filtered upper ) Filter of b1 : ( ( non empty reflexive transitive antisymmetric lower-bounded ) ( non empty reflexive transitive antisymmetric lower-bounded non void ) Poset) ) ) ;

registration
cluster non empty non trivial strict reflexive transitive antisymmetric Boolean non void with_suprema with_infima for ( ( ) ( ) RelStr ) ;
end;

registration
let L be ( ( non trivial reflexive transitive antisymmetric upper-bounded ) ( non empty non trivial reflexive transitive antisymmetric upper-bounded non void ) Poset) ;
cluster non empty proper filtered upper for ( ( ) ( ) Element of bool the carrier of L : ( ( non trivial reflexive transitive antisymmetric upper-bounded ) ( non empty non trivial reflexive transitive antisymmetric upper-bounded non void ) RelStr ) : ( ( ) ( non empty non trivial ) set ) : ( ( ) ( non empty ) set ) ) ;
end;

theorem :: WAYBEL_7:5
for X being ( ( ) ( ) set )
for a being ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) holds 'not' a : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) : ( ( ) ( ) Element of the carrier of (BoolePoset b1 : ( ( ) ( ) set ) ) : ( ( strict ) ( non empty strict reflexive transitive antisymmetric lower-bounded upper-bounded bounded up-complete /\-complete distributive V134() complemented Boolean non void with_suprema with_infima complete ) RelStr ) : ( ( ) ( non empty ) set ) ) = X : ( ( ) ( ) set ) \ a : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) : ( ( ) ( ) Element of bool b1 : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ;

theorem :: WAYBEL_7:6
for X being ( ( ) ( ) set )
for Y being ( ( ) ( ) Subset of ) holds
( Y : ( ( ) ( ) Subset of ) is lower iff for x, y being ( ( ) ( ) set ) st x : ( ( ) ( ) set ) c= y : ( ( ) ( ) set ) & y : ( ( ) ( ) set ) in Y : ( ( ) ( ) Subset of ) holds
x : ( ( ) ( ) set ) in Y : ( ( ) ( ) Subset of ) ) ;

theorem :: WAYBEL_7:7
for X being ( ( ) ( ) set )
for Y being ( ( ) ( ) Subset of ) holds
( Y : ( ( ) ( ) Subset of ) is upper iff for x, y being ( ( ) ( ) set ) st x : ( ( ) ( ) set ) c= y : ( ( ) ( ) set ) & y : ( ( ) ( ) set ) c= X : ( ( ) ( ) set ) & x : ( ( ) ( ) set ) in Y : ( ( ) ( ) Subset of ) holds
y : ( ( ) ( ) set ) in Y : ( ( ) ( ) Subset of ) ) ;

theorem :: WAYBEL_7:8
for X being ( ( ) ( ) set )
for Y being ( ( lower ) ( lower ) Subset of ) holds
( Y : ( ( lower ) ( lower ) Subset of ) is directed iff for x, y being ( ( ) ( ) set ) st x : ( ( ) ( ) set ) in Y : ( ( lower ) ( lower ) Subset of ) & y : ( ( ) ( ) set ) in Y : ( ( lower ) ( lower ) Subset of ) holds
x : ( ( ) ( ) set ) \/ y : ( ( ) ( ) set ) : ( ( ) ( ) set ) in Y : ( ( lower ) ( lower ) Subset of ) ) ;

theorem :: WAYBEL_7:9
for X being ( ( ) ( ) set )
for Y being ( ( upper ) ( upper ) Subset of ) holds
( Y : ( ( upper ) ( upper ) Subset of ) is filtered iff for x, y being ( ( ) ( ) set ) st x : ( ( ) ( ) set ) in Y : ( ( upper ) ( upper ) Subset of ) & y : ( ( ) ( ) set ) in Y : ( ( upper ) ( upper ) Subset of ) holds
x : ( ( ) ( ) set ) /\ y : ( ( ) ( ) set ) : ( ( ) ( ) set ) in Y : ( ( upper ) ( upper ) Subset of ) ) ;

theorem :: WAYBEL_7:10
for X being ( ( ) ( ) set )
for Y being ( ( non empty lower ) ( non empty lower ) Subset of ) holds
( Y : ( ( non empty lower ) ( non empty lower ) Subset of ) is directed iff for Z being ( ( finite ) ( finite ) Subset-Family of ) st Z : ( ( finite ) ( finite ) Subset-Family of ) c= Y : ( ( non empty lower ) ( non empty lower ) Subset of ) holds
union Z : ( ( finite ) ( finite ) Subset-Family of ) : ( ( ) ( ) Element of bool b1 : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) in Y : ( ( non empty lower ) ( non empty lower ) Subset of ) ) ;

theorem :: WAYBEL_7:11
for X being ( ( ) ( ) set )
for Y being ( ( non empty upper ) ( non empty upper ) Subset of ) holds
( Y : ( ( non empty upper ) ( non empty upper ) Subset of ) is filtered iff for Z being ( ( finite ) ( finite ) Subset-Family of ) st Z : ( ( finite ) ( finite ) Subset-Family of ) c= Y : ( ( non empty upper ) ( non empty upper ) Subset of ) holds
Intersect Z : ( ( finite ) ( finite ) Subset-Family of ) : ( ( ) ( ) Element of bool b1 : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) in Y : ( ( non empty upper ) ( non empty upper ) Subset of ) ) ;

begin

definition
let L be ( ( reflexive transitive antisymmetric with_infima ) ( non empty reflexive transitive antisymmetric non void with_infima ) Poset) ;
let I be ( ( non empty directed lower ) ( non empty directed lower ) Ideal of L : ( ( reflexive transitive antisymmetric with_infima ) ( non empty reflexive transitive antisymmetric non void with_infima ) Poset) ) ;
attr I is prime means :: WAYBEL_7:def 1
 for x, y being ( ( ) ( ) Element of ( ( ) ( non empty non trivial ) set ) ) holds
( not x : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) "/\" y : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) : ( ( ) ( ) Element of the carrier of L : ( ( non trivial reflexive transitive antisymmetric upper-bounded ) ( non empty non trivial reflexive transitive antisymmetric upper-bounded non void ) RelStr ) : ( ( ) ( non empty non trivial ) set ) ) in I : ( ( ) ( ) set ) or x : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) in I : ( ( ) ( ) set ) or y : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) in I : ( ( ) ( ) set ) );
end;

theorem :: WAYBEL_7:12
for L being ( ( reflexive transitive antisymmetric with_infima ) ( non empty reflexive transitive antisymmetric non void with_infima ) Poset)
for I being ( ( non empty directed lower ) ( non empty directed lower ) Ideal of L : ( ( reflexive transitive antisymmetric with_infima ) ( non empty reflexive transitive antisymmetric non void with_infima ) Poset) ) holds
( I : ( ( non empty directed lower ) ( non empty directed lower ) Ideal of b1 : ( ( reflexive transitive antisymmetric with_infima ) ( non empty reflexive transitive antisymmetric non void with_infima ) Poset) ) is prime iff for A being ( ( non empty finite ) ( non empty finite ) Subset of ) st inf A : ( ( non empty finite ) ( non empty finite ) Subset of ) : ( ( ) ( ) Element of the carrier of b1 : ( ( reflexive transitive antisymmetric with_infima ) ( non empty reflexive transitive antisymmetric non void with_infima ) Poset) : ( ( ) ( non empty ) set ) ) in I : ( ( non empty directed lower ) ( non empty directed lower ) Ideal of b1 : ( ( reflexive transitive antisymmetric with_infima ) ( non empty reflexive transitive antisymmetric non void with_infima ) Poset) ) holds
ex a being ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) st
( a : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) in A : ( ( non empty finite ) ( non empty finite ) Subset of ) & a : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) in I : ( ( non empty directed lower ) ( non empty directed lower ) Ideal of b1 : ( ( reflexive transitive antisymmetric with_infima ) ( non empty reflexive transitive antisymmetric non void with_infima ) Poset) ) ) ) ;

registration
let L be ( ( reflexive transitive antisymmetric with_suprema with_infima ) ( non empty reflexive transitive antisymmetric non void with_suprema with_infima ) LATTICE) ;
cluster non empty directed lower prime for ( ( ) ( ) Element of bool the carrier of L : ( ( reflexive transitive antisymmetric with_suprema with_infima ) ( non empty reflexive transitive antisymmetric non void with_suprema with_infima ) RelStr ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ;
end;

theorem :: WAYBEL_7:13
for L1, L2 being ( ( reflexive transitive antisymmetric with_suprema with_infima ) ( non empty reflexive transitive antisymmetric non void with_suprema with_infima ) LATTICE) st RelStr(# the carrier of L1 : ( ( reflexive transitive antisymmetric with_suprema with_infima ) ( non empty reflexive transitive antisymmetric non void with_suprema with_infima ) LATTICE) : ( ( ) ( non empty ) set ) , the InternalRel of L1 : ( ( reflexive transitive antisymmetric with_suprema with_infima ) ( non empty reflexive transitive antisymmetric non void with_suprema with_infima ) LATTICE) : ( ( ) ( non empty Relation-like ) Element of bool [: the carrier of b1 : ( ( reflexive transitive antisymmetric with_suprema with_infima ) ( non empty reflexive transitive antisymmetric non void with_suprema with_infima ) LATTICE) : ( ( ) ( non empty ) set ) , the carrier of b1 : ( ( reflexive transitive antisymmetric with_suprema with_infima ) ( non empty reflexive transitive antisymmetric non void with_suprema with_infima ) LATTICE) : ( ( ) ( non empty ) set ) :] : ( ( ) ( non empty Relation-like ) set ) : ( ( ) ( non empty ) set ) ) #) : ( ( strict ) ( strict ) RelStr ) = RelStr(# the carrier of L2 : ( ( reflexive transitive antisymmetric with_suprema with_infima ) ( non empty reflexive transitive antisymmetric non void with_suprema with_infima ) LATTICE) : ( ( ) ( non empty ) set ) , the InternalRel of L2 : ( ( reflexive transitive antisymmetric with_suprema with_infima ) ( non empty reflexive transitive antisymmetric non void with_suprema with_infima ) LATTICE) : ( ( ) ( non empty Relation-like ) Element of bool [: the carrier of b2 : ( ( reflexive transitive antisymmetric with_suprema with_infima ) ( non empty reflexive transitive antisymmetric non void with_suprema with_infima ) LATTICE) : ( ( ) ( non empty ) set ) , the carrier of b2 : ( ( reflexive transitive antisymmetric with_suprema with_infima ) ( non empty reflexive transitive antisymmetric non void with_suprema with_infima ) LATTICE) : ( ( ) ( non empty ) set ) :] : ( ( ) ( non empty Relation-like ) set ) : ( ( ) ( non empty ) set ) ) #) : ( ( strict ) ( strict ) RelStr ) holds
for x being ( ( ) ( ) set ) st x : ( ( ) ( ) set ) is ( ( non empty directed lower prime ) ( non empty directed lower prime ) Ideal of L1 : ( ( reflexive transitive antisymmetric with_suprema with_infima ) ( non empty reflexive transitive antisymmetric non void with_suprema with_infima ) LATTICE) ) holds
x : ( ( ) ( ) set ) is ( ( non empty directed lower prime ) ( non empty directed lower prime ) Ideal of L2 : ( ( reflexive transitive antisymmetric with_suprema with_infima ) ( non empty reflexive transitive antisymmetric non void with_suprema with_infima ) LATTICE) ) ;

definition
let L be ( ( reflexive transitive antisymmetric with_suprema ) ( non empty reflexive transitive antisymmetric non void with_suprema ) Poset) ;
let F be ( ( non empty filtered upper ) ( non empty filtered upper ) Filter of L : ( ( reflexive transitive antisymmetric with_suprema ) ( non empty reflexive transitive antisymmetric non void with_suprema ) Poset) ) ;
attr F is prime means :: WAYBEL_7:def 2
 for x, y being ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) holds
( not x : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) "\/" y : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) : ( ( ) ( ) Element of the carrier of L : ( ( reflexive transitive antisymmetric with_suprema with_infima ) ( non empty reflexive transitive antisymmetric non void with_suprema with_infima ) RelStr ) : ( ( ) ( non empty ) set ) ) in F : ( ( ) ( ) set ) or x : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) in F : ( ( ) ( ) set ) or y : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) in F : ( ( ) ( ) set ) );
end;

theorem :: WAYBEL_7:14
for L being ( ( reflexive transitive antisymmetric with_suprema ) ( non empty reflexive transitive antisymmetric non void with_suprema ) Poset)
for F being ( ( non empty filtered upper ) ( non empty filtered upper ) Filter of L : ( ( reflexive transitive antisymmetric with_suprema ) ( non empty reflexive transitive antisymmetric non void with_suprema ) Poset) ) holds
( F : ( ( non empty filtered upper ) ( non empty filtered upper ) Filter of b1 : ( ( reflexive transitive antisymmetric with_suprema ) ( non empty reflexive transitive antisymmetric non void with_suprema ) Poset) ) is prime iff for A being ( ( non empty finite ) ( non empty finite ) Subset of ) st sup A : ( ( non empty finite ) ( non empty finite ) Subset of ) : ( ( ) ( ) Element of the carrier of b1 : ( ( reflexive transitive antisymmetric with_suprema ) ( non empty reflexive transitive antisymmetric non void with_suprema ) Poset) : ( ( ) ( non empty ) set ) ) in F : ( ( non empty filtered upper ) ( non empty filtered upper ) Filter of b1 : ( ( reflexive transitive antisymmetric with_suprema ) ( non empty reflexive transitive antisymmetric non void with_suprema ) Poset) ) holds
ex a being ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) st
( a : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) in A : ( ( non empty finite ) ( non empty finite ) Subset of ) & a : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) in F : ( ( non empty filtered upper ) ( non empty filtered upper ) Filter of b1 : ( ( reflexive transitive antisymmetric with_suprema ) ( non empty reflexive transitive antisymmetric non void with_suprema ) Poset) ) ) ) ;

registration
let L be ( ( reflexive transitive antisymmetric with_suprema with_infima ) ( non empty reflexive transitive antisymmetric non void with_suprema with_infima ) LATTICE) ;
cluster non empty filtered upper prime for ( ( ) ( ) Element of bool the carrier of L : ( ( reflexive transitive antisymmetric with_suprema with_infima ) ( non empty reflexive transitive antisymmetric non void with_suprema with_infima ) RelStr ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ;
end;

theorem :: WAYBEL_7:15
for L1, L2 being ( ( reflexive transitive antisymmetric with_suprema with_infima ) ( non empty reflexive transitive antisymmetric non void with_suprema with_infima ) LATTICE) st RelStr(# the carrier of L1 : ( ( reflexive transitive antisymmetric with_suprema with_infima ) ( non empty reflexive transitive antisymmetric non void with_suprema with_infima ) LATTICE) : ( ( ) ( non empty ) set ) , the InternalRel of L1 : ( ( reflexive transitive antisymmetric with_suprema with_infima ) ( non empty reflexive transitive antisymmetric non void with_suprema with_infima ) LATTICE) : ( ( ) ( non empty Relation-like ) Element of bool [: the carrier of b1 : ( ( reflexive transitive antisymmetric with_suprema with_infima ) ( non empty reflexive transitive antisymmetric non void with_suprema with_infima ) LATTICE) : ( ( ) ( non empty ) set ) , the carrier of b1 : ( ( reflexive transitive antisymmetric with_suprema with_infima ) ( non empty reflexive transitive antisymmetric non void with_suprema with_infima ) LATTICE) : ( ( ) ( non empty ) set ) :] : ( ( ) ( non empty Relation-like ) set ) : ( ( ) ( non empty ) set ) ) #) : ( ( strict ) ( strict ) RelStr ) = RelStr(# the carrier of L2 : ( ( reflexive transitive antisymmetric with_suprema with_infima ) ( non empty reflexive transitive antisymmetric non void with_suprema with_infima ) LATTICE) : ( ( ) ( non empty ) set ) , the InternalRel of L2 : ( ( reflexive transitive antisymmetric with_suprema with_infima ) ( non empty reflexive transitive antisymmetric non void with_suprema with_infima ) LATTICE) : ( ( ) ( non empty Relation-like ) Element of bool [: the carrier of b2 : ( ( reflexive transitive antisymmetric with_suprema with_infima ) ( non empty reflexive transitive antisymmetric non void with_suprema with_infima ) LATTICE) : ( ( ) ( non empty ) set ) , the carrier of b2 : ( ( reflexive transitive antisymmetric with_suprema with_infima ) ( non empty reflexive transitive antisymmetric non void with_suprema with_infima ) LATTICE) : ( ( ) ( non empty ) set ) :] : ( ( ) ( non empty Relation-like ) set ) : ( ( ) ( non empty ) set ) ) #) : ( ( strict ) ( strict ) RelStr ) holds
for x being ( ( ) ( ) set ) st x : ( ( ) ( ) set ) is ( ( non empty filtered upper prime ) ( non empty filtered upper prime ) Filter of L1 : ( ( reflexive transitive antisymmetric with_suprema with_infima ) ( non empty reflexive transitive antisymmetric non void with_suprema with_infima ) LATTICE) ) holds
x : ( ( ) ( ) set ) is ( ( non empty filtered upper prime ) ( non empty filtered upper prime ) Filter of L2 : ( ( reflexive transitive antisymmetric with_suprema with_infima ) ( non empty reflexive transitive antisymmetric non void with_suprema with_infima ) LATTICE) ) ;

theorem :: WAYBEL_7:16
for L being ( ( reflexive transitive antisymmetric with_suprema with_infima ) ( non empty reflexive transitive antisymmetric non void with_suprema with_infima ) LATTICE)
for x being ( ( ) ( ) set ) holds
( x : ( ( ) ( ) set ) is ( ( non empty directed lower prime ) ( non empty directed lower prime ) Ideal of L : ( ( reflexive transitive antisymmetric with_suprema with_infima ) ( non empty reflexive transitive antisymmetric non void with_suprema with_infima ) LATTICE) ) iff x : ( ( ) ( ) set ) is ( ( non empty filtered upper prime ) ( non empty filtered upper prime ) Filter of L : ( ( reflexive transitive antisymmetric with_suprema with_infima ) ( non empty reflexive transitive antisymmetric non void with_suprema with_infima ) LATTICE) opp : ( ( strict ) ( non empty strict reflexive transitive antisymmetric non void with_suprema with_infima ) RelStr ) ) ) ;

theorem :: WAYBEL_7:17
for L being ( ( reflexive transitive antisymmetric with_suprema with_infima ) ( non empty reflexive transitive antisymmetric non void with_suprema with_infima ) LATTICE)
for x being ( ( ) ( ) set ) holds
( x : ( ( ) ( ) set ) is ( ( non empty filtered upper prime ) ( non empty filtered upper prime ) Filter of L : ( ( reflexive transitive antisymmetric with_suprema with_infima ) ( non empty reflexive transitive antisymmetric non void with_suprema with_infima ) LATTICE) ) iff x : ( ( ) ( ) set ) is ( ( non empty directed lower prime ) ( non empty directed lower prime ) Ideal of L : ( ( reflexive transitive antisymmetric with_suprema with_infima ) ( non empty reflexive transitive antisymmetric non void with_suprema with_infima ) LATTICE) opp : ( ( strict ) ( non empty strict reflexive transitive antisymmetric non void with_suprema with_infima ) RelStr ) ) ) ;

theorem :: WAYBEL_7:18
for L being ( ( reflexive transitive antisymmetric with_infima ) ( non empty reflexive transitive antisymmetric non void with_infima ) Poset)
for I being ( ( non empty directed lower ) ( non empty directed lower ) Ideal of L : ( ( reflexive transitive antisymmetric with_infima ) ( non empty reflexive transitive antisymmetric non void with_infima ) Poset) ) holds
( I : ( ( non empty directed lower ) ( non empty directed lower ) Ideal of b1 : ( ( reflexive transitive antisymmetric with_infima ) ( non empty reflexive transitive antisymmetric non void with_infima ) Poset) ) is prime iff ( I : ( ( non empty directed lower ) ( non empty directed lower ) Ideal of b1 : ( ( reflexive transitive antisymmetric with_infima ) ( non empty reflexive transitive antisymmetric non void with_infima ) Poset) ) ` : ( ( ) ( ) Element of bool the carrier of b1 : ( ( reflexive transitive antisymmetric with_infima ) ( non empty reflexive transitive antisymmetric non void with_infima ) Poset) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) is ( ( non empty filtered upper ) ( non empty filtered upper ) Filter of L : ( ( reflexive transitive antisymmetric with_infima ) ( non empty reflexive transitive antisymmetric non void with_infima ) Poset) ) or I : ( ( non empty directed lower ) ( non empty directed lower ) Ideal of b1 : ( ( reflexive transitive antisymmetric with_infima ) ( non empty reflexive transitive antisymmetric non void with_infima ) Poset) ) ` : ( ( ) ( ) Element of bool the carrier of b1 : ( ( reflexive transitive antisymmetric with_infima ) ( non empty reflexive transitive antisymmetric non void with_infima ) Poset) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) = {} : ( ( ) ( empty Relation-like non-empty empty-yielding finite finite-yielding V35() ) set ) ) ) ;

theorem :: WAYBEL_7:19
for L being ( ( reflexive transitive antisymmetric with_suprema with_infima ) ( non empty reflexive transitive antisymmetric non void with_suprema with_infima ) LATTICE)
for I being ( ( non empty directed lower ) ( non empty directed lower ) Ideal of L : ( ( reflexive transitive antisymmetric with_suprema with_infima ) ( non empty reflexive transitive antisymmetric non void with_suprema with_infima ) LATTICE) ) holds
( I : ( ( non empty directed lower ) ( non empty directed lower ) Ideal of b1 : ( ( reflexive transitive antisymmetric with_suprema with_infima ) ( non empty reflexive transitive antisymmetric non void with_suprema with_infima ) LATTICE) ) is prime iff I : ( ( non empty directed lower ) ( non empty directed lower ) Ideal of b1 : ( ( reflexive transitive antisymmetric with_suprema with_infima ) ( non empty reflexive transitive antisymmetric non void with_suprema with_infima ) LATTICE) ) in PRIME (InclPoset (Ids L : ( ( reflexive transitive antisymmetric with_suprema with_infima ) ( non empty reflexive transitive antisymmetric non void with_suprema with_infima ) LATTICE) ) : ( ( ) ( non empty ) set ) ) : ( ( strict ) ( non empty strict reflexive transitive antisymmetric non void with_suprema with_infima ) RelStr ) : ( ( ) ( ) Element of bool the carrier of (InclPoset (Ids b1 : ( ( reflexive transitive antisymmetric with_suprema with_infima ) ( non empty reflexive transitive antisymmetric non void with_suprema with_infima ) LATTICE) ) : ( ( ) ( non empty ) set ) ) : ( ( strict ) ( non empty strict reflexive transitive antisymmetric non void with_suprema with_infima ) RelStr ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) ;

theorem :: WAYBEL_7:20
for L being ( ( reflexive transitive antisymmetric Boolean with_suprema with_infima ) ( non empty reflexive transitive antisymmetric lower-bounded upper-bounded bounded distributive V134() complemented Boolean non void with_suprema with_infima ) LATTICE)
for F being ( ( non empty filtered upper ) ( non empty filtered upper ) Filter of L : ( ( reflexive transitive antisymmetric Boolean with_suprema with_infima ) ( non empty reflexive transitive antisymmetric lower-bounded upper-bounded bounded distributive V134() complemented Boolean non void with_suprema with_infima ) LATTICE) ) holds
( F : ( ( non empty filtered upper ) ( non empty filtered upper ) Filter of b1 : ( ( reflexive transitive antisymmetric Boolean with_suprema with_infima ) ( non empty reflexive transitive antisymmetric lower-bounded upper-bounded bounded distributive V134() complemented Boolean non void with_suprema with_infima ) LATTICE) ) is prime iff for a being ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) holds
( a : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) in F : ( ( non empty filtered upper ) ( non empty filtered upper ) Filter of b1 : ( ( reflexive transitive antisymmetric Boolean with_suprema with_infima ) ( non empty reflexive transitive antisymmetric lower-bounded upper-bounded bounded distributive V134() complemented Boolean non void with_suprema with_infima ) LATTICE) ) or 'not' a : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) : ( ( ) ( ) Element of the carrier of b1 : ( ( reflexive transitive antisymmetric Boolean with_suprema with_infima ) ( non empty reflexive transitive antisymmetric lower-bounded upper-bounded bounded distributive V134() complemented Boolean non void with_suprema with_infima ) LATTICE) : ( ( ) ( non empty ) set ) ) in F : ( ( non empty filtered upper ) ( non empty filtered upper ) Filter of b1 : ( ( reflexive transitive antisymmetric Boolean with_suprema with_infima ) ( non empty reflexive transitive antisymmetric lower-bounded upper-bounded bounded distributive V134() complemented Boolean non void with_suprema with_infima ) LATTICE) ) ) ) ;

theorem :: WAYBEL_7:21
for X being ( ( ) ( ) set )
for F being ( ( non empty filtered upper ) ( non empty filtered upper ) Filter of BoolePoset X : ( ( ) ( ) set ) : ( ( strict ) ( non empty strict reflexive transitive antisymmetric lower-bounded upper-bounded bounded up-complete /\-complete distributive V134() complemented Boolean non void with_suprema with_infima complete ) RelStr ) ) holds
( F : ( ( non empty filtered upper ) ( non empty filtered upper ) Filter of BoolePoset b1 : ( ( ) ( ) set ) : ( ( strict ) ( non empty strict reflexive transitive antisymmetric lower-bounded upper-bounded bounded up-complete /\-complete distributive V134() complemented Boolean non void with_suprema with_infima complete ) RelStr ) ) is prime iff for A being ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) holds
( A : ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) in F : ( ( non empty filtered upper ) ( non empty filtered upper ) Filter of BoolePoset b1 : ( ( ) ( ) set ) : ( ( strict ) ( non empty strict reflexive transitive antisymmetric lower-bounded upper-bounded bounded up-complete /\-complete distributive V134() complemented Boolean non void with_suprema with_infima complete ) RelStr ) ) or X : ( ( ) ( ) set ) \ A : ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) : ( ( ) ( ) Element of bool b1 : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) in F : ( ( non empty filtered upper ) ( non empty filtered upper ) Filter of BoolePoset b1 : ( ( ) ( ) set ) : ( ( strict ) ( non empty strict reflexive transitive antisymmetric lower-bounded upper-bounded bounded up-complete /\-complete distributive V134() complemented Boolean non void with_suprema with_infima complete ) RelStr ) ) ) ) ;

definition
let L be ( ( non empty reflexive transitive antisymmetric ) ( non empty reflexive transitive antisymmetric non void ) Poset) ;
let F be ( ( non empty filtered upper ) ( non empty filtered upper ) Filter of L : ( ( non empty reflexive transitive antisymmetric ) ( non empty reflexive transitive antisymmetric non void ) Poset) ) ;
attr F is ultra means :: WAYBEL_7:def 3
( F : ( ( ) ( ) set ) is proper & ( for G being ( ( non empty filtered upper ) ( non empty filtered upper ) Filter of L : ( ( reflexive transitive antisymmetric with_suprema with_infima ) ( non empty reflexive transitive antisymmetric non void with_suprema with_infima ) RelStr ) ) holds
( not F : ( ( ) ( ) set ) c= G : ( ( non empty filtered upper ) ( non empty filtered upper ) Filter of L : ( ( non empty reflexive transitive antisymmetric ) ( non empty reflexive transitive antisymmetric non void ) Poset) ) or F : ( ( ) ( ) set ) = G : ( ( non empty filtered upper ) ( non empty filtered upper ) Filter of L : ( ( non empty reflexive transitive antisymmetric ) ( non empty reflexive transitive antisymmetric non void ) Poset) ) or G : ( ( non empty filtered upper ) ( non empty filtered upper ) Filter of L : ( ( non empty reflexive transitive antisymmetric ) ( non empty reflexive transitive antisymmetric non void ) Poset) ) = the carrier of L : ( ( reflexive transitive antisymmetric with_suprema with_infima ) ( non empty reflexive transitive antisymmetric non void with_suprema with_infima ) RelStr ) : ( ( ) ( non empty ) set ) ) ) );
end;

registration
let L be ( ( non empty reflexive transitive antisymmetric ) ( non empty reflexive transitive antisymmetric non void ) Poset) ;
cluster non empty filtered upper ultra -> non empty proper filtered upper for ( ( ) ( ) Element of bool the carrier of L : ( ( reflexive transitive antisymmetric with_suprema with_infima ) ( non empty reflexive transitive antisymmetric non void with_suprema with_infima ) RelStr ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ;
end;

theorem :: WAYBEL_7:22
for L being ( ( reflexive transitive antisymmetric Boolean with_suprema with_infima ) ( non empty reflexive transitive antisymmetric lower-bounded upper-bounded bounded distributive V134() complemented Boolean non void with_suprema with_infima ) LATTICE)
for F being ( ( non empty filtered upper ) ( non empty filtered upper ) Filter of L : ( ( reflexive transitive antisymmetric Boolean with_suprema with_infima ) ( non empty reflexive transitive antisymmetric lower-bounded upper-bounded bounded distributive V134() complemented Boolean non void with_suprema with_infima ) LATTICE) ) holds
( ( F : ( ( non empty filtered upper ) ( non empty filtered upper ) Filter of b1 : ( ( reflexive transitive antisymmetric Boolean with_suprema with_infima ) ( non empty reflexive transitive antisymmetric lower-bounded upper-bounded bounded distributive V134() complemented Boolean non void with_suprema with_infima ) LATTICE) ) is proper & F : ( ( non empty filtered upper ) ( non empty filtered upper ) Filter of b1 : ( ( reflexive transitive antisymmetric Boolean with_suprema with_infima ) ( non empty reflexive transitive antisymmetric lower-bounded upper-bounded bounded distributive V134() complemented Boolean non void with_suprema with_infima ) LATTICE) ) is prime ) iff F : ( ( non empty filtered upper ) ( non empty filtered upper ) Filter of b1 : ( ( reflexive transitive antisymmetric Boolean with_suprema with_infima ) ( non empty reflexive transitive antisymmetric lower-bounded upper-bounded bounded distributive V134() complemented Boolean non void with_suprema with_infima ) LATTICE) ) is ultra ) ;

theorem :: WAYBEL_7:23
for L being ( ( reflexive transitive antisymmetric distributive with_suprema with_infima ) ( non empty reflexive transitive antisymmetric distributive non void with_suprema with_infima ) LATTICE)
for I being ( ( non empty directed lower ) ( non empty directed lower ) Ideal of L : ( ( reflexive transitive antisymmetric distributive with_suprema with_infima ) ( non empty reflexive transitive antisymmetric distributive non void with_suprema with_infima ) LATTICE) )
for F being ( ( non empty filtered upper ) ( non empty filtered upper ) Filter of L : ( ( reflexive transitive antisymmetric distributive with_suprema with_infima ) ( non empty reflexive transitive antisymmetric distributive non void with_suprema with_infima ) LATTICE) ) st I : ( ( non empty directed lower ) ( non empty directed lower ) Ideal of b1 : ( ( reflexive transitive antisymmetric distributive with_suprema with_infima ) ( non empty reflexive transitive antisymmetric distributive non void with_suprema with_infima ) LATTICE) ) misses F : ( ( non empty filtered upper ) ( non empty filtered upper ) Filter of b1 : ( ( reflexive transitive antisymmetric distributive with_suprema with_infima ) ( non empty reflexive transitive antisymmetric distributive non void with_suprema with_infima ) LATTICE) ) holds
ex P being ( ( non empty directed lower ) ( non empty directed lower ) Ideal of L : ( ( reflexive transitive antisymmetric distributive with_suprema with_infima ) ( non empty reflexive transitive antisymmetric distributive non void with_suprema with_infima ) LATTICE) ) st
( P : ( ( non empty directed lower ) ( non empty directed lower ) Ideal of b1 : ( ( reflexive transitive antisymmetric distributive with_suprema with_infima ) ( non empty reflexive transitive antisymmetric distributive non void with_suprema with_infima ) LATTICE) ) is prime & I : ( ( non empty directed lower ) ( non empty directed lower ) Ideal of b1 : ( ( reflexive transitive antisymmetric distributive with_suprema with_infima ) ( non empty reflexive transitive antisymmetric distributive non void with_suprema with_infima ) LATTICE) ) c= P : ( ( non empty directed lower ) ( non empty directed lower ) Ideal of b1 : ( ( reflexive transitive antisymmetric distributive with_suprema with_infima ) ( non empty reflexive transitive antisymmetric distributive non void with_suprema with_infima ) LATTICE) ) & P : ( ( non empty directed lower ) ( non empty directed lower ) Ideal of b1 : ( ( reflexive transitive antisymmetric distributive with_suprema with_infima ) ( non empty reflexive transitive antisymmetric distributive non void with_suprema with_infima ) LATTICE) ) misses F : ( ( non empty filtered upper ) ( non empty filtered upper ) Filter of b1 : ( ( reflexive transitive antisymmetric distributive with_suprema with_infima ) ( non empty reflexive transitive antisymmetric distributive non void with_suprema with_infima ) LATTICE) ) ) ;

theorem :: WAYBEL_7:24
for L being ( ( reflexive transitive antisymmetric distributive with_suprema with_infima ) ( non empty reflexive transitive antisymmetric distributive non void with_suprema with_infima ) LATTICE)
for I being ( ( non empty directed lower ) ( non empty directed lower ) Ideal of L : ( ( reflexive transitive antisymmetric distributive with_suprema with_infima ) ( non empty reflexive transitive antisymmetric distributive non void with_suprema with_infima ) LATTICE) )
for x being ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) st not x : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) in I : ( ( non empty directed lower ) ( non empty directed lower ) Ideal of b1 : ( ( reflexive transitive antisymmetric distributive with_suprema with_infima ) ( non empty reflexive transitive antisymmetric distributive non void with_suprema with_infima ) LATTICE) ) holds
ex P being ( ( non empty directed lower ) ( non empty directed lower ) Ideal of L : ( ( reflexive transitive antisymmetric distributive with_suprema with_infima ) ( non empty reflexive transitive antisymmetric distributive non void with_suprema with_infima ) LATTICE) ) st
( P : ( ( non empty directed lower ) ( non empty directed lower ) Ideal of b1 : ( ( reflexive transitive antisymmetric distributive with_suprema with_infima ) ( non empty reflexive transitive antisymmetric distributive non void with_suprema with_infima ) LATTICE) ) is prime & I : ( ( non empty directed lower ) ( non empty directed lower ) Ideal of b1 : ( ( reflexive transitive antisymmetric distributive with_suprema with_infima ) ( non empty reflexive transitive antisymmetric distributive non void with_suprema with_infima ) LATTICE) ) c= P : ( ( non empty directed lower ) ( non empty directed lower ) Ideal of b1 : ( ( reflexive transitive antisymmetric distributive with_suprema with_infima ) ( non empty reflexive transitive antisymmetric distributive non void with_suprema with_infima ) LATTICE) ) & not x : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) in P : ( ( non empty directed lower ) ( non empty directed lower ) Ideal of b1 : ( ( reflexive transitive antisymmetric distributive with_suprema with_infima ) ( non empty reflexive transitive antisymmetric distributive non void with_suprema with_infima ) LATTICE) ) ) ;

theorem :: WAYBEL_7:25
for L being ( ( reflexive transitive antisymmetric distributive with_suprema with_infima ) ( non empty reflexive transitive antisymmetric distributive non void with_suprema with_infima ) LATTICE)
for I being ( ( non empty directed lower ) ( non empty directed lower ) Ideal of L : ( ( reflexive transitive antisymmetric distributive with_suprema with_infima ) ( non empty reflexive transitive antisymmetric distributive non void with_suprema with_infima ) LATTICE) )
for F being ( ( non empty filtered upper ) ( non empty filtered upper ) Filter of L : ( ( reflexive transitive antisymmetric distributive with_suprema with_infima ) ( non empty reflexive transitive antisymmetric distributive non void with_suprema with_infima ) LATTICE) ) st I : ( ( non empty directed lower ) ( non empty directed lower ) Ideal of b1 : ( ( reflexive transitive antisymmetric distributive with_suprema with_infima ) ( non empty reflexive transitive antisymmetric distributive non void with_suprema with_infima ) LATTICE) ) misses F : ( ( non empty filtered upper ) ( non empty filtered upper ) Filter of b1 : ( ( reflexive transitive antisymmetric distributive with_suprema with_infima ) ( non empty reflexive transitive antisymmetric distributive non void with_suprema with_infima ) LATTICE) ) holds
ex P being ( ( non empty filtered upper ) ( non empty filtered upper ) Filter of L : ( ( reflexive transitive antisymmetric distributive with_suprema with_infima ) ( non empty reflexive transitive antisymmetric distributive non void with_suprema with_infima ) LATTICE) ) st
( P : ( ( non empty filtered upper ) ( non empty filtered upper ) Filter of b1 : ( ( reflexive transitive antisymmetric distributive with_suprema with_infima ) ( non empty reflexive transitive antisymmetric distributive non void with_suprema with_infima ) LATTICE) ) is prime & F : ( ( non empty filtered upper ) ( non empty filtered upper ) Filter of b1 : ( ( reflexive transitive antisymmetric distributive with_suprema with_infima ) ( non empty reflexive transitive antisymmetric distributive non void with_suprema with_infima ) LATTICE) ) c= P : ( ( non empty filtered upper ) ( non empty filtered upper ) Filter of b1 : ( ( reflexive transitive antisymmetric distributive with_suprema with_infima ) ( non empty reflexive transitive antisymmetric distributive non void with_suprema with_infima ) LATTICE) ) & I : ( ( non empty directed lower ) ( non empty directed lower ) Ideal of b1 : ( ( reflexive transitive antisymmetric distributive with_suprema with_infima ) ( non empty reflexive transitive antisymmetric distributive non void with_suprema with_infima ) LATTICE) ) misses P : ( ( non empty filtered upper ) ( non empty filtered upper ) Filter of b1 : ( ( reflexive transitive antisymmetric distributive with_suprema with_infima ) ( non empty reflexive transitive antisymmetric distributive non void with_suprema with_infima ) LATTICE) ) ) ;

theorem :: WAYBEL_7:26
for L being ( ( non trivial reflexive transitive antisymmetric Boolean with_suprema with_infima ) ( non empty non trivial reflexive transitive antisymmetric lower-bounded upper-bounded bounded distributive V134() complemented Boolean non void with_suprema with_infima ) LATTICE)
for F being ( ( non empty proper filtered upper ) ( non empty proper filtered upper ) Filter of L : ( ( non trivial reflexive transitive antisymmetric Boolean with_suprema with_infima ) ( non empty non trivial reflexive transitive antisymmetric lower-bounded upper-bounded bounded distributive V134() complemented Boolean non void with_suprema with_infima ) LATTICE) ) ex G being ( ( non empty filtered upper ) ( non empty filtered upper ) Filter of L : ( ( non trivial reflexive transitive antisymmetric Boolean with_suprema with_infima ) ( non empty non trivial reflexive transitive antisymmetric lower-bounded upper-bounded bounded distributive V134() complemented Boolean non void with_suprema with_infima ) LATTICE) ) st
( F : ( ( non empty proper filtered upper ) ( non empty proper filtered upper ) Filter of b1 : ( ( non trivial reflexive transitive antisymmetric Boolean with_suprema with_infima ) ( non empty non trivial reflexive transitive antisymmetric lower-bounded upper-bounded bounded distributive V134() complemented Boolean non void with_suprema with_infima ) LATTICE) ) c= G : ( ( non empty filtered upper ) ( non empty filtered upper ) Filter of b1 : ( ( non trivial reflexive transitive antisymmetric Boolean with_suprema with_infima ) ( non empty non trivial reflexive transitive antisymmetric lower-bounded upper-bounded bounded distributive V134() complemented Boolean non void with_suprema with_infima ) LATTICE) ) & G : ( ( non empty filtered upper ) ( non empty filtered upper ) Filter of b1 : ( ( non trivial reflexive transitive antisymmetric Boolean with_suprema with_infima ) ( non empty non trivial reflexive transitive antisymmetric lower-bounded upper-bounded bounded distributive V134() complemented Boolean non void with_suprema with_infima ) LATTICE) ) is ultra ) ;

begin

definition
let T be ( ( TopSpace-like ) ( TopSpace-like ) TopSpace) ;
let F, x be ( ( ) ( ) set ) ;
pred x is_a_cluster_point_of F,T means :: WAYBEL_7:def 4
 for A being ( ( ) ( ) Subset of ) st A : ( ( ) ( ) Subset of ) is open & x : ( ( ) ( Relation-like ) Element of bool [:F : ( ( ) ( ) set ) ,F : ( ( ) ( ) set ) :] : ( ( ) ( Relation-like ) set ) : ( ( ) ( non empty ) set ) ) in A : ( ( ) ( ) Subset of ) holds
for B being ( ( ) ( ) set ) st B : ( ( ) ( ) set ) in F : ( ( ) ( ) set ) holds
A : ( ( ) ( ) Subset of ) meets B : ( ( ) ( ) set ) ;
pred x is_a_convergence_point_of F,T means :: WAYBEL_7:def 5
 for A being ( ( ) ( ) Subset of ) st A : ( ( ) ( ) Subset of ) is open & x : ( ( ) ( Relation-like ) Element of bool [:F : ( ( ) ( ) set ) ,F : ( ( ) ( ) set ) :] : ( ( ) ( Relation-like ) set ) : ( ( ) ( non empty ) set ) ) in A : ( ( ) ( ) Subset of ) holds
A : ( ( ) ( ) Subset of ) in F : ( ( ) ( ) set ) ;
end;

registration
let X be ( ( non empty ) ( non empty ) set ) ;
cluster non empty filtered upper ultra for ( ( ) ( ) Element of bool the carrier of (BoolePoset X : ( ( non empty ) ( non empty ) set ) ) : ( ( strict ) ( non empty non trivial strict reflexive transitive antisymmetric lower-bounded upper-bounded bounded up-complete /\-complete distributive V134() complemented Boolean non void with_suprema with_infima complete ) RelStr ) : ( ( ) ( non empty non trivial ) set ) : ( ( ) ( non empty ) set ) ) ;
end;

theorem :: WAYBEL_7:27
for T being ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace)
for F being ( ( non empty filtered upper ultra ) ( non empty proper filtered upper ultra ) Filter of BoolePoset the carrier of T : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) : ( ( strict ) ( non empty non trivial strict reflexive transitive antisymmetric lower-bounded upper-bounded bounded up-complete /\-complete distributive V134() complemented Boolean non void with_suprema with_infima complete ) RelStr ) )
for p being ( ( ) ( ) set ) holds
( p : ( ( ) ( ) set ) is_a_cluster_point_of F : ( ( non empty filtered upper ultra ) ( non empty proper filtered upper ultra ) Filter of BoolePoset the carrier of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) : ( ( strict ) ( non empty non trivial strict reflexive transitive antisymmetric lower-bounded upper-bounded bounded up-complete /\-complete distributive V134() complemented Boolean non void with_suprema with_infima complete ) RelStr ) ) ,T : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) iff p : ( ( ) ( ) set ) is_a_convergence_point_of F : ( ( non empty filtered upper ultra ) ( non empty proper filtered upper ultra ) Filter of BoolePoset the carrier of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) : ( ( strict ) ( non empty non trivial strict reflexive transitive antisymmetric lower-bounded upper-bounded bounded up-complete /\-complete distributive V134() complemented Boolean non void with_suprema with_infima complete ) RelStr ) ) ,T : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) ) ;

theorem :: WAYBEL_7:28
for T being ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace)
for x, y being ( ( ) ( ) Element of ( ( ) ( non empty non trivial ) set ) ) st x : ( ( ) ( ) Element of ( ( ) ( non empty non trivial ) set ) ) << y : ( ( ) ( ) Element of ( ( ) ( non empty non trivial ) set ) ) holds
for F being ( ( non empty proper filtered upper ) ( non empty proper filtered upper ) Filter of BoolePoset the carrier of T : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) : ( ( strict ) ( non empty non trivial strict reflexive transitive antisymmetric lower-bounded upper-bounded bounded up-complete /\-complete distributive V134() complemented Boolean non void with_suprema with_infima complete ) RelStr ) ) st x : ( ( ) ( ) Element of ( ( ) ( non empty non trivial ) set ) ) in F : ( ( non empty proper filtered upper ) ( non empty proper filtered upper ) Filter of BoolePoset the carrier of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) : ( ( strict ) ( non empty non trivial strict reflexive transitive antisymmetric lower-bounded upper-bounded bounded up-complete /\-complete distributive V134() complemented Boolean non void with_suprema with_infima complete ) RelStr ) ) holds
ex p being ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) st
( p : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) in y : ( ( ) ( ) Element of ( ( ) ( non empty non trivial ) set ) ) & p : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) is_a_cluster_point_of F : ( ( non empty proper filtered upper ) ( non empty proper filtered upper ) Filter of BoolePoset the carrier of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) : ( ( strict ) ( non empty non trivial strict reflexive transitive antisymmetric lower-bounded upper-bounded bounded up-complete /\-complete distributive V134() complemented Boolean non void with_suprema with_infima complete ) RelStr ) ) ,T : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) ) ;

theorem :: WAYBEL_7:29
for T being ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace)
for x, y being ( ( ) ( ) Element of ( ( ) ( non empty non trivial ) set ) ) st x : ( ( ) ( ) Element of ( ( ) ( non empty non trivial ) set ) ) << y : ( ( ) ( ) Element of ( ( ) ( non empty non trivial ) set ) ) holds
for F being ( ( non empty filtered upper ultra ) ( non empty proper filtered upper ultra ) Filter of BoolePoset the carrier of T : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) : ( ( strict ) ( non empty non trivial strict reflexive transitive antisymmetric lower-bounded upper-bounded bounded up-complete /\-complete distributive V134() complemented Boolean non void with_suprema with_infima complete ) RelStr ) ) st x : ( ( ) ( ) Element of ( ( ) ( non empty non trivial ) set ) ) in F : ( ( non empty filtered upper ultra ) ( non empty proper filtered upper ultra ) Filter of BoolePoset the carrier of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) : ( ( strict ) ( non empty non trivial strict reflexive transitive antisymmetric lower-bounded upper-bounded bounded up-complete /\-complete distributive V134() complemented Boolean non void with_suprema with_infima complete ) RelStr ) ) holds
ex p being ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) st
( p : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) in y : ( ( ) ( ) Element of ( ( ) ( non empty non trivial ) set ) ) & p : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) is_a_convergence_point_of F : ( ( non empty filtered upper ultra ) ( non empty proper filtered upper ultra ) Filter of BoolePoset the carrier of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) : ( ( strict ) ( non empty non trivial strict reflexive transitive antisymmetric lower-bounded upper-bounded bounded up-complete /\-complete distributive V134() complemented Boolean non void with_suprema with_infima complete ) RelStr ) ) ,T : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) ) ;

theorem :: WAYBEL_7:30
for T being ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace)
for x, y being ( ( ) ( ) Element of ( ( ) ( non empty non trivial ) set ) ) st x : ( ( ) ( ) Element of ( ( ) ( non empty non trivial ) set ) ) c= y : ( ( ) ( ) Element of ( ( ) ( non empty non trivial ) set ) ) & ( for F being ( ( non empty filtered upper ultra ) ( non empty proper filtered upper ultra ) Filter of BoolePoset the carrier of T : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) : ( ( strict ) ( non empty non trivial strict reflexive transitive antisymmetric lower-bounded upper-bounded bounded up-complete /\-complete distributive V134() complemented Boolean non void with_suprema with_infima complete ) RelStr ) ) st x : ( ( ) ( ) Element of ( ( ) ( non empty non trivial ) set ) ) in F : ( ( non empty filtered upper ultra ) ( non empty proper filtered upper ultra ) Filter of BoolePoset the carrier of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) : ( ( strict ) ( non empty non trivial strict reflexive transitive antisymmetric lower-bounded upper-bounded bounded up-complete /\-complete distributive V134() complemented Boolean non void with_suprema with_infima complete ) RelStr ) ) holds
ex p being ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) st
( p : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) in y : ( ( ) ( ) Element of ( ( ) ( non empty non trivial ) set ) ) & p : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) is_a_convergence_point_of F : ( ( non empty filtered upper ultra ) ( non empty proper filtered upper ultra ) Filter of BoolePoset the carrier of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) : ( ( strict ) ( non empty non trivial strict reflexive transitive antisymmetric lower-bounded upper-bounded bounded up-complete /\-complete distributive V134() complemented Boolean non void with_suprema with_infima complete ) RelStr ) ) ,T : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) ) ) holds
x : ( ( ) ( ) Element of ( ( ) ( non empty non trivial ) set ) ) << y : ( ( ) ( ) Element of ( ( ) ( non empty non trivial ) set ) ) ;

theorem :: WAYBEL_7:31
for T being ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace)
for B being ( ( open quasi_prebasis ) ( open quasi_prebasis ) prebasis of T : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) )
for x, y being ( ( ) ( ) Element of ( ( ) ( non empty non trivial ) set ) ) st x : ( ( ) ( ) Element of ( ( ) ( non empty non trivial ) set ) ) c= y : ( ( ) ( ) Element of ( ( ) ( non empty non trivial ) set ) ) holds
( x : ( ( ) ( ) Element of ( ( ) ( non empty non trivial ) set ) ) << y : ( ( ) ( ) Element of ( ( ) ( non empty non trivial ) set ) ) iff for F being ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) st y : ( ( ) ( ) Element of ( ( ) ( non empty non trivial ) set ) ) c= union F : ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) holds
ex G being ( ( finite ) ( finite ) Subset of ( ( ) ( non empty ) set ) ) st x : ( ( ) ( ) Element of ( ( ) ( non empty non trivial ) set ) ) c= union G : ( ( finite ) ( finite ) Subset of ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) ;

theorem :: WAYBEL_7:32
for L being ( ( reflexive transitive antisymmetric distributive with_suprema with_infima complete ) ( non empty reflexive transitive antisymmetric lower-bounded upper-bounded bounded up-complete /\-complete distributive non void with_suprema with_infima complete ) LATTICE)
for x, y being ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) holds
( x : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) << y : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) iff for P being ( ( non empty directed lower prime ) ( non empty directed lower prime ) Ideal of L : ( ( reflexive transitive antisymmetric distributive with_suprema with_infima complete ) ( non empty reflexive transitive antisymmetric lower-bounded upper-bounded bounded up-complete /\-complete distributive non void with_suprema with_infima complete ) LATTICE) ) st y : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) <= sup P : ( ( non empty directed lower prime ) ( non empty directed lower prime ) Ideal of b1 : ( ( reflexive transitive antisymmetric distributive with_suprema with_infima complete ) ( non empty reflexive transitive antisymmetric lower-bounded upper-bounded bounded up-complete /\-complete distributive non void with_suprema with_infima complete ) LATTICE) ) : ( ( ) ( ) Element of the carrier of b1 : ( ( reflexive transitive antisymmetric distributive with_suprema with_infima complete ) ( non empty reflexive transitive antisymmetric lower-bounded upper-bounded bounded up-complete /\-complete distributive non void with_suprema with_infima complete ) LATTICE) : ( ( ) ( non empty ) set ) ) holds
x : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) in P : ( ( non empty directed lower prime ) ( non empty directed lower prime ) Ideal of b1 : ( ( reflexive transitive antisymmetric distributive with_suprema with_infima complete ) ( non empty reflexive transitive antisymmetric lower-bounded upper-bounded bounded up-complete /\-complete distributive non void with_suprema with_infima complete ) LATTICE) ) ) ;

theorem :: WAYBEL_7:33
for L being ( ( reflexive transitive antisymmetric with_suprema with_infima ) ( non empty reflexive transitive antisymmetric non void with_suprema with_infima ) LATTICE)
for p being ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) st p : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) is prime holds
downarrow p : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty directed lower ) Element of bool the carrier of b1 : ( ( reflexive transitive antisymmetric with_suprema with_infima ) ( non empty reflexive transitive antisymmetric non void with_suprema with_infima ) LATTICE) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) is prime ;

begin

definition
let L be ( ( reflexive transitive antisymmetric with_suprema with_infima ) ( non empty reflexive transitive antisymmetric non void with_suprema with_infima ) LATTICE) ;
let p be ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ;
attr p is pseudoprime means :: WAYBEL_7:def 6
 ex P being ( ( non empty directed lower prime ) ( non empty directed lower prime ) Ideal of L : ( ( non empty ) ( non empty ) set ) ) st p : ( ( ) ( ) set ) = sup P : ( ( non empty directed lower prime ) ( non empty directed lower prime ) Ideal of L : ( ( reflexive transitive antisymmetric with_suprema with_infima ) ( non empty reflexive transitive antisymmetric non void with_suprema with_infima ) LATTICE) ) : ( ( ) ( ) Element of the carrier of L : ( ( non empty ) ( non empty ) set ) : ( ( ) ( ) set ) ) ;
end;

theorem :: WAYBEL_7:34
for L being ( ( reflexive transitive antisymmetric with_suprema with_infima ) ( non empty reflexive transitive antisymmetric non void with_suprema with_infima ) LATTICE)
for p being ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) st p : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) is prime holds
p : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) is pseudoprime ;

theorem :: WAYBEL_7:35
for L being ( ( reflexive transitive antisymmetric with_suprema with_infima continuous ) ( non empty reflexive transitive antisymmetric upper-bounded up-complete non void with_suprema with_infima satisfying_axiom_of_approximation continuous ) LATTICE)
for p being ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) st p : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) is pseudoprime holds
for A being ( ( non empty finite ) ( non empty finite ) Subset of ) st inf A : ( ( non empty finite ) ( non empty finite ) Subset of ) : ( ( ) ( ) Element of the carrier of b1 : ( ( reflexive transitive antisymmetric with_suprema with_infima continuous ) ( non empty reflexive transitive antisymmetric upper-bounded up-complete non void with_suprema with_infima satisfying_axiom_of_approximation continuous ) LATTICE) : ( ( ) ( non empty ) set ) ) << p : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) holds
ex a being ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) st
( a : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) in A : ( ( non empty finite ) ( non empty finite ) Subset of ) & a : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) <= p : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ) ;

theorem :: WAYBEL_7:36
for L being ( ( reflexive transitive antisymmetric with_suprema with_infima continuous ) ( non empty reflexive transitive antisymmetric upper-bounded up-complete non void with_suprema with_infima satisfying_axiom_of_approximation continuous ) LATTICE)
for p being ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) st ( p : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) <> Top L : ( ( reflexive transitive antisymmetric with_suprema with_infima continuous ) ( non empty reflexive transitive antisymmetric upper-bounded up-complete non void with_suprema with_infima satisfying_axiom_of_approximation continuous ) LATTICE) : ( ( ) ( ) Element of the carrier of b1 : ( ( reflexive transitive antisymmetric with_suprema with_infima continuous ) ( non empty reflexive transitive antisymmetric upper-bounded up-complete non void with_suprema with_infima satisfying_axiom_of_approximation continuous ) LATTICE) : ( ( ) ( non empty ) set ) ) or not Top L : ( ( reflexive transitive antisymmetric with_suprema with_infima continuous ) ( non empty reflexive transitive antisymmetric upper-bounded up-complete non void with_suprema with_infima satisfying_axiom_of_approximation continuous ) LATTICE) : ( ( ) ( ) Element of the carrier of b1 : ( ( reflexive transitive antisymmetric with_suprema with_infima continuous ) ( non empty reflexive transitive antisymmetric upper-bounded up-complete non void with_suprema with_infima satisfying_axiom_of_approximation continuous ) LATTICE) : ( ( ) ( non empty ) set ) ) is compact ) & ( for A being ( ( non empty finite ) ( non empty finite ) Subset of ) st inf A : ( ( non empty finite ) ( non empty finite ) Subset of ) : ( ( ) ( ) Element of the carrier of b1 : ( ( reflexive transitive antisymmetric with_suprema with_infima continuous ) ( non empty reflexive transitive antisymmetric upper-bounded up-complete non void with_suprema with_infima satisfying_axiom_of_approximation continuous ) LATTICE) : ( ( ) ( non empty ) set ) ) << p : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) holds
ex a being ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) st
( a : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) in A : ( ( non empty finite ) ( non empty finite ) Subset of ) & a : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) <= p : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ) ) holds
uparrow (fininfs ((downarrow p : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ) : ( ( ) ( non empty directed lower ) Element of bool the carrier of b1 : ( ( reflexive transitive antisymmetric with_suprema with_infima continuous ) ( non empty reflexive transitive antisymmetric upper-bounded up-complete non void with_suprema with_infima satisfying_axiom_of_approximation continuous ) LATTICE) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) `) : ( ( ) ( ) Element of bool the carrier of b1 : ( ( reflexive transitive antisymmetric with_suprema with_infima continuous ) ( non empty reflexive transitive antisymmetric upper-bounded up-complete non void with_suprema with_infima satisfying_axiom_of_approximation continuous ) LATTICE) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) : ( ( ) ( non empty filtered ) Element of bool the carrier of b1 : ( ( reflexive transitive antisymmetric with_suprema with_infima continuous ) ( non empty reflexive transitive antisymmetric upper-bounded up-complete non void with_suprema with_infima satisfying_axiom_of_approximation continuous ) LATTICE) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty filtered upper ) Element of bool the carrier of b1 : ( ( reflexive transitive antisymmetric with_suprema with_infima continuous ) ( non empty reflexive transitive antisymmetric upper-bounded up-complete non void with_suprema with_infima satisfying_axiom_of_approximation continuous ) LATTICE) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) misses waybelow p : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty directed lower ) Element of bool the carrier of b1 : ( ( reflexive transitive antisymmetric with_suprema with_infima continuous ) ( non empty reflexive transitive antisymmetric upper-bounded up-complete non void with_suprema with_infima satisfying_axiom_of_approximation continuous ) LATTICE) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ;

theorem :: WAYBEL_7:37
for L being ( ( reflexive transitive antisymmetric with_suprema with_infima continuous ) ( non empty reflexive transitive antisymmetric upper-bounded up-complete non void with_suprema with_infima satisfying_axiom_of_approximation continuous ) LATTICE) st Top L : ( ( reflexive transitive antisymmetric with_suprema with_infima continuous ) ( non empty reflexive transitive antisymmetric upper-bounded up-complete non void with_suprema with_infima satisfying_axiom_of_approximation continuous ) LATTICE) : ( ( ) ( ) Element of the carrier of b1 : ( ( reflexive transitive antisymmetric with_suprema with_infima continuous ) ( non empty reflexive transitive antisymmetric upper-bounded up-complete non void with_suprema with_infima satisfying_axiom_of_approximation continuous ) LATTICE) : ( ( ) ( non empty ) set ) ) is compact holds
( ( for A being ( ( non empty finite ) ( non empty finite ) Subset of ) st inf A : ( ( non empty finite ) ( non empty finite ) Subset of ) : ( ( ) ( ) Element of the carrier of b1 : ( ( reflexive transitive antisymmetric with_suprema with_infima continuous ) ( non empty reflexive transitive antisymmetric upper-bounded up-complete non void with_suprema with_infima satisfying_axiom_of_approximation continuous ) LATTICE) : ( ( ) ( non empty ) set ) ) << Top L : ( ( reflexive transitive antisymmetric with_suprema with_infima continuous ) ( non empty reflexive transitive antisymmetric upper-bounded up-complete non void with_suprema with_infima satisfying_axiom_of_approximation continuous ) LATTICE) : ( ( ) ( ) Element of the carrier of b1 : ( ( reflexive transitive antisymmetric with_suprema with_infima continuous ) ( non empty reflexive transitive antisymmetric upper-bounded up-complete non void with_suprema with_infima satisfying_axiom_of_approximation continuous ) LATTICE) : ( ( ) ( non empty ) set ) ) holds
ex a being ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) st
( a : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) in A : ( ( non empty finite ) ( non empty finite ) Subset of ) & a : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) <= Top L : ( ( reflexive transitive antisymmetric with_suprema with_infima continuous ) ( non empty reflexive transitive antisymmetric upper-bounded up-complete non void with_suprema with_infima satisfying_axiom_of_approximation continuous ) LATTICE) : ( ( ) ( ) Element of the carrier of b1 : ( ( reflexive transitive antisymmetric with_suprema with_infima continuous ) ( non empty reflexive transitive antisymmetric upper-bounded up-complete non void with_suprema with_infima satisfying_axiom_of_approximation continuous ) LATTICE) : ( ( ) ( non empty ) set ) ) ) ) & uparrow (fininfs ((downarrow (Top L : ( ( reflexive transitive antisymmetric with_suprema with_infima continuous ) ( non empty reflexive transitive antisymmetric upper-bounded up-complete non void with_suprema with_infima satisfying_axiom_of_approximation continuous ) LATTICE) ) : ( ( ) ( ) Element of the carrier of b1 : ( ( reflexive transitive antisymmetric with_suprema with_infima continuous ) ( non empty reflexive transitive antisymmetric upper-bounded up-complete non void with_suprema with_infima satisfying_axiom_of_approximation continuous ) LATTICE) : ( ( ) ( non empty ) set ) ) ) : ( ( ) ( non empty directed lower ) Element of bool the carrier of b1 : ( ( reflexive transitive antisymmetric with_suprema with_infima continuous ) ( non empty reflexive transitive antisymmetric upper-bounded up-complete non void with_suprema with_infima satisfying_axiom_of_approximation continuous ) LATTICE) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) `) : ( ( ) ( ) Element of bool the carrier of b1 : ( ( reflexive transitive antisymmetric with_suprema with_infima continuous ) ( non empty reflexive transitive antisymmetric upper-bounded up-complete non void with_suprema with_infima satisfying_axiom_of_approximation continuous ) LATTICE) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) : ( ( ) ( non empty filtered ) Element of bool the carrier of b1 : ( ( reflexive transitive antisymmetric with_suprema with_infima continuous ) ( non empty reflexive transitive antisymmetric upper-bounded up-complete non void with_suprema with_infima satisfying_axiom_of_approximation continuous ) LATTICE) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty filtered upper ) Element of bool the carrier of b1 : ( ( reflexive transitive antisymmetric with_suprema with_infima continuous ) ( non empty reflexive transitive antisymmetric upper-bounded up-complete non void with_suprema with_infima satisfying_axiom_of_approximation continuous ) LATTICE) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) meets waybelow (Top L : ( ( reflexive transitive antisymmetric with_suprema with_infima continuous ) ( non empty reflexive transitive antisymmetric upper-bounded up-complete non void with_suprema with_infima satisfying_axiom_of_approximation continuous ) LATTICE) ) : ( ( ) ( ) Element of the carrier of b1 : ( ( reflexive transitive antisymmetric with_suprema with_infima continuous ) ( non empty reflexive transitive antisymmetric upper-bounded up-complete non void with_suprema with_infima satisfying_axiom_of_approximation continuous ) LATTICE) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty directed lower ) Element of bool the carrier of b1 : ( ( reflexive transitive antisymmetric with_suprema with_infima continuous ) ( non empty reflexive transitive antisymmetric upper-bounded up-complete non void with_suprema with_infima satisfying_axiom_of_approximation continuous ) LATTICE) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) ;

theorem :: WAYBEL_7:38
for L being ( ( reflexive transitive antisymmetric with_suprema with_infima continuous ) ( non empty reflexive transitive antisymmetric upper-bounded up-complete non void with_suprema with_infima satisfying_axiom_of_approximation continuous ) LATTICE)
for p being ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) st uparrow (fininfs ((downarrow p : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ) : ( ( ) ( non empty directed lower ) Element of bool the carrier of b1 : ( ( reflexive transitive antisymmetric with_suprema with_infima continuous ) ( non empty reflexive transitive antisymmetric upper-bounded up-complete non void with_suprema with_infima satisfying_axiom_of_approximation continuous ) LATTICE) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) `) : ( ( ) ( ) Element of bool the carrier of b1 : ( ( reflexive transitive antisymmetric with_suprema with_infima continuous ) ( non empty reflexive transitive antisymmetric upper-bounded up-complete non void with_suprema with_infima satisfying_axiom_of_approximation continuous ) LATTICE) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) : ( ( ) ( non empty filtered ) Element of bool the carrier of b1 : ( ( reflexive transitive antisymmetric with_suprema with_infima continuous ) ( non empty reflexive transitive antisymmetric upper-bounded up-complete non void with_suprema with_infima satisfying_axiom_of_approximation continuous ) LATTICE) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty filtered upper ) Element of bool the carrier of b1 : ( ( reflexive transitive antisymmetric with_suprema with_infima continuous ) ( non empty reflexive transitive antisymmetric upper-bounded up-complete non void with_suprema with_infima satisfying_axiom_of_approximation continuous ) LATTICE) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) misses waybelow p : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty directed lower ) Element of bool the carrier of b1 : ( ( reflexive transitive antisymmetric with_suprema with_infima continuous ) ( non empty reflexive transitive antisymmetric upper-bounded up-complete non void with_suprema with_infima satisfying_axiom_of_approximation continuous ) LATTICE) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) holds
for A being ( ( non empty finite ) ( non empty finite ) Subset of ) st inf A : ( ( non empty finite ) ( non empty finite ) Subset of ) : ( ( ) ( ) Element of the carrier of b1 : ( ( reflexive transitive antisymmetric with_suprema with_infima continuous ) ( non empty reflexive transitive antisymmetric upper-bounded up-complete non void with_suprema with_infima satisfying_axiom_of_approximation continuous ) LATTICE) : ( ( ) ( non empty ) set ) ) << p : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) holds
ex a being ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) st
( a : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) in A : ( ( non empty finite ) ( non empty finite ) Subset of ) & a : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) <= p : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ) ;

theorem :: WAYBEL_7:39
for L being ( ( reflexive transitive antisymmetric distributive with_suprema with_infima continuous ) ( non empty reflexive transitive antisymmetric upper-bounded up-complete distributive non void with_suprema with_infima satisfying_axiom_of_approximation continuous ) LATTICE)
for p being ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) st uparrow (fininfs ((downarrow p : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ) : ( ( ) ( non empty directed lower ) Element of bool the carrier of b1 : ( ( reflexive transitive antisymmetric distributive with_suprema with_infima continuous ) ( non empty reflexive transitive antisymmetric upper-bounded up-complete distributive non void with_suprema with_infima satisfying_axiom_of_approximation continuous ) LATTICE) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) `) : ( ( ) ( ) Element of bool the carrier of b1 : ( ( reflexive transitive antisymmetric distributive with_suprema with_infima continuous ) ( non empty reflexive transitive antisymmetric upper-bounded up-complete distributive non void with_suprema with_infima satisfying_axiom_of_approximation continuous ) LATTICE) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) : ( ( ) ( non empty filtered ) Element of bool the carrier of b1 : ( ( reflexive transitive antisymmetric distributive with_suprema with_infima continuous ) ( non empty reflexive transitive antisymmetric upper-bounded up-complete distributive non void with_suprema with_infima satisfying_axiom_of_approximation continuous ) LATTICE) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty filtered upper ) Element of bool the carrier of b1 : ( ( reflexive transitive antisymmetric distributive with_suprema with_infima continuous ) ( non empty reflexive transitive antisymmetric upper-bounded up-complete distributive non void with_suprema with_infima satisfying_axiom_of_approximation continuous ) LATTICE) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) misses waybelow p : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty directed lower ) Element of bool the carrier of b1 : ( ( reflexive transitive antisymmetric distributive with_suprema with_infima continuous ) ( non empty reflexive transitive antisymmetric upper-bounded up-complete distributive non void with_suprema with_infima satisfying_axiom_of_approximation continuous ) LATTICE) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) holds
p : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) is pseudoprime ;

definition
let L be ( ( non empty ) ( non empty ) RelStr ) ;
let R be ( ( ) ( Relation-like ) Relation of ) ;
attr R is multiplicative means :: WAYBEL_7:def 7
 for a, x, y being ( ( ) ( ) Element of ( ( ) ( ) set ) ) st [a : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ,x : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ] : ( ( ) ( ) Element of the carrier of [:L : ( ( non empty ) ( non empty ) set ) ,L : ( ( non empty ) ( non empty ) set ) :] : ( ( strict ) ( strict ) RelStr ) : ( ( ) ( ) set ) ) in R : ( ( ) ( ) set ) & [a : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ,y : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ] : ( ( ) ( ) Element of the carrier of [:L : ( ( non empty ) ( non empty ) set ) ,L : ( ( non empty ) ( non empty ) set ) :] : ( ( strict ) ( strict ) RelStr ) : ( ( ) ( ) set ) ) in R : ( ( ) ( ) set ) holds
[a : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ,(x : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) "/\" y : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ) Element of the carrier of L : ( ( non empty ) ( non empty ) set ) : ( ( ) ( ) set ) ) ] : ( ( ) ( ) Element of the carrier of [:L : ( ( non empty ) ( non empty ) set ) ,L : ( ( non empty ) ( non empty ) set ) :] : ( ( strict ) ( strict ) RelStr ) : ( ( ) ( ) set ) ) in R : ( ( ) ( ) set ) ;
end;

registration
let L be ( ( reflexive transitive antisymmetric lower-bounded with_suprema ) ( non empty reflexive transitive antisymmetric lower-bounded non void with_suprema ) sup-Semilattice) ;
let R be ( ( auxiliary ) ( Relation-like V82() auxiliary(i) auxiliary(ii) auxiliary(iii) auxiliary(iv) auxiliary ) Relation of ) ;
let x be ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ;
cluster R : ( ( auxiliary ) ( Relation-like V82() auxiliary(i) auxiliary(ii) auxiliary(iii) auxiliary(iv) auxiliary ) Element of bool [: the carrier of L : ( ( reflexive transitive antisymmetric lower-bounded with_suprema ) ( non empty reflexive transitive antisymmetric lower-bounded non void with_suprema ) RelStr ) : ( ( ) ( non empty ) set ) , the carrier of L : ( ( reflexive transitive antisymmetric lower-bounded with_suprema ) ( non empty reflexive transitive antisymmetric lower-bounded non void with_suprema ) RelStr ) : ( ( ) ( non empty ) set ) :] : ( ( ) ( non empty Relation-like ) set ) : ( ( ) ( non empty ) set ) ) -above x : ( ( ) ( ) Element of the carrier of L : ( ( reflexive transitive antisymmetric lower-bounded with_suprema ) ( non empty reflexive transitive antisymmetric lower-bounded non void with_suprema ) RelStr ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) Element of bool the carrier of L : ( ( reflexive transitive antisymmetric lower-bounded with_suprema ) ( non empty reflexive transitive antisymmetric lower-bounded non void with_suprema ) RelStr ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) -> upper ;
end;

theorem :: WAYBEL_7:40
for L being ( ( reflexive transitive antisymmetric lower-bounded with_suprema with_infima ) ( non empty reflexive transitive antisymmetric lower-bounded non void with_suprema with_infima ) LATTICE)
for R being ( ( auxiliary ) ( Relation-like V82() auxiliary(i) auxiliary(ii) auxiliary(iii) auxiliary(iv) auxiliary ) Relation of ) holds
( R : ( ( auxiliary ) ( Relation-like V82() auxiliary(i) auxiliary(ii) auxiliary(iii) auxiliary(iv) auxiliary ) Relation of ) is multiplicative iff for x being ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) holds R : ( ( auxiliary ) ( Relation-like V82() auxiliary(i) auxiliary(ii) auxiliary(iii) auxiliary(iv) auxiliary ) Relation of ) -above x : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) : ( ( ) ( upper ) Element of bool the carrier of b1 : ( ( reflexive transitive antisymmetric lower-bounded with_suprema with_infima ) ( non empty reflexive transitive antisymmetric lower-bounded non void with_suprema with_infima ) LATTICE) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) is filtered ) ;

theorem :: WAYBEL_7:41
for L being ( ( reflexive transitive antisymmetric lower-bounded with_suprema with_infima ) ( non empty reflexive transitive antisymmetric lower-bounded non void with_suprema with_infima ) LATTICE)
for R being ( ( auxiliary ) ( Relation-like V82() auxiliary(i) auxiliary(ii) auxiliary(iii) auxiliary(iv) auxiliary ) Relation of ) holds
( R : ( ( auxiliary ) ( Relation-like V82() auxiliary(i) auxiliary(ii) auxiliary(iii) auxiliary(iv) auxiliary ) Relation of ) is multiplicative iff for a, b, x, y being ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) st [a : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ,x : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ] : ( ( ) ( ) Element of the carrier of [:b1 : ( ( reflexive transitive antisymmetric lower-bounded with_suprema with_infima ) ( non empty reflexive transitive antisymmetric lower-bounded non void with_suprema with_infima ) LATTICE) ,b1 : ( ( reflexive transitive antisymmetric lower-bounded with_suprema with_infima ) ( non empty reflexive transitive antisymmetric lower-bounded non void with_suprema with_infima ) LATTICE) :] : ( ( strict ) ( non empty strict reflexive transitive antisymmetric non void with_suprema with_infima ) RelStr ) : ( ( ) ( non empty ) set ) ) in R : ( ( auxiliary ) ( Relation-like V82() auxiliary(i) auxiliary(ii) auxiliary(iii) auxiliary(iv) auxiliary ) Relation of ) & [b : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ,y : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ] : ( ( ) ( ) Element of the carrier of [:b1 : ( ( reflexive transitive antisymmetric lower-bounded with_suprema with_infima ) ( non empty reflexive transitive antisymmetric lower-bounded non void with_suprema with_infima ) LATTICE) ,b1 : ( ( reflexive transitive antisymmetric lower-bounded with_suprema with_infima ) ( non empty reflexive transitive antisymmetric lower-bounded non void with_suprema with_infima ) LATTICE) :] : ( ( strict ) ( non empty strict reflexive transitive antisymmetric non void with_suprema with_infima ) RelStr ) : ( ( ) ( non empty ) set ) ) in R : ( ( auxiliary ) ( Relation-like V82() auxiliary(i) auxiliary(ii) auxiliary(iii) auxiliary(iv) auxiliary ) Relation of ) holds
[(a : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) "/\" b : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ) Element of the carrier of b1 : ( ( reflexive transitive antisymmetric lower-bounded with_suprema with_infima ) ( non empty reflexive transitive antisymmetric lower-bounded non void with_suprema with_infima ) LATTICE) : ( ( ) ( non empty ) set ) ) ,(x : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) "/\" y : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ) Element of the carrier of b1 : ( ( reflexive transitive antisymmetric lower-bounded with_suprema with_infima ) ( non empty reflexive transitive antisymmetric lower-bounded non void with_suprema with_infima ) LATTICE) : ( ( ) ( non empty ) set ) ) ] : ( ( ) ( ) Element of the carrier of [:b1 : ( ( reflexive transitive antisymmetric lower-bounded with_suprema with_infima ) ( non empty reflexive transitive antisymmetric lower-bounded non void with_suprema with_infima ) LATTICE) ,b1 : ( ( reflexive transitive antisymmetric lower-bounded with_suprema with_infima ) ( non empty reflexive transitive antisymmetric lower-bounded non void with_suprema with_infima ) LATTICE) :] : ( ( strict ) ( non empty strict reflexive transitive antisymmetric non void with_suprema with_infima ) RelStr ) : ( ( ) ( non empty ) set ) ) in R : ( ( auxiliary ) ( Relation-like V82() auxiliary(i) auxiliary(ii) auxiliary(iii) auxiliary(iv) auxiliary ) Relation of ) ) ;

theorem :: WAYBEL_7:42
for L being ( ( reflexive transitive antisymmetric lower-bounded with_suprema with_infima ) ( non empty reflexive transitive antisymmetric lower-bounded non void with_suprema with_infima ) LATTICE)
for R being ( ( auxiliary ) ( Relation-like V82() auxiliary(i) auxiliary(ii) auxiliary(iii) auxiliary(iv) auxiliary ) Relation of ) holds
( R : ( ( auxiliary ) ( Relation-like V82() auxiliary(i) auxiliary(ii) auxiliary(iii) auxiliary(iv) auxiliary ) Relation of ) is multiplicative iff for S being ( ( full ) ( reflexive transitive antisymmetric full ) SubRelStr of [:L : ( ( reflexive transitive antisymmetric lower-bounded with_suprema with_infima ) ( non empty reflexive transitive antisymmetric lower-bounded non void with_suprema with_infima ) LATTICE) ,L : ( ( reflexive transitive antisymmetric lower-bounded with_suprema with_infima ) ( non empty reflexive transitive antisymmetric lower-bounded non void with_suprema with_infima ) LATTICE) :] : ( ( strict ) ( non empty strict reflexive transitive antisymmetric non void with_suprema with_infima ) RelStr ) ) st the carrier of S : ( ( full ) ( reflexive transitive antisymmetric full ) SubRelStr of [:b1 : ( ( reflexive transitive antisymmetric lower-bounded with_suprema with_infima ) ( non empty reflexive transitive antisymmetric lower-bounded non void with_suprema with_infima ) LATTICE) ,b1 : ( ( reflexive transitive antisymmetric lower-bounded with_suprema with_infima ) ( non empty reflexive transitive antisymmetric lower-bounded non void with_suprema with_infima ) LATTICE) :] : ( ( strict ) ( non empty strict reflexive transitive antisymmetric non void with_suprema with_infima ) RelStr ) ) : ( ( ) ( ) set ) = R : ( ( auxiliary ) ( Relation-like V82() auxiliary(i) auxiliary(ii) auxiliary(iii) auxiliary(iv) auxiliary ) Relation of ) holds
S : ( ( full ) ( reflexive transitive antisymmetric full ) SubRelStr of [:b1 : ( ( reflexive transitive antisymmetric lower-bounded with_suprema with_infima ) ( non empty reflexive transitive antisymmetric lower-bounded non void with_suprema with_infima ) LATTICE) ,b1 : ( ( reflexive transitive antisymmetric lower-bounded with_suprema with_infima ) ( non empty reflexive transitive antisymmetric lower-bounded non void with_suprema with_infima ) LATTICE) :] : ( ( strict ) ( non empty strict reflexive transitive antisymmetric non void with_suprema with_infima ) RelStr ) ) is meet-inheriting ) ;

theorem :: WAYBEL_7:43
for L being ( ( reflexive transitive antisymmetric lower-bounded with_suprema with_infima ) ( non empty reflexive transitive antisymmetric lower-bounded non void with_suprema with_infima ) LATTICE)
for R being ( ( auxiliary ) ( Relation-like V82() auxiliary(i) auxiliary(ii) auxiliary(iii) auxiliary(iv) auxiliary ) Relation of ) holds
( R : ( ( auxiliary ) ( Relation-like V82() auxiliary(i) auxiliary(ii) auxiliary(iii) auxiliary(iv) auxiliary ) Relation of ) is multiplicative iff R : ( ( auxiliary ) ( Relation-like V82() auxiliary(i) auxiliary(ii) auxiliary(iii) auxiliary(iv) auxiliary ) Relation of ) -below : ( ( Function-like V21( the carrier of b1 : ( ( reflexive transitive antisymmetric lower-bounded with_suprema with_infima ) ( non empty reflexive transitive antisymmetric lower-bounded non void with_suprema with_infima ) LATTICE) : ( ( ) ( non empty ) set ) , the carrier of (InclPoset (Ids b1 : ( ( reflexive transitive antisymmetric lower-bounded with_suprema with_infima ) ( non empty reflexive transitive antisymmetric lower-bounded non void with_suprema with_infima ) LATTICE) ) : ( ( ) ( non empty ) set ) ) : ( ( strict ) ( non empty strict reflexive transitive antisymmetric lower-bounded upper-bounded bounded up-complete /\-complete non void with_suprema with_infima complete ) RelStr ) : ( ( ) ( non empty ) set ) ) ) ( Relation-like Function-like V21( the carrier of b1 : ( ( reflexive transitive antisymmetric lower-bounded with_suprema with_infima ) ( non empty reflexive transitive antisymmetric lower-bounded non void with_suprema with_infima ) LATTICE) : ( ( ) ( non empty ) set ) , the carrier of (InclPoset (Ids b1 : ( ( reflexive transitive antisymmetric lower-bounded with_suprema with_infima ) ( non empty reflexive transitive antisymmetric lower-bounded non void with_suprema with_infima ) LATTICE) ) : ( ( ) ( non empty ) set ) ) : ( ( strict ) ( non empty strict reflexive transitive antisymmetric lower-bounded upper-bounded bounded up-complete /\-complete non void with_suprema with_infima complete ) RelStr ) : ( ( ) ( non empty ) set ) ) ) Element of bool [: the carrier of b1 : ( ( reflexive transitive antisymmetric lower-bounded with_suprema with_infima ) ( non empty reflexive transitive antisymmetric lower-bounded non void with_suprema with_infima ) LATTICE) : ( ( ) ( non empty ) set ) , the carrier of (InclPoset (Ids b1 : ( ( reflexive transitive antisymmetric lower-bounded with_suprema with_infima ) ( non empty reflexive transitive antisymmetric lower-bounded non void with_suprema with_infima ) LATTICE) ) : ( ( ) ( non empty ) set ) ) : ( ( strict ) ( non empty strict reflexive transitive antisymmetric lower-bounded upper-bounded bounded up-complete /\-complete non void with_suprema with_infima complete ) RelStr ) : ( ( ) ( non empty ) set ) :] : ( ( ) ( non empty Relation-like ) set ) : ( ( ) ( non empty ) set ) ) is meet-preserving ) ;

theorem :: WAYBEL_7:44
for L being ( ( reflexive transitive antisymmetric lower-bounded with_suprema with_infima continuous ) ( non empty reflexive transitive antisymmetric lower-bounded upper-bounded bounded up-complete /\-complete non void with_suprema with_infima complete satisfying_axiom_of_approximation continuous ) LATTICE) st L : ( ( reflexive transitive antisymmetric lower-bounded with_suprema with_infima continuous ) ( non empty reflexive transitive antisymmetric lower-bounded upper-bounded bounded up-complete /\-complete non void with_suprema with_infima complete satisfying_axiom_of_approximation continuous ) LATTICE) -waybelow : ( ( ) ( Relation-like V82() auxiliary(i) auxiliary(ii) auxiliary(iii) auxiliary(iv) auxiliary approximating satisfying_SI satisfying_INT ) Element of bool [: the carrier of b1 : ( ( reflexive transitive antisymmetric lower-bounded with_suprema with_infima continuous ) ( non empty reflexive transitive antisymmetric lower-bounded upper-bounded bounded up-complete /\-complete non void with_suprema with_infima complete satisfying_axiom_of_approximation continuous ) LATTICE) : ( ( ) ( non empty ) set ) , the carrier of b1 : ( ( reflexive transitive antisymmetric lower-bounded with_suprema with_infima continuous ) ( non empty reflexive transitive antisymmetric lower-bounded upper-bounded bounded up-complete /\-complete non void with_suprema with_infima complete satisfying_axiom_of_approximation continuous ) LATTICE) : ( ( ) ( non empty ) set ) :] : ( ( ) ( non empty Relation-like ) set ) : ( ( ) ( non empty ) set ) ) is multiplicative holds
for p being ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) holds
( p : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) is pseudoprime iff for a, b being ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) holds
( not a : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) "/\" b : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) : ( ( ) ( ) Element of the carrier of b1 : ( ( reflexive transitive antisymmetric lower-bounded with_suprema with_infima continuous ) ( non empty reflexive transitive antisymmetric lower-bounded upper-bounded bounded up-complete /\-complete non void with_suprema with_infima complete satisfying_axiom_of_approximation continuous ) LATTICE) : ( ( ) ( non empty ) set ) ) << p : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) or a : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) <= p : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) or b : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) <= p : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ) ) ;

theorem :: WAYBEL_7:45
for L being ( ( reflexive transitive antisymmetric lower-bounded with_suprema with_infima continuous ) ( non empty reflexive transitive antisymmetric lower-bounded upper-bounded bounded up-complete /\-complete non void with_suprema with_infima complete satisfying_axiom_of_approximation continuous ) LATTICE) st L : ( ( reflexive transitive antisymmetric lower-bounded with_suprema with_infima continuous ) ( non empty reflexive transitive antisymmetric lower-bounded upper-bounded bounded up-complete /\-complete non void with_suprema with_infima complete satisfying_axiom_of_approximation continuous ) LATTICE) -waybelow : ( ( ) ( Relation-like V82() auxiliary(i) auxiliary(ii) auxiliary(iii) auxiliary(iv) auxiliary approximating satisfying_SI satisfying_INT ) Element of bool [: the carrier of b1 : ( ( reflexive transitive antisymmetric lower-bounded with_suprema with_infima continuous ) ( non empty reflexive transitive antisymmetric lower-bounded upper-bounded bounded up-complete /\-complete non void with_suprema with_infima complete satisfying_axiom_of_approximation continuous ) LATTICE) : ( ( ) ( non empty ) set ) , the carrier of b1 : ( ( reflexive transitive antisymmetric lower-bounded with_suprema with_infima continuous ) ( non empty reflexive transitive antisymmetric lower-bounded upper-bounded bounded up-complete /\-complete non void with_suprema with_infima complete satisfying_axiom_of_approximation continuous ) LATTICE) : ( ( ) ( non empty ) set ) :] : ( ( ) ( non empty Relation-like ) set ) : ( ( ) ( non empty ) set ) ) is multiplicative holds
for p being ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) st p : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) is pseudoprime holds
p : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) is prime ;

theorem :: WAYBEL_7:46
for L being ( ( reflexive transitive antisymmetric lower-bounded distributive with_suprema with_infima continuous ) ( non empty reflexive transitive antisymmetric lower-bounded upper-bounded bounded up-complete /\-complete distributive non void with_suprema with_infima complete satisfying_axiom_of_approximation continuous ) LATTICE) st ( for p being ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) st p : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) is pseudoprime holds
p : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) is prime ) holds
L : ( ( reflexive transitive antisymmetric lower-bounded distributive with_suprema with_infima continuous ) ( non empty reflexive transitive antisymmetric lower-bounded upper-bounded bounded up-complete /\-complete distributive non void with_suprema with_infima complete satisfying_axiom_of_approximation continuous ) LATTICE) -waybelow : ( ( ) ( Relation-like V82() auxiliary(i) auxiliary(ii) auxiliary(iii) auxiliary(iv) auxiliary approximating satisfying_SI satisfying_INT ) Element of bool [: the carrier of b1 : ( ( reflexive transitive antisymmetric lower-bounded distributive with_suprema with_infima continuous ) ( non empty reflexive transitive antisymmetric lower-bounded upper-bounded bounded up-complete /\-complete distributive non void with_suprema with_infima complete satisfying_axiom_of_approximation continuous ) LATTICE) : ( ( ) ( non empty ) set ) , the carrier of b1 : ( ( reflexive transitive antisymmetric lower-bounded distributive with_suprema with_infima continuous ) ( non empty reflexive transitive antisymmetric lower-bounded upper-bounded bounded up-complete /\-complete distributive non void with_suprema with_infima complete satisfying_axiom_of_approximation continuous ) LATTICE) : ( ( ) ( non empty ) set ) :] : ( ( ) ( non empty Relation-like ) set ) : ( ( ) ( non empty ) set ) ) is multiplicative ;