:: Directed Sets, Nets, Ideals, Filters, and Maps
:: by Grzegorz Bancerek
::
:: Received September 12, 1996
:: Copyright (c) 1996-2012 Association of Mizar Users


begin

definition
let L be RelStr ;
let X be Subset of L;
attrX is directed  means :Def1: :: WAYBEL_0:def 1
 for x, y being Element of L st x in X & y in X holds
ex z being Element of L st
( z in X &amp; x <= z &amp; y <= z );
attrX is filtered  means :Def2: :: WAYBEL_0:def 2
 for x, y being Element of L st x in X &amp; y in X holds
ex z being Element of L st
( z in X &amp; z <= x &amp; z <= y );
end;

:: deftheorem Def1 defines directed WAYBEL_0:def_1_:_
 for L being RelStr
for X being Subset of L holds
( X is directed iff for x, y being Element of L st x in X &amp; y in X holds
ex z being Element of L st
( z in X &amp; x <= z &amp; y <= z ) );

:: deftheorem Def2 defines filtered WAYBEL_0:def_2_:_
 for L being RelStr
for X being Subset of L holds
( X is filtered iff for x, y being Element of L st x in X &amp; y in X holds
ex z being Element of L st
( z in X &amp; z <= x &amp; z <= y ) );

:: Original "directed subset" is equivalent to "non empty directed subset"
:: in our terminology. It is shown bellow.
theorem Th1: :: WAYBEL_0:1
for L being non empty transitive RelStr
for X being Subset of L holds
( ( not X is empty &amp; X is directed ) iff for Y being finite Subset of X ex x being Element of L st
( x in X &amp; x is_>=_than Y ) )
proofend;

:: Original "filtered subset" is equivalent to "non empty filtered subset"
:: in our terminology. It is shown bellow.
theorem Th2: :: WAYBEL_0:2
for L being non empty transitive RelStr
for X being Subset of L holds
( ( not X is empty &amp; X is filtered ) iff for Y being finite Subset of X ex x being Element of L st
( x in X &amp; x is_<=_than Y ) )
proofend;

registration
let L be RelStr ;
cluster empty  ->  directed filtered for Element of K10( the carrier of L);
coherence
 for b1 being Subset of L st b1 is empty holds
( b1 is directed &amp; b1 is filtered )
proofend;
end;

registration
let L be RelStr ;
cluster directed filtered for Element of K10( the carrier of L);
existence
 ex b1 being Subset of L st
( b1 is directed &amp; b1 is filtered )
proofend;
end;

theorem Th3: :: WAYBEL_0:3
for L1, L2 being RelStr st RelStr(# the carrier of L1, the InternalRel of L1 #) = RelStr(# the carrier of L2, the InternalRel of L2 #) holds
for X1 being Subset of L1
for X2 being Subset of L2 st X1 = X2 &amp; X1 is directed holds
X2 is directed
proofend;

theorem :: WAYBEL_0:4
for L1, L2 being RelStr st RelStr(# the carrier of L1, the InternalRel of L1 #) = RelStr(# the carrier of L2, the InternalRel of L2 #) holds
for X1 being Subset of L1
for X2 being Subset of L2 st X1 = X2 &amp; X1 is filtered holds
X2 is filtered
proofend;

theorem Th5: :: WAYBEL_0:5
for L being non empty reflexive RelStr
for x being Element of L holds
( {x} is directed &amp; {x} is filtered )
proofend;

registration
let L be non empty reflexive RelStr ;
cluster non empty finite directed filtered for Element of K10( the carrier of L);
existence
 ex b1 being Subset of L st
( b1 is directed &amp; b1 is filtered &amp; not b1 is empty &amp; b1 is finite )
proofend;
end;

registration
let L be with_suprema RelStr ;
cluster [#] L ->  directed ;
coherence
 [#] L is directed
proofend;
end;

registration
let L be non empty upper-bounded RelStr ;
cluster [#] L ->  directed ;
coherence
 [#] L is directed
proofend;
end;

registration
let L be with_infima RelStr ;
cluster [#] L ->  filtered ;
coherence
 [#] L is filtered
proofend;
end;

registration
let L be non empty lower-bounded RelStr ;
cluster [#] L ->  filtered ;
coherence
 [#] L is filtered
proofend;
end;

definition
let L be non empty RelStr ;
let S be SubRelStr of L;
attrS is filtered-infs-inheriting  means :Def3: :: WAYBEL_0:def 3
 for X being filtered Subset of S st X <> {} &amp; ex_inf_of X,L holds
"/\" (X,L) in the carrier of S;
attrS is directed-sups-inheriting  means :Def4: :: WAYBEL_0:def 4
 for X being directed Subset of S st X <> {} &amp; ex_sup_of X,L holds
"\/" (X,L) in the carrier of S;
end;

:: deftheorem Def3 defines filtered-infs-inheriting WAYBEL_0:def_3_:_
 for L being non empty RelStr
for S being SubRelStr of L holds
( S is filtered-infs-inheriting iff for X being filtered Subset of S st X <> {} &amp; ex_inf_of X,L holds
"/\" (X,L) in the carrier of S );

:: deftheorem Def4 defines directed-sups-inheriting WAYBEL_0:def_4_:_
 for L being non empty RelStr
for S being SubRelStr of L holds
( S is directed-sups-inheriting iff for X being directed Subset of S st X <> {} &amp; ex_sup_of X,L holds
"\/" (X,L) in the carrier of S );

registration
let L be non empty RelStr ;
cluster infs-inheriting  ->  filtered-infs-inheriting for SubRelStr of L;
coherence
 for b1 being SubRelStr of L st b1 is infs-inheriting holds
b1 is filtered-infs-inheriting
proofend;
cluster sups-inheriting  ->  directed-sups-inheriting for SubRelStr of L;
coherence
 for b1 being SubRelStr of L st b1 is sups-inheriting holds
b1 is directed-sups-inheriting
proofend;
end;

registration
let L be non empty RelStr ;
cluster non empty strict full infs-inheriting sups-inheriting for SubRelStr of L;
existence
 ex b1 being SubRelStr of L st
( b1 is infs-inheriting &amp; b1 is sups-inheriting &amp; not b1 is empty &amp; b1 is full &amp; b1 is strict )
proofend;
end;

theorem :: WAYBEL_0:6
for L being non empty transitive RelStr
for S being non empty full filtered-infs-inheriting SubRelStr of L
for X being filtered Subset of S st X <> {} &amp; ex_inf_of X,L holds
( ex_inf_of X,S &amp; "/\" (X,S) = "/\" (X,L) )
proofend;

theorem :: WAYBEL_0:7
for L being non empty transitive RelStr
for S being non empty full directed-sups-inheriting SubRelStr of L
for X being directed Subset of S st X <> {} &amp; ex_sup_of X,L holds
( ex_sup_of X,S &amp; "\/" (X,S) = "\/" (X,L) )
proofend;

begin

definition
let L1, L2 be RelStr ;
let f be Function of L1,L2;
attrf is antitone  means :: WAYBEL_0:def 5
 for x, y being Element of L1 st x <= y holds
for a, b being Element of L2 st a = f . x &amp; b = f . y holds
a >= b;
end;

:: deftheorem  defines antitone WAYBEL_0:def_5_:_
 for L1, L2 being RelStr
for f being Function of L1,L2 holds
( f is antitone iff for x, y being Element of L1 st x <= y holds
for a, b being Element of L2 st a = f . x &amp; b = f . y holds
a >= b );

:: Definition 1.2
definition
let L be 1-sorted ;
attrc2 is strict ;
struct NetStr over L ->  RelStr ;
aggrNetStr(# carrier, InternalRel, mapping #) ->  NetStr over L;
sel mapping c2 ->  Function of the carrier of c2, the carrier of L;
end;

registration
let L be 1-sorted ;
let X be non empty set ;
let O be Relation of X;
let F be Function of X, the carrier of L;
cluster NetStr(# X,O,F #) ->  non empty ;
coherence
 not NetStr(# X,O,F #) is empty ;
end;

definition
let N be RelStr ;
attrN is directed  means :Def6: :: WAYBEL_0:def 6
 [#] N is directed ;
end;

:: deftheorem Def6 defines directed WAYBEL_0:def_6_:_
 for N being RelStr holds
( N is directed iff [#] N is directed );

registration
let L be 1-sorted ;
cluster non empty reflexive transitive antisymmetric strict directed for NetStr over L;
existence
 ex b1 being strict NetStr over L st
( not b1 is empty &amp; b1 is reflexive &amp; b1 is transitive &amp; b1 is antisymmetric &amp; b1 is directed )
proofend;
end;

definition
let L be 1-sorted ;
mode prenet of L is non empty directed NetStr over L;
end;

definition
let L be 1-sorted ;
mode net of L is transitive prenet of L;
end;

definition
let L be non empty 1-sorted ;
let N be non empty NetStr over L;
func netmap (N,L) ->  Function of N,L equals :: WAYBEL_0:def 7
 the mapping of N;
coherence
 the mapping of N is Function of N,L ;
let i be Element of N;
funcN . i ->  Element of L equals :: WAYBEL_0:def 8
 the mapping of N . i;
correctness
coherence
the mapping of N . i is Element of L;
;
end;

:: deftheorem  defines netmap WAYBEL_0:def_7_:_
 for L being non empty 1-sorted
for N being non empty NetStr over L holds netmap (N,L) = the mapping of N;

:: deftheorem  defines . WAYBEL_0:def_8_:_
 for L being non empty 1-sorted
for N being non empty NetStr over L
for i being Element of N holds N . i = the mapping of N . i;

definition
let L be non empty RelStr ;
let N be non empty NetStr over L;
attrN is monotone  means :: WAYBEL_0:def 9
 netmap (N,L) is monotone ;
attrN is antitone  means :: WAYBEL_0:def 10
 netmap (N,L) is antitone ;
end;

:: deftheorem  defines monotone WAYBEL_0:def_9_:_
 for L being non empty RelStr
for N being non empty NetStr over L holds
( N is monotone iff netmap (N,L) is monotone );

:: deftheorem  defines antitone WAYBEL_0:def_10_:_
 for L being non empty RelStr
for N being non empty NetStr over L holds
( N is antitone iff netmap (N,L) is antitone );

definition
let L be non empty 1-sorted ;
let N be non empty NetStr over L;
let X be set ;
predN is_eventually_in X means :Def11: :: WAYBEL_0:def 11
 ex i being Element of N st
for j being Element of N st i <= j holds
N . j in X;
predN is_often_in X means :: WAYBEL_0:def 12
 for i being Element of N ex j being Element of N st
( i <= j &amp; N . j in X );
end;

:: deftheorem Def11 defines is_eventually_in WAYBEL_0:def_11_:_
 for L being non empty 1-sorted
for N being non empty NetStr over L
for X being set holds
( N is_eventually_in X iff ex i being Element of N st
for j being Element of N st i <= j holds
N . j in X );

:: deftheorem  defines is_often_in WAYBEL_0:def_12_:_
 for L being non empty 1-sorted
for N being non empty NetStr over L
for X being set holds
( N is_often_in X iff for i being Element of N ex j being Element of N st
( i <= j &amp; N . j in X ) );

theorem :: WAYBEL_0:8
for L being non empty 1-sorted
for N being non empty NetStr over L
for X, Y being set st X c= Y holds
( ( N is_eventually_in X implies N is_eventually_in Y ) &amp; ( N is_often_in X implies N is_often_in Y ) )
proofend;

theorem :: WAYBEL_0:9
for L being non empty 1-sorted
for N being non empty NetStr over L
for X being set holds
( N is_eventually_in X iff not N is_often_in the carrier of L \ X )
proofend;

theorem :: WAYBEL_0:10
for L being non empty 1-sorted
for N being non empty NetStr over L
for X being set holds
( N is_often_in X iff not N is_eventually_in the carrier of L \ X )
proofend;

scheme :: WAYBEL_0:sch 1
HoldsEventually{ F1() ->  non empty RelStr , F2() ->  non empty NetStr over F1(), P1[ set ] } :
 ( F2() is_eventually_in  {  (F2() . k) where k is Element of F2() : P1[F2() . k]  }  iff ex i being Element of F2() st
for j being Element of F2() st i <= j holds
P1[F2() . j] )
proofend;

definition
let L be non empty RelStr ;
let N be non empty NetStr over L;
attrN is eventually-directed  means :Def13: :: WAYBEL_0:def 13
 for i being Element of N holds N is_eventually_in  {  (N . j) where j is Element of N : N . i <= N . j  }  ;
attrN is eventually-filtered  means :Def14: :: WAYBEL_0:def 14
 for i being Element of N holds N is_eventually_in  {  (N . j) where j is Element of N : N . i >= N . j  }  ;
end;

:: deftheorem Def13 defines eventually-directed WAYBEL_0:def_13_:_
 for L being non empty RelStr
for N being non empty NetStr over L holds
( N is eventually-directed iff for i being Element of N holds N is_eventually_in  {  (N . j) where j is Element of N : N . i <= N . j  }  );

:: deftheorem Def14 defines eventually-filtered WAYBEL_0:def_14_:_
 for L being non empty RelStr
for N being non empty NetStr over L holds
( N is eventually-filtered iff for i being Element of N holds N is_eventually_in  {  (N . j) where j is Element of N : N . i >= N . j  }  );

theorem Th11: :: WAYBEL_0:11
for L being non empty RelStr
for N being non empty NetStr over L holds
( N is eventually-directed iff for i being Element of N ex j being Element of N st
for k being Element of N st j <= k holds
N . i <= N . k )
proofend;

theorem Th12: :: WAYBEL_0:12
for L being non empty RelStr
for N being non empty NetStr over L holds
( N is eventually-filtered iff for i being Element of N ex j being Element of N st
for k being Element of N st j <= k holds
N . i >= N . k )
proofend;

registration
let L be non empty RelStr ;
cluster non empty directed monotone  ->  eventually-directed for NetStr over L;
coherence
 for b1 being prenet of L st b1 is monotone holds
b1 is eventually-directed
proofend;
cluster non empty directed antitone  ->  eventually-filtered for NetStr over L;
coherence
 for b1 being prenet of L st b1 is antitone holds
b1 is eventually-filtered
proofend;
end;

registration
let L be non empty reflexive RelStr ;
cluster non empty strict directed monotone antitone for NetStr over L;
existence
 ex b1 being prenet of L st
( b1 is monotone &amp; b1 is antitone &amp; b1 is strict )
proofend;
end;

begin

:: Definition 1.3
definition
let L be RelStr ;
let X be Subset of L;
func downarrow X ->  Subset of L means :Def15: :: WAYBEL_0:def 15
 for x being Element of L holds
( x in it iff ex y being Element of L st
( y >= x &amp; y in X ) );
existence
 ex b1 being Subset of L st
for x being Element of L holds
( x in b1 iff ex y being Element of L st
( y >= x &amp; y in X ) )
proofend;
uniqueness
 for b1, b2 being Subset of L st ( for x being Element of L holds
( x in b1 iff ex y being Element of L st
( y >= x &amp; y in X ) ) ) &amp; ( for x being Element of L holds
( x in b2 iff ex y being Element of L st
( y >= x &amp; y in X ) ) ) holds
b1 = b2
proofend;
func uparrow X ->  Subset of L means :Def16: :: WAYBEL_0:def 16
 for x being Element of L holds
( x in it iff ex y being Element of L st
( y <= x &amp; y in X ) );
existence
 ex b1 being Subset of L st
for x being Element of L holds
( x in b1 iff ex y being Element of L st
( y <= x &amp; y in X ) )
proofend;
correctness
uniqueness
for b1, b2 being Subset of L st ( for x being Element of L holds
( x in b1 iff ex y being Element of L st
( y <= x &amp; y in X ) ) ) &amp; ( for x being Element of L holds
( x in b2 iff ex y being Element of L st
( y <= x &amp; y in X ) ) ) holds
b1 = b2;
proofend;
end;

:: deftheorem Def15 defines downarrow WAYBEL_0:def_15_:_
 for L being RelStr
for X, b3 being Subset of L holds
( b3 = downarrow X iff for x being Element of L holds
( x in b3 iff ex y being Element of L st
( y >= x &amp; y in X ) ) );

:: deftheorem Def16 defines uparrow WAYBEL_0:def_16_:_
 for L being RelStr
for X, b3 being Subset of L holds
( b3 = uparrow X iff for x being Element of L holds
( x in b3 iff ex y being Element of L st
( y <= x &amp; y in X ) ) );

theorem Th13: :: WAYBEL_0:13
for L1, L2 being RelStr st RelStr(# the carrier of L1, the InternalRel of L1 #) = RelStr(# the carrier of L2, the InternalRel of L2 #) holds
for X being Subset of L1
for Y being Subset of L2 st X = Y holds
( downarrow X = downarrow Y &amp; uparrow X = uparrow Y )
proofend;

theorem Th14: :: WAYBEL_0:14
for L being non empty RelStr
for X being Subset of L holds downarrow X =  {  x where x is Element of L : ex y being Element of L st
( x <= y &amp; y in X )  }
proofend;

theorem Th15: :: WAYBEL_0:15
for L being non empty RelStr
for X being Subset of L holds uparrow X =  {  x where x is Element of L : ex y being Element of L st
( x >= y &amp; y in X )  }
proofend;

registration
let L be non empty reflexive RelStr ;
let X be non empty Subset of L;
cluster downarrow X ->  non empty ;
coherence
 not downarrow X is empty
proofend;
cluster uparrow X ->  non empty ;
coherence
 not uparrow X is empty
proofend;
end;

theorem Th16: :: WAYBEL_0:16
for L being reflexive RelStr
for X being Subset of L holds
( X c= downarrow X &amp; X c= uparrow X )
proofend;

definition
let L be non empty RelStr ;
let x be Element of L;
func downarrow x ->  Subset of L equals :: WAYBEL_0:def 17
 downarrow {x};
correctness
coherence
downarrow {x} is Subset of L;
;
func uparrow x ->  Subset of L equals :: WAYBEL_0:def 18
 uparrow {x};
correctness
coherence
uparrow {x} is Subset of L;
;
end;

:: deftheorem  defines downarrow WAYBEL_0:def_17_:_
 for L being non empty RelStr
for x being Element of L holds downarrow x = downarrow {x};

:: deftheorem  defines uparrow WAYBEL_0:def_18_:_
 for L being non empty RelStr
for x being Element of L holds uparrow x = uparrow {x};

theorem Th17: :: WAYBEL_0:17
for L being non empty RelStr
for x, y being Element of L holds
( y in downarrow x iff y <= x )
proofend;

theorem Th18: :: WAYBEL_0:18
for L being non empty RelStr
for x, y being Element of L holds
( y in uparrow x iff x <= y )
proofend;

theorem :: WAYBEL_0:19
for L being non empty reflexive antisymmetric RelStr
for x, y being Element of L st downarrow x = downarrow y holds
x = y
proofend;

theorem :: WAYBEL_0:20
for L being non empty reflexive antisymmetric RelStr
for x, y being Element of L st uparrow x = uparrow y holds
x = y
proofend;

theorem Th21: :: WAYBEL_0:21
for L being non empty transitive RelStr
for x, y being Element of L st x <= y holds
downarrow x c= downarrow y
proofend;

theorem Th22: :: WAYBEL_0:22
for L being non empty transitive RelStr
for x, y being Element of L st x <= y holds
uparrow y c= uparrow x
proofend;

registration
let L be non empty reflexive RelStr ;
let x be Element of L;
cluster downarrow x ->  non empty directed ;
coherence
 ( not downarrow x is empty &amp; downarrow x is directed )
proofend;
cluster uparrow x ->  non empty filtered ;
coherence
 ( not uparrow x is empty &amp; uparrow x is filtered )
proofend;
end;

definition
let L be RelStr ;
let X be Subset of L;
attrX is lower  means :Def19: :: WAYBEL_0:def 19
 for x, y being Element of L st x in X &amp; y <= x holds
y in X;
attrX is upper  means :Def20: :: WAYBEL_0:def 20
 for x, y being Element of L st x in X &amp; x <= y holds
y in X;
end;

:: deftheorem Def19 defines lower WAYBEL_0:def_19_:_
 for L being RelStr
for X being Subset of L holds
( X is lower iff for x, y being Element of L st x in X &amp; y <= x holds
y in X );

:: deftheorem Def20 defines upper WAYBEL_0:def_20_:_
 for L being RelStr
for X being Subset of L holds
( X is upper iff for x, y being Element of L st x in X &amp; x <= y holds
y in X );

registration
let L be RelStr ;
cluster lower upper for Element of K10( the carrier of L);
existence
 ex b1 being Subset of L st
( b1 is lower &amp; b1 is upper )
proofend;
end;

theorem Th23: :: WAYBEL_0:23
for L being RelStr
for X being Subset of L holds
( X is lower iff downarrow X c= X )
proofend;

theorem Th24: :: WAYBEL_0:24
for L being RelStr
for X being Subset of L holds
( X is upper iff uparrow X c= X )
proofend;

theorem :: WAYBEL_0:25
for L1, L2 being RelStr st RelStr(# the carrier of L1, the InternalRel of L1 #) = RelStr(# the carrier of L2, the InternalRel of L2 #) holds
for X1 being Subset of L1
for X2 being Subset of L2 st X1 = X2 holds
( ( X1 is lower implies X2 is lower ) &amp; ( X1 is upper implies X2 is upper ) )
proofend;

theorem :: WAYBEL_0:26
for L being RelStr
for A being Subset-Family of L st ( for X being Subset of L st X in A holds
X is lower ) holds
union A is lower Subset of L
proofend;

theorem Th27: :: WAYBEL_0:27
for L being RelStr
for X, Y being Subset of L st X is lower &amp; Y is lower holds
( X /\ Y is lower &amp; X \/ Y is lower )
proofend;

theorem :: WAYBEL_0:28
for L being RelStr
for A being Subset-Family of L st ( for X being Subset of L st X in A holds
X is upper ) holds
union A is upper Subset of L
proofend;

theorem Th29: :: WAYBEL_0:29
for L being RelStr
for X, Y being Subset of L st X is upper &amp; Y is upper holds
( X /\ Y is upper &amp; X \/ Y is upper )
proofend;

registration
let L be non empty transitive RelStr ;
let X be Subset of L;
cluster downarrow X ->  lower ;
coherence
 downarrow X is lower
proofend;
cluster uparrow X ->  upper ;
coherence
 uparrow X is upper
proofend;
end;

registration
let L be non empty transitive RelStr ;
let x be Element of L;
cluster downarrow x ->  lower ;
coherence
 downarrow x is lower ;
cluster uparrow x ->  upper ;
coherence
 uparrow x is upper ;
end;

registration
let L be non empty RelStr ;
cluster [#] L ->  lower upper ;
coherence
 ( [#] L is lower &amp; [#] L is upper )
proofend;
end;

registration
let L be non empty RelStr ;
cluster non empty lower upper for Element of K10( the carrier of L);
existence
 ex b1 being Subset of L st
( not b1 is empty &amp; b1 is lower &amp; b1 is upper )
proofend;
end;

registration
let L be non empty reflexive transitive RelStr ;
cluster non empty directed lower for Element of K10( the carrier of L);
existence
 ex b1 being Subset of L st
( not b1 is empty &amp; b1 is lower &amp; b1 is directed )
proofend;
cluster non empty filtered upper for Element of K10( the carrier of L);
existence
 ex b1 being Subset of L st
( not b1 is empty &amp; b1 is upper &amp; b1 is filtered )
proofend;
end;

registration
let L be with_suprema with_infima Poset;
cluster non empty directed filtered lower upper for Element of K10( the carrier of L);
existence
 ex b1 being Subset of L st
( not b1 is empty &amp; b1 is directed &amp; b1 is filtered &amp; b1 is lower &amp; b1 is upper )
proofend;
end;

theorem Th30: :: WAYBEL_0:30
for L being non empty reflexive transitive RelStr
for X being Subset of L holds
( X is directed iff downarrow X is directed )
proofend;

registration
let L be non empty reflexive transitive RelStr ;
let X be directed Subset of L;
cluster downarrow X ->  directed ;
coherence
 downarrow X is directed by Th30;
end;

theorem Th31: :: WAYBEL_0:31
for L being non empty reflexive transitive RelStr
for X being Subset of L
for x being Element of L holds
( x is_>=_than X iff x is_>=_than downarrow X )
proofend;

theorem Th32: :: WAYBEL_0:32
for L being non empty reflexive transitive RelStr
for X being Subset of L holds
( ex_sup_of X,L iff ex_sup_of downarrow X,L )
proofend;

theorem Th33: :: WAYBEL_0:33
for L being non empty reflexive transitive RelStr
for X being Subset of L st ex_sup_of X,L holds
sup X = sup (downarrow X)
proofend;

theorem :: WAYBEL_0:34
for L being non empty Poset
for x being Element of L holds
( ex_sup_of downarrow x,L &amp; sup (downarrow x) = x )
proofend;

theorem Th35: :: WAYBEL_0:35
for L being non empty reflexive transitive RelStr
for X being Subset of L holds
( X is filtered iff uparrow X is filtered )
proofend;

registration
let L be non empty reflexive transitive RelStr ;
let X be filtered Subset of L;
cluster uparrow X ->  filtered ;
coherence
 uparrow X is filtered by Th35;
end;

theorem Th36: :: WAYBEL_0:36
for L being non empty reflexive transitive RelStr
for X being Subset of L
for x being Element of L holds
( x is_<=_than X iff x is_<=_than uparrow X )
proofend;

theorem Th37: :: WAYBEL_0:37
for L being non empty reflexive transitive RelStr
for X being Subset of L holds
( ex_inf_of X,L iff ex_inf_of uparrow X,L )
proofend;

theorem Th38: :: WAYBEL_0:38
for L being non empty reflexive transitive RelStr
for X being Subset of L st ex_inf_of X,L holds
inf X = inf (uparrow X)
proofend;

theorem :: WAYBEL_0:39
for L being non empty Poset
for x being Element of L holds
( ex_inf_of uparrow x,L &amp; inf (uparrow x) = x )
proofend;

begin

definition
let L be non empty reflexive transitive RelStr ;
mode Ideal of L is non empty directed lower Subset of L;
mode Filter of L is non empty filtered upper Subset of L;
end;

theorem Th40: :: WAYBEL_0:40
for L being antisymmetric with_suprema RelStr
for X being lower Subset of L holds
( X is directed iff for x, y being Element of L st x in X &amp; y in X holds
x "\/" y in X )
proofend;

theorem Th41: :: WAYBEL_0:41
for L being antisymmetric with_infima RelStr
for X being upper Subset of L holds
( X is filtered iff for x, y being Element of L st x in X &amp; y in X holds
x "/\" y in X )
proofend;

theorem Th42: :: WAYBEL_0:42
for L being with_suprema Poset
for X being non empty lower Subset of L holds
( X is directed iff for Y being finite Subset of X st Y <> {} holds
"\/" (Y,L) in X )
proofend;

theorem Th43: :: WAYBEL_0:43
for L being with_infima Poset
for X being non empty upper Subset of L holds
( X is filtered iff for Y being finite Subset of X st Y <> {} holds
"/\" (Y,L) in X )
proofend;

theorem :: WAYBEL_0:44
for L being non empty antisymmetric RelStr st ( L is with_suprema or L is with_infima ) holds
for X, Y being Subset of L st X is lower &amp; X is directed &amp; Y is lower &amp; Y is directed holds
X /\ Y is directed
proofend;

theorem :: WAYBEL_0:45
for L being non empty antisymmetric RelStr st ( L is with_suprema or L is with_infima ) holds
for X, Y being Subset of L st X is upper &amp; X is filtered &amp; Y is upper &amp; Y is filtered holds
X /\ Y is filtered
proofend;

theorem :: WAYBEL_0:46
for L being RelStr
for A being Subset-Family of L st ( for X being Subset of L st X in A holds
X is directed ) &amp; ( for X, Y being Subset of L st X in A &amp; Y in A holds
ex Z being Subset of L st
( Z in A &amp; X \/ Y c= Z ) ) holds
for X being Subset of L st X = union A holds
X is directed
proofend;

theorem :: WAYBEL_0:47
for L being RelStr
for A being Subset-Family of L st ( for X being Subset of L st X in A holds
X is filtered ) &amp; ( for X, Y being Subset of L st X in A &amp; Y in A holds
ex Z being Subset of L st
( Z in A &amp; X \/ Y c= Z ) ) holds
for X being Subset of L st X = union A holds
X is filtered
proofend;

definition
let L be non empty reflexive transitive RelStr ;
let I be Ideal of L;
attrI is principal  means :: WAYBEL_0:def 21
 ex x being Element of L st
( x in I &amp; x is_>=_than I );
end;

:: deftheorem  defines principal WAYBEL_0:def_21_:_
 for L being non empty reflexive transitive RelStr
for I being Ideal of L holds
( I is principal iff ex x being Element of L st
( x in I &amp; x is_>=_than I ) );

definition
let L be non empty reflexive transitive RelStr ;
let F be Filter of L;
attrF is principal  means :: WAYBEL_0:def 22
 ex x being Element of L st
( x in F &amp; x is_<=_than F );
end;

:: deftheorem  defines principal WAYBEL_0:def_22_:_
 for L being non empty reflexive transitive RelStr
for F being Filter of L holds
( F is principal iff ex x being Element of L st
( x in F &amp; x is_<=_than F ) );

theorem :: WAYBEL_0:48
for L being non empty reflexive transitive RelStr
for I being Ideal of L holds
( I is principal iff ex x being Element of L st I = downarrow x )
proofend;

theorem :: WAYBEL_0:49
for L being non empty reflexive transitive RelStr
for F being Filter of L holds
( F is principal iff ex x being Element of L st F = uparrow x )
proofend;

definition
let L be non empty reflexive transitive RelStr ;
func Ids L ->  set  equals :: WAYBEL_0:def 23
 {  X where X is Ideal of L : verum  }  ;
correctness
coherence
{  X where X is Ideal of L : verum  }  is set ;
;
func Filt L ->  set  equals :: WAYBEL_0:def 24
 {  X where X is Filter of L : verum  }  ;
correctness
coherence
{  X where X is Filter of L : verum  }  is set ;
;
end;

:: deftheorem  defines Ids WAYBEL_0:def_23_:_
 for L being non empty reflexive transitive RelStr holds Ids L =  {  X where X is Ideal of L : verum  }  ;

:: deftheorem  defines Filt WAYBEL_0:def_24_:_
 for L being non empty reflexive transitive RelStr holds Filt L =  {  X where X is Filter of L : verum  }  ;

definition
let L be non empty reflexive transitive RelStr ;
func Ids_0 L ->  set  equals :: WAYBEL_0:def 25
(Ids L) \/ {{}};
correctness
coherence
(Ids L) \/ {{}} is set ;
;
func Filt_0 L ->  set  equals :: WAYBEL_0:def 26
(Filt L) \/ {{}};
correctness
coherence
(Filt L) \/ {{}} is set ;
;
end;

:: deftheorem  defines Ids_0 WAYBEL_0:def_25_:_
 for L being non empty reflexive transitive RelStr holds Ids_0 L = (Ids L) \/ {{}};

:: deftheorem  defines Filt_0 WAYBEL_0:def_26_:_
 for L being non empty reflexive transitive RelStr holds Filt_0 L = (Filt L) \/ {{}};

definition
let L be non empty RelStr ;
let X be Subset of L;
set D =  {  ("\/" (Y,L)) where Y is finite Subset of X : ex_sup_of Y,L  }  ;
A1:  {  ("\/" (Y,L)) where Y is finite Subset of X : ex_sup_of Y,L  }  c= the carrier of L
proofend;
func finsups X ->  Subset of L equals :: WAYBEL_0:def 27
 {  ("\/" (Y,L)) where Y is finite Subset of X : ex_sup_of Y,L  }  ;
correctness
coherence
{  ("\/" (Y,L)) where Y is finite Subset of X : ex_sup_of Y,L  }  is Subset of L;
by A1;
set D =  {  ("/\" (Y,L)) where Y is finite Subset of X : ex_inf_of Y,L  }  ;
A2:  {  ("/\" (Y,L)) where Y is finite Subset of X : ex_inf_of Y,L  }  c= the carrier of L
proofend;
func fininfs X ->  Subset of L equals :: WAYBEL_0:def 28
 {  ("/\" (Y,L)) where Y is finite Subset of X : ex_inf_of Y,L  }  ;
correctness
coherence
{  ("/\" (Y,L)) where Y is finite Subset of X : ex_inf_of Y,L  }  is Subset of L;
by A2;
end;

:: deftheorem  defines finsups WAYBEL_0:def_27_:_
 for L being non empty RelStr
for X being Subset of L holds finsups X =  {  ("\/" (Y,L)) where Y is finite Subset of X : ex_sup_of Y,L  }  ;

:: deftheorem  defines fininfs WAYBEL_0:def_28_:_
 for L being non empty RelStr
for X being Subset of L holds fininfs X =  {  ("/\" (Y,L)) where Y is finite Subset of X : ex_inf_of Y,L  }  ;

registration
let L be non empty antisymmetric lower-bounded RelStr ;
let X be Subset of L;
cluster finsups X ->  non empty ;
coherence
 not finsups X is empty
proofend;
end;

registration
let L be non empty antisymmetric upper-bounded RelStr ;
let X be Subset of L;
cluster fininfs X ->  non empty ;
coherence
 not fininfs X is empty
proofend;
end;

registration
let L be non empty reflexive antisymmetric RelStr ;
let X be non empty Subset of L;
cluster finsups X ->  non empty ;
coherence
 not finsups X is empty
proofend;
cluster fininfs X ->  non empty ;
coherence
 not fininfs X is empty
proofend;
end;

theorem Th50: :: WAYBEL_0:50
for L being non empty reflexive antisymmetric RelStr
for X being Subset of L holds
( X c= finsups X &amp; X c= fininfs X )
proofend;

theorem Th51: :: WAYBEL_0:51
for L being non empty transitive RelStr
for X, F being Subset of L st ( for Y being finite Subset of X st Y <> {} holds
ex_sup_of Y,L ) &amp; ( for x being Element of L st x in F holds
ex Y being finite Subset of X st
( ex_sup_of Y,L &amp; x = "\/" (Y,L) ) ) &amp; ( for Y being finite Subset of X st Y <> {} holds
"\/" (Y,L) in F ) holds
F is directed
proofend;

registration
let L be with_suprema Poset;
let X be Subset of L;
cluster finsups X ->  directed ;
coherence
 finsups X is directed
proofend;
end;

theorem Th52: :: WAYBEL_0:52
for L being non empty reflexive transitive RelStr
for X, F being Subset of L st ( for Y being finite Subset of X st Y <> {} holds
ex_sup_of Y,L ) &amp; ( for x being Element of L st x in F holds
ex Y being finite Subset of X st
( ex_sup_of Y,L &amp; x = "\/" (Y,L) ) ) &amp; ( for Y being finite Subset of X st Y <> {} holds
"\/" (Y,L) in F ) holds
for x being Element of L holds
( x is_>=_than X iff x is_>=_than F )
proofend;

theorem Th53: :: WAYBEL_0:53
for L being non empty reflexive transitive RelStr
for X, F being Subset of L st ( for Y being finite Subset of X st Y <> {} holds
ex_sup_of Y,L ) &amp; ( for x being Element of L st x in F holds
ex Y being finite Subset of X st
( ex_sup_of Y,L &amp; x = "\/" (Y,L) ) ) &amp; ( for Y being finite Subset of X st Y <> {} holds
"\/" (Y,L) in F ) holds
( ex_sup_of X,L iff ex_sup_of F,L )
proofend;

theorem Th54: :: WAYBEL_0:54
for L being non empty reflexive transitive RelStr
for X, F being Subset of L st ( for Y being finite Subset of X st Y <> {} holds
ex_sup_of Y,L ) &amp; ( for x being Element of L st x in F holds
ex Y being finite Subset of X st
( ex_sup_of Y,L &amp; x = "\/" (Y,L) ) ) &amp; ( for Y being finite Subset of X st Y <> {} holds
"\/" (Y,L) in F ) &amp; ex_sup_of X,L holds
sup F = sup X
proofend;

theorem :: WAYBEL_0:55
for L being with_suprema Poset
for X being Subset of L st ( ex_sup_of X,L or L is complete ) holds
sup X = sup (finsups X)
proofend;

theorem Th56: :: WAYBEL_0:56
for L being non empty transitive RelStr
for X, F being Subset of L st ( for Y being finite Subset of X st Y <> {} holds
ex_inf_of Y,L ) &amp; ( for x being Element of L st x in F holds
ex Y being finite Subset of X st
( ex_inf_of Y,L &amp; x = "/\" (Y,L) ) ) &amp; ( for Y being finite Subset of X st Y <> {} holds
"/\" (Y,L) in F ) holds
F is filtered
proofend;

registration
let L be with_infima Poset;
let X be Subset of L;
cluster fininfs X ->  filtered ;
coherence
 fininfs X is filtered
proofend;
end;

theorem Th57: :: WAYBEL_0:57
for L being non empty reflexive transitive RelStr
for X, F being Subset of L st ( for Y being finite Subset of X st Y <> {} holds
ex_inf_of Y,L ) &amp; ( for x being Element of L st x in F holds
ex Y being finite Subset of X st
( ex_inf_of Y,L &amp; x = "/\" (Y,L) ) ) &amp; ( for Y being finite Subset of X st Y <> {} holds
"/\" (Y,L) in F ) holds
for x being Element of L holds
( x is_<=_than X iff x is_<=_than F )
proofend;

theorem Th58: :: WAYBEL_0:58
for L being non empty reflexive transitive RelStr
for X, F being Subset of L st ( for Y being finite Subset of X st Y <> {} holds
ex_inf_of Y,L ) &amp; ( for x being Element of L st x in F holds
ex Y being finite Subset of X st
( ex_inf_of Y,L &amp; x = "/\" (Y,L) ) ) &amp; ( for Y being finite Subset of X st Y <> {} holds
"/\" (Y,L) in F ) holds
( ex_inf_of X,L iff ex_inf_of F,L )
proofend;

theorem Th59: :: WAYBEL_0:59
for L being non empty reflexive transitive RelStr
for X, F being Subset of L st ( for Y being finite Subset of X st Y <> {} holds
ex_inf_of Y,L ) &amp; ( for x being Element of L st x in F holds
ex Y being finite Subset of X st
( ex_inf_of Y,L &amp; x = "/\" (Y,L) ) ) &amp; ( for Y being finite Subset of X st Y <> {} holds
"/\" (Y,L) in F ) &amp; ex_inf_of X,L holds
inf F = inf X
proofend;

theorem :: WAYBEL_0:60
for L being with_infima Poset
for X being Subset of L st ( ex_inf_of X,L or L is complete ) holds
inf X = inf (fininfs X)
proofend;

theorem :: WAYBEL_0:61
for L being with_suprema Poset
for X being Subset of L holds
( X c= downarrow (finsups X) &amp; ( for I being Ideal of L st X c= I holds
downarrow (finsups X) c= I ) )
proofend;

theorem :: WAYBEL_0:62
for L being with_infima Poset
for X being Subset of L holds
( X c= uparrow (fininfs X) &amp; ( for F being Filter of L st X c= F holds
uparrow (fininfs X) c= F ) )
proofend;

begin

definition
let L be non empty RelStr ;
attrL is connected  means :Def29: :: WAYBEL_0:def 29
 for x, y being Element of L holds
( x <= y or y <= x );
end;

:: deftheorem Def29 defines connected WAYBEL_0:def_29_:_
 for L being non empty RelStr holds
( L is connected iff for x, y being Element of L holds
( x <= y or y <= x ) );

registration
cluster non empty trivial reflexive  ->  non empty reflexive connected for RelStr ;
coherence
 for b1 being non empty reflexive RelStr st b1 is trivial holds
b1 is connected
proofend;
end;

registration
cluster non empty V58() reflexive transitive antisymmetric connected for RelStr ;
existence
 ex b1 being non empty Poset st b1 is connected
proofend;
end;

definition
mode Chain is non empty connected Poset;
end;

registration
let L be Chain;
clusterL ~  ->  connected ;
coherence
 L ~ is connected
proofend;
end;

begin

definition
mode Semilattice is with_infima Poset;
mode sup-Semilattice is with_suprema Poset;
mode LATTICE is with_suprema with_infima Poset;
end;

theorem :: WAYBEL_0:63
for L being Semilattice
for X being non empty upper Subset of L holds
( X is Filter of L iff subrelstr X is meet-inheriting )
proofend;

theorem :: WAYBEL_0:64
for L being sup-Semilattice
for X being non empty lower Subset of L holds
( X is Ideal of L iff subrelstr X is join-inheriting )
proofend;

begin

definition
let S, T be non empty RelStr ;
let f be Function of S,T;
let X be Subset of S;
predf preserves_inf_of X means :Def30: :: WAYBEL_0:def 30
( ex_inf_of X,S implies ( ex_inf_of f .: X,T &amp; inf (f .: X) = f . (inf X) ) );
predf preserves_sup_of X means :Def31: :: WAYBEL_0:def 31
( ex_sup_of X,S implies ( ex_sup_of f .: X,T &amp; sup (f .: X) = f . (sup X) ) );
end;

:: deftheorem Def30 defines preserves_inf_of WAYBEL_0:def_30_:_
 for S, T being non empty RelStr
for f being Function of S,T
for X being Subset of S holds
( f preserves_inf_of X iff ( ex_inf_of X,S implies ( ex_inf_of f .: X,T &amp; inf (f .: X) = f . (inf X) ) ) );

:: deftheorem Def31 defines preserves_sup_of WAYBEL_0:def_31_:_
 for S, T being non empty RelStr
for f being Function of S,T
for X being Subset of S holds
( f preserves_sup_of X iff ( ex_sup_of X,S implies ( ex_sup_of f .: X,T &amp; sup (f .: X) = f . (sup X) ) ) );

theorem :: WAYBEL_0:65
for S1, S2, T1, T2 being non empty RelStr st RelStr(# the carrier of S1, the InternalRel of S1 #) = RelStr(# the carrier of T1, the InternalRel of T1 #) &amp; RelStr(# the carrier of S2, the InternalRel of S2 #) = RelStr(# the carrier of T2, the InternalRel of T2 #) holds
for f being Function of S1,S2
for g being Function of T1,T2 st f = g holds
for X being Subset of S1
for Y being Subset of T1 st X = Y holds
( ( f preserves_sup_of X implies g preserves_sup_of Y ) &amp; ( f preserves_inf_of X implies g preserves_inf_of Y ) )
proofend;

definition
let L1, L2 be non empty RelStr ;
let f be Function of L1,L2;
attrf is infs-preserving  means :: WAYBEL_0:def 32
 for X being Subset of L1 holds f preserves_inf_of X;
attrf is sups-preserving  means :: WAYBEL_0:def 33
 for X being Subset of L1 holds f preserves_sup_of X;
attrf is meet-preserving  means :: WAYBEL_0:def 34
 for x, y being Element of L1 holds f preserves_inf_of {x,y};
attrf is join-preserving  means :: WAYBEL_0:def 35
 for x, y being Element of L1 holds f preserves_sup_of {x,y};
attrf is filtered-infs-preserving  means :: WAYBEL_0:def 36
 for X being Subset of L1 st not X is empty &amp; X is filtered holds
f preserves_inf_of X;
attrf is directed-sups-preserving  means :: WAYBEL_0:def 37
 for X being Subset of L1 st not X is empty &amp; X is directed holds
f preserves_sup_of X;
end;

:: deftheorem  defines infs-preserving WAYBEL_0:def_32_:_
 for L1, L2 being non empty RelStr
for f being Function of L1,L2 holds
( f is infs-preserving iff for X being Subset of L1 holds f preserves_inf_of X );

:: deftheorem  defines sups-preserving WAYBEL_0:def_33_:_
 for L1, L2 being non empty RelStr
for f being Function of L1,L2 holds
( f is sups-preserving iff for X being Subset of L1 holds f preserves_sup_of X );

:: deftheorem  defines meet-preserving WAYBEL_0:def_34_:_
 for L1, L2 being non empty RelStr
for f being Function of L1,L2 holds
( f is meet-preserving iff for x, y being Element of L1 holds f preserves_inf_of {x,y} );

:: deftheorem  defines join-preserving WAYBEL_0:def_35_:_
 for L1, L2 being non empty RelStr
for f being Function of L1,L2 holds
( f is join-preserving iff for x, y being Element of L1 holds f preserves_sup_of {x,y} );

:: deftheorem  defines filtered-infs-preserving WAYBEL_0:def_36_:_
 for L1, L2 being non empty RelStr
for f being Function of L1,L2 holds
( f is filtered-infs-preserving iff for X being Subset of L1 st not X is empty &amp; X is filtered holds
f preserves_inf_of X );

:: deftheorem  defines directed-sups-preserving WAYBEL_0:def_37_:_
 for L1, L2 being non empty RelStr
for f being Function of L1,L2 holds
( f is directed-sups-preserving iff for X being Subset of L1 st not X is empty &amp; X is directed holds
f preserves_sup_of X );

registration
let L1, L2 be non empty RelStr ;
cluster Function-like V21( the carrier of L1, the carrier of L2) infs-preserving  ->  meet-preserving filtered-infs-preserving for Element of K10(K11( the carrier of L1, the carrier of L2));
coherence
 for b1 being Function of L1,L2 st b1 is infs-preserving holds
( b1 is filtered-infs-preserving &amp; b1 is meet-preserving )
proofend;
cluster Function-like V21( the carrier of L1, the carrier of L2) sups-preserving  ->  join-preserving directed-sups-preserving for Element of K10(K11( the carrier of L1, the carrier of L2));
coherence
 for b1 being Function of L1,L2 st b1 is sups-preserving holds
( b1 is directed-sups-preserving &amp; b1 is join-preserving )
proofend;
end;

definition
let S, T be RelStr ;
let f be Function of S,T;
attrf is isomorphic  means :Def38: :: WAYBEL_0:def 38
( f is one-to-one &amp; f is monotone &amp; ex g being Function of T,S st
( g = f " &amp; g is monotone ) ) if ( not S is empty &amp; not T is empty )
otherwise ( S is empty &amp; T is empty );
correctness
consistency
verum;
;
end;

:: deftheorem Def38 defines isomorphic WAYBEL_0:def_38_:_
 for S, T being RelStr
for f being Function of S,T holds
( ( not S is empty &amp; not T is empty implies ( f is isomorphic iff ( f is one-to-one &amp; f is monotone &amp; ex g being Function of T,S st
( g = f " &amp; g is monotone ) ) ) ) &amp; ( ( S is empty or T is empty ) implies ( f is isomorphic iff ( S is empty &amp; T is empty ) ) ) );

theorem Th66: :: WAYBEL_0:66
for S, T being non empty RelStr
for f being Function of S,T holds
( f is isomorphic iff ( f is one-to-one &amp; rng f = the carrier of T &amp; ( for x, y being Element of S holds
( x <= y iff f . x <= f . y ) ) ) )
proofend;

registration
let S, T be non empty RelStr ;
cluster Function-like V21( the carrier of S, the carrier of T) isomorphic  ->  one-to-one monotone for Element of K10(K11( the carrier of S, the carrier of T));
coherence
 for b1 being Function of S,T st b1 is isomorphic holds
( b1 is one-to-one &amp; b1 is monotone ) by Def38;
end;

theorem :: WAYBEL_0:67
for S, T being non empty RelStr
for f being Function of S,T st f is isomorphic holds
( f " is Function of T,S &amp; rng (f ") = the carrier of S )
proofend;

theorem :: WAYBEL_0:68
for S, T being non empty RelStr
for f being Function of S,T st f is isomorphic holds
for g being Function of T,S st g = f " holds
g is isomorphic
proofend;

theorem Th69: :: WAYBEL_0:69
for S, T being non empty Poset
for f being Function of S,T st ( for X being Filter of S holds f preserves_inf_of X ) holds
f is monotone
proofend;

theorem :: WAYBEL_0:70
for S, T being non empty Poset
for f being Function of S,T st ( for X being Filter of S holds f preserves_inf_of X ) holds
f is filtered-infs-preserving
proofend;

theorem :: WAYBEL_0:71
for S being Semilattice
for T being non empty Poset
for f being Function of S,T st ( for X being finite Subset of S holds f preserves_inf_of X ) &amp; ( for X being non empty filtered Subset of S holds f preserves_inf_of X ) holds
f is infs-preserving
proofend;

theorem Th72: :: WAYBEL_0:72
for S, T being non empty Poset
for f being Function of S,T st ( for X being Ideal of S holds f preserves_sup_of X ) holds
f is monotone
proofend;

theorem :: WAYBEL_0:73
for S, T being non empty Poset
for f being Function of S,T st ( for X being Ideal of S holds f preserves_sup_of X ) holds
f is directed-sups-preserving
proofend;

theorem :: WAYBEL_0:74
for S being sup-Semilattice
for T being non empty Poset
for f being Function of S,T st ( for X being finite Subset of S holds f preserves_sup_of X ) &amp; ( for X being non empty directed Subset of S holds f preserves_sup_of X ) holds
f is sups-preserving
proofend;

begin

definition
let L be non empty reflexive RelStr ;
attrL is up-complete  means :Def39: :: WAYBEL_0:def 39
 for X being non empty directed Subset of L ex x being Element of L st
( x is_>=_than X &amp; ( for y being Element of L st y is_>=_than X holds
x <= y ) );
end;

:: deftheorem Def39 defines up-complete WAYBEL_0:def_39_:_
 for L being non empty reflexive RelStr holds
( L is up-complete iff for X being non empty directed Subset of L ex x being Element of L st
( x is_>=_than X &amp; ( for y being Element of L st y is_>=_than X holds
x <= y ) ) );

registration
cluster reflexive with_suprema up-complete  ->  reflexive with_suprema upper-bounded for RelStr ;
coherence
 for b1 being reflexive with_suprema RelStr st b1 is up-complete holds
b1 is upper-bounded
proofend;
end;

theorem :: WAYBEL_0:75
for L being non empty reflexive antisymmetric RelStr holds
( L is up-complete iff for X being non empty directed Subset of L holds ex_sup_of X,L )
proofend;

definition
let L be non empty reflexive RelStr ;
attrL is /\-complete  means :Def40: :: WAYBEL_0:def 40
 for X being non empty Subset of L ex x being Element of L st
( x is_<=_than X &amp; ( for y being Element of L st y is_<=_than X holds
x >= y ) );
end;

:: deftheorem Def40 defines /\-complete WAYBEL_0:def_40_:_
 for L being non empty reflexive RelStr holds
( L is /\-complete iff for X being non empty Subset of L ex x being Element of L st
( x is_<=_than X &amp; ( for y being Element of L st y is_<=_than X holds
x >= y ) ) );

theorem Th76: :: WAYBEL_0:76
for L being non empty reflexive antisymmetric RelStr holds
( L is /\-complete iff for X being non empty Subset of L holds ex_inf_of X,L )
proofend;

registration
cluster non empty reflexive complete  ->  non empty reflexive up-complete /\-complete for RelStr ;
coherence
 for b1 being non empty reflexive RelStr st b1 is complete holds
( b1 is up-complete &amp; b1 is /\-complete )
proofend;
cluster non empty reflexive /\-complete  ->  non empty reflexive lower-bounded for RelStr ;
coherence
 for b1 being non empty reflexive RelStr st b1 is /\-complete holds
b1 is lower-bounded
proofend;
cluster non empty reflexive transitive antisymmetric with_suprema lower-bounded up-complete  ->  non empty complete for RelStr ;
coherence
 for b1 being non empty Poset st b1 is up-complete &amp; b1 is with_suprema &amp; b1 is lower-bounded holds
b1 is complete
proofend;
end;

registration
cluster non empty reflexive antisymmetric /\-complete  ->  non empty reflexive antisymmetric with_infima for RelStr ;
coherence
 for b1 being non empty reflexive antisymmetric RelStr st b1 is /\-complete holds
b1 is with_infima
proofend;
end;

registration
cluster non empty reflexive antisymmetric upper-bounded /\-complete  ->  non empty reflexive antisymmetric with_suprema upper-bounded for RelStr ;
coherence
 for b1 being non empty reflexive antisymmetric upper-bounded RelStr st b1 is /\-complete holds
b1 is with_suprema
proofend;
end;

registration
cluster non empty strict V58() reflexive transitive antisymmetric with_suprema with_infima complete for RelStr ;
existence
 ex b1 being LATTICE st
( b1 is complete &amp; b1 is strict )
proofend;
end;