:: WAYBEL_3 semantic presentation

begin

definition
let L be non empty reflexive RelStr ;
let x, y be Element of L;
predx is_way_below y means :Def1: :: WAYBEL_3:def 1
 for D being non empty directed Subset of L st y <= sup D holds
ex d being Element of L st
( d in D & x <= d );
end;

:: deftheorem Def1 defines is_way_below WAYBEL_3:def_1_:_
 for L being non empty reflexive RelStr
for x, y being Element of L holds
( x is_way_below y iff for D being non empty directed Subset of L st y <= sup D holds
ex d being Element of L st
( d in D & x <= d ) );

notation
let L be non empty reflexive RelStr ;
let x, y be Element of L;
synonym x << y for x is_way_below y;
synonym y >> x for x is_way_below y;
end;

definition
let L be non empty reflexive RelStr ;
let x be Element of L;
attrx is compact  means :Def2: :: WAYBEL_3:def 2
x is_way_below x;
end;

:: deftheorem Def2 defines compact WAYBEL_3:def_2_:_
 for L being non empty reflexive RelStr
for x being Element of L holds
( x is compact iff x is_way_below x );

notation
let L be non empty reflexive RelStr ;
let x be Element of L;
synonym  isolated_from_below x for  compact ;
end;

theorem Th1: :: WAYBEL_3:1
for L being non empty reflexive antisymmetric RelStr
for x, y being Element of L st x << y holds
x <= y
proof
let L be non empty reflexive antisymmetric RelStr ; ::_thesis: for x, y being Element of L st x << y holds
x <= y
let x, y be Element of L; ::_thesis: ( x << y implies x <= y )
assume A1: for D being non empty directed Subset of L st y <= sup D holds
ex d being Element of L st
( d in D & x <= d ) ; :: according to WAYBEL_3:def_1 ::_thesis: x <= y
A2: {y} is directed by WAYBEL_0:5;
 sup {y} = y by YELLOW_0:39;
then  ex d being Element of L st
( d in {y} & x <= d ) by A1, A2;
hence  x <= y by TARSKI:def_1; ::_thesis: verum
end;

theorem Th2: :: WAYBEL_3:2
for L being non empty reflexive transitive RelStr
for u, x, y, z being Element of L st u <= x & x << y & y <= z holds
u << z
proof
let L be non empty reflexive transitive RelStr ; ::_thesis: for u, x, y, z being Element of L st u <= x & x << y & y <= z holds
u << z
let u, x, y, z be Element of L; ::_thesis: ( u <= x & x << y & y <= z implies u << z )
assume that
A1: u <= x and
A2: for D being non empty directed Subset of L st y <= sup D holds
ex d being Element of L st
( d in D & x <= d ) and
A3: y <= z ; :: according to WAYBEL_3:def_1 ::_thesis: u << z
let D be non empty directed Subset of L; :: according to WAYBEL_3:def_1 ::_thesis: ( z <= sup D implies ex d being Element of L st
( d in D & u <= d ) )
assume  z <= sup D ; ::_thesis: ex d being Element of L st
( d in D & u <= d )
then  y <= sup D by A3, ORDERS_2:3;
then consider d being Element of L such that
A4: d in D and
A5: x <= d by A2;
take  d ; ::_thesis: ( d in D & u <= d )
thus  ( d in D & u <= d ) by A1, A4, A5, ORDERS_2:3; ::_thesis: verum
end;

theorem Th3: :: WAYBEL_3:3
for L being non empty Poset st ( L is with_suprema or L is /\-complete ) holds
for x, y, z being Element of L st x << z & y << z holds
( ex_sup_of {x,y},L & x "\/" y << z )
proof
let L be non empty Poset; ::_thesis: ( ( L is with_suprema or L is /\-complete ) implies for x, y, z being Element of L st x << z & y << z holds
( ex_sup_of {x,y},L & x "\/" y << z ) )
assume A1: ( L is with_suprema or L is /\-complete ) ; ::_thesis: for x, y, z being Element of L st x << z & y << z holds
( ex_sup_of {x,y},L & x "\/" y << z )
let x, y, z be Element of L; ::_thesis: ( x << z & y << z implies ( ex_sup_of {x,y},L & x "\/" y << z ) )
assume A2: z >> x ; ::_thesis: ( not y << z or ( ex_sup_of {x,y},L & x "\/" y << z ) )
then A3: z >= x by Th1;
assume A4: z >> y ; ::_thesis: ( ex_sup_of {x,y},L & x "\/" y << z )
then A5: z >= y by Th1;
hereby  ::_thesis: x "\/" y << z
percases ( L is with_suprema or L is /\-complete ) by A1;
suppose L is with_suprema ; ::_thesis: ex_sup_of {x,y},L
hence  ex_sup_of {x,y},L by YELLOW_0:20; ::_thesis: verum
end;
supposeA7: L is /\-complete ; ::_thesis: ex_sup_of {x,y},L
set X =  {  a where a is Element of L : ( a >= x & a >= y )  }  ;
  {  a where a is Element of L : ( a >= x & a >= y )  }  c= the carrier of L
proof
let a be set ; :: according to TARSKI:def_3 ::_thesis: ( not a in  {  a where a is Element of L : ( a >= x & a >= y )  }  or a in the carrier of L )
assume  a in  {  a where a is Element of L : ( a >= x & a >= y )  }  ; ::_thesis: a in the carrier of L
then  ex z being Element of L st
( a = z & z >= x & z >= y ) ;
hence  a in the carrier of L ; ::_thesis: verum
end;
then reconsider X =  {  a where a is Element of L : ( a >= x & a >= y )  }  as Subset of L ;
 z in X by A3, A5;
then  ex_inf_of X,L by A7, WAYBEL_0:76;
then consider c being Element of L such that
A8: c is_<=_than X and
A9: for d being Element of L st d is_<=_than X holds
d <= c by YELLOW_0:16;
A10: c is_>=_than {x,y}
proof
let a be Element of L; :: according to LATTICE3:def_9 ::_thesis: ( not a in {x,y} or a <= c )
assume A11: a in {x,y} ; ::_thesis: a <= c
 a is_<=_than X
proof
let b be Element of L; :: according to LATTICE3:def_8 ::_thesis: ( not b in X or a <= b )
assume  b in X ; ::_thesis: a <= b
then  ex z being Element of L st
( b = z & z >= x & z >= y ) ;
hence  a <= b by A11, TARSKI:def_2; ::_thesis: verum
end;
hence  a <= c by A9; ::_thesis: verum
end;
now__::_thesis:_for_a_being_Element_of_L_st_a_is_>=_than_{x,y}_holds_
c_<=_a
let a be Element of L; ::_thesis: ( a is_>=_than {x,y} implies c <= a )
assume A12: a is_>=_than {x,y} ; ::_thesis: c <= a
then A13: a >= x by YELLOW_0:8;
 a >= y by A12, YELLOW_0:8;
then  a in X by A13;
hence  c <= a by A8, LATTICE3:def_8; ::_thesis: verum
end;
hence  ex_sup_of {x,y},L by A10, YELLOW_0:15; ::_thesis: verum
end;
end;
end;
let D be non empty directed Subset of L; :: according to WAYBEL_3:def_1 ::_thesis: ( z <= sup D implies ex d being Element of L st
( d in D & x "\/" y <= d ) )
assume A14: z <= sup D ; ::_thesis: ex d being Element of L st
( d in D & x "\/" y <= d )
then consider d1 being Element of L such that
A15: d1 in D and
A16: x <= d1 by A2, Def1;
consider d2 being Element of L such that
A17: d2 in D and
A18: y <= d2 by A4, A14, Def1;
consider d being Element of L such that
A19: d in D and
A20: d1 <= d and
A21: d2 <= d by A15, A17, WAYBEL_0:def_1;
A22: x <= d by A16, A20, ORDERS_2:3;
A23: y <= d by A18, A21, ORDERS_2:3;
take  d ; ::_thesis: ( d in D & x "\/" y <= d )
thus  ( d in D & x "\/" y <= d ) by A6, A19, A22, A23, YELLOW_0:18; ::_thesis: verum
end;

theorem Th4: :: WAYBEL_3:4
for L being non empty reflexive antisymmetric lower-bounded RelStr
for x being Element of L holds Bottom L << x
proof
let L be non empty reflexive antisymmetric lower-bounded RelStr ; ::_thesis: for x being Element of L holds Bottom L << x
let x be Element of L; ::_thesis: Bottom L << x
let D be non empty directed Subset of L; :: according to WAYBEL_3:def_1 ::_thesis: ( x <= sup D implies ex d being Element of L st
( d in D & Bottom L <= d ) )
assume  x <= sup D ; ::_thesis: ex d being Element of L st
( d in D & Bottom L <= d )
set d = the Element of D;
reconsider d = the Element of D as Element of L ;
take  d ; ::_thesis: ( d in D & Bottom L <= d )
thus  ( d in D & Bottom L <= d ) by YELLOW_0:44; ::_thesis: verum
end;

theorem :: WAYBEL_3:5
for L being non empty Poset
for x, y, z being Element of L st x << y & y << z holds
x << z
proof
let L be non empty Poset; ::_thesis: for x, y, z being Element of L st x << y & y << z holds
x << z
let x, y, z be Element of L; ::_thesis: ( x << y & y << z implies x << z )
assume  x << y ; ::_thesis: ( not y << z or x << z )
then  x <= y by Th1;
hence  ( not y << z or x << z ) by Th2; ::_thesis: verum
end;

theorem :: WAYBEL_3:6
for L being non empty reflexive antisymmetric RelStr
for x, y being Element of L st x << y & x >> y holds
x = y
proof
let L be non empty reflexive antisymmetric RelStr ; ::_thesis: for x, y being Element of L st x << y & x >> y holds
x = y
let x, y be Element of L; ::_thesis: ( x << y & x >> y implies x = y )
assume that
A1: x << y and
A2: x >> y ; ::_thesis: x = y
A3: x <= y by A1, Th1;
 y <= x by A2, Th1;
hence  x = y by A3, ORDERS_2:2; ::_thesis: verum
end;

definition
let L be non empty reflexive RelStr ;
let x be Element of L;
A1:  {  y where y is Element of L : y << x  }  c= the carrier of L
proof
let z be set ; :: according to TARSKI:def_3 ::_thesis: ( not z in  {  y where y is Element of L : y << x  }  or z in the carrier of L )
assume  z in  {  y where y is Element of L : y << x  }  ; ::_thesis: z in the carrier of L
then  ex y being Element of L st
( z = y & y << x ) ;
hence  z in the carrier of L ; ::_thesis: verum
end;
func waybelow x ->  Subset of L equals :: WAYBEL_3:def 3
 {  y where y is Element of L : y << x  }  ;
correctness
coherence
{  y where y is Element of L : y << x  }  is Subset of L;
by A1;
A2:  {  y where y is Element of L : y >> x  }  c= the carrier of L
proof
let z be set ; :: according to TARSKI:def_3 ::_thesis: ( not z in  {  y where y is Element of L : y >> x  }  or z in the carrier of L )
assume  z in  {  y where y is Element of L : y >> x  }  ; ::_thesis: z in the carrier of L
then  ex y being Element of L st
( z = y & y >> x ) ;
hence  z in the carrier of L ; ::_thesis: verum
end;
func wayabove x ->  Subset of L equals :: WAYBEL_3:def 4
 {  y where y is Element of L : y >> x  }  ;
correctness
coherence
{  y where y is Element of L : y >> x  }  is Subset of L;
by A2;
end;

:: deftheorem  defines waybelow WAYBEL_3:def_3_:_
 for L being non empty reflexive RelStr
for x being Element of L holds waybelow x =  {  y where y is Element of L : y << x  }  ;

:: deftheorem  defines wayabove WAYBEL_3:def_4_:_
 for L being non empty reflexive RelStr
for x being Element of L holds wayabove x =  {  y where y is Element of L : y >> x  }  ;

theorem Th7: :: WAYBEL_3:7
for L being non empty reflexive RelStr
for x, y being Element of L holds
( x in waybelow y iff x << y )
proof
let L be non empty reflexive RelStr ; ::_thesis: for x, y being Element of L holds
( x in waybelow y iff x << y )
let x, y be Element of L; ::_thesis: ( x in waybelow y iff x << y )
 ( x in waybelow y iff ex z being Element of L st
( x = z & z << y ) ) ;
hence  ( x in waybelow y iff x << y ) ; ::_thesis: verum
end;

theorem Th8: :: WAYBEL_3:8
for L being non empty reflexive RelStr
for x, y being Element of L holds
( x in wayabove y iff x >> y )
proof
let L be non empty reflexive RelStr ; ::_thesis: for x, y being Element of L holds
( x in wayabove y iff x >> y )
let x, y be Element of L; ::_thesis: ( x in wayabove y iff x >> y )
 ( x in wayabove y iff ex z being Element of L st
( x = z & z >> y ) ) ;
hence  ( x in wayabove y iff x >> y ) ; ::_thesis: verum
end;

theorem Th9: :: WAYBEL_3:9
for L being non empty reflexive antisymmetric RelStr
for x being Element of L holds x is_>=_than waybelow x
proof
let L be non empty reflexive antisymmetric RelStr ; ::_thesis: for x being Element of L holds x is_>=_than waybelow x
let x, y be Element of L; :: according to LATTICE3:def_9 ::_thesis: ( not y in waybelow x or y <= x )
assume  y in waybelow x ; ::_thesis: y <= x
then  y << x by Th7;
hence  y <= x by Th1; ::_thesis: verum
end;

theorem :: WAYBEL_3:10
for L being non empty reflexive antisymmetric RelStr
for x being Element of L holds x is_<=_than wayabove x
proof
let L be non empty reflexive antisymmetric RelStr ; ::_thesis: for x being Element of L holds x is_<=_than wayabove x
let x, y be Element of L; :: according to LATTICE3:def_8 ::_thesis: ( not y in wayabove x or x <= y )
assume  y in wayabove x ; ::_thesis: x <= y
then  y >> x by Th8;
hence  x <= y by Th1; ::_thesis: verum
end;

theorem Th11: :: WAYBEL_3:11
for L being non empty reflexive antisymmetric RelStr
for x being Element of L holds
( waybelow x c= downarrow x & wayabove x c= uparrow x )
proof
let L be non empty reflexive antisymmetric RelStr ; ::_thesis: for x being Element of L holds
( waybelow x c= downarrow x & wayabove x c= uparrow x )
let x be Element of L; ::_thesis: ( waybelow x c= downarrow x & wayabove x c= uparrow x )
hereby  :: according to TARSKI:def_3 ::_thesis: wayabove x c= uparrow x
let a be set ; ::_thesis: ( a in waybelow x implies a in downarrow x )
assume  a in waybelow x ; ::_thesis: a in downarrow x
then consider y being Element of L such that
A1: a = y and
A2: y << x ;
 y <= x by A2, Th1;
hence  a in downarrow x by A1, WAYBEL_0:17; ::_thesis: verum
end;
let a be set ; :: according to TARSKI:def_3 ::_thesis: ( not a in wayabove x or a in uparrow x )
assume  a in wayabove x ; ::_thesis: a in uparrow x
then consider y being Element of L such that
A3: a = y and
A4: y >> x ;
 x <= y by A4, Th1;
hence  a in uparrow x by A3, WAYBEL_0:18; ::_thesis: verum
end;

theorem Th12: :: WAYBEL_3:12
for L being non empty reflexive transitive RelStr
for x, y being Element of L st x <= y holds
( waybelow x c= waybelow y & wayabove y c= wayabove x )
proof
let L be non empty reflexive transitive RelStr ; ::_thesis: for x, y being Element of L st x <= y holds
( waybelow x c= waybelow y & wayabove y c= wayabove x )
let x, y be Element of L; ::_thesis: ( x <= y implies ( waybelow x c= waybelow y & wayabove y c= wayabove x ) )
assume A1: x <= y ; ::_thesis: ( waybelow x c= waybelow y & wayabove y c= wayabove x )
hereby  :: according to TARSKI:def_3 ::_thesis: wayabove y c= wayabove x
let z be set ; ::_thesis: ( z in waybelow x implies z in waybelow y )
assume  z in waybelow x ; ::_thesis: z in waybelow y
then consider v being Element of L such that
A2: z = v and
A3: v << x ;
 v << y by A1, A3, Th2;
hence  z in waybelow y by A2; ::_thesis: verum
end;
let z be set ; :: according to TARSKI:def_3 ::_thesis: ( not z in wayabove y or z in wayabove x )
assume  z in wayabove y ; ::_thesis: z in wayabove x
then consider v being Element of L such that
A4: z = v and
A5: v >> y ;
 v >> x by A1, A5, Th2;
hence  z in wayabove x by A4; ::_thesis: verum
end;

registration
let L be non empty reflexive antisymmetric lower-bounded RelStr ;
let x be Element of L;
cluster waybelow x ->  non empty ;
coherence
 not waybelow x is empty
proof
 Bottom L << x by Th4;
hence  not waybelow x is empty by Th7; ::_thesis: verum
end;
end;

registration
let L be non empty reflexive transitive RelStr ;
let x be Element of L;
cluster waybelow x ->  lower ;
coherence
 waybelow x is lower
proof
let z, y be Element of L; :: according to WAYBEL_0:def_19 ::_thesis: ( not z in waybelow x or not y <= z or y in waybelow x )
assume  z in waybelow x ; ::_thesis: ( not y <= z or y in waybelow x )
then  z << x by Th7;
then  ( y <= z implies y << x ) by Th2;
hence  ( y <= z implies y in waybelow x ) ; ::_thesis: verum
end;
cluster wayabove x ->  upper ;
coherence
 wayabove x is upper
proof
hereby  :: according to WAYBEL_0:def_20 ::_thesis: verum
let z, y be Element of L; ::_thesis: ( z in wayabove x & y >= z implies y in wayabove x )
assume  z in wayabove x ; ::_thesis: ( y >= z implies y in wayabove x )
then  z >> x by Th8;
then  ( y >= z implies y >> x ) by Th2;
hence  ( y >= z implies y in wayabove x ) ; ::_thesis: verum
end;
end;
end;

registration
let L be sup-Semilattice;
let x be Element of L;
cluster waybelow x ->  directed ;
coherence
 waybelow x is directed
proof
let v, y be Element of L; :: according to WAYBEL_0:def_1 ::_thesis: ( not v in waybelow x or not y in waybelow x or ex b1 being Element of the carrier of L st
( b1 in waybelow x & v <= b1 & y <= b1 ) )
assume that
A1: v in waybelow x and
A2: y in waybelow x ; ::_thesis: ex b1 being Element of the carrier of L st
( b1 in waybelow x & v <= b1 & y <= b1 )
A3: v << x by A1, Th7;
A4: y << x by A2, Th7;
then A5: ex_sup_of {v,y},L by A3, Th3;
take z = v "\/" y; ::_thesis: ( z in waybelow x & v <= z & y <= z )
 z << x by A3, A4, Th3;
hence  z in waybelow x ; ::_thesis: ( v <= z & y <= z )
thus  ( v <= z & y <= z ) by A5, YELLOW_0:18; ::_thesis: verum
end;
end;

registration
let L be non empty /\-complete Poset;
let x be Element of L;
cluster waybelow x ->  directed ;
coherence
 waybelow x is directed
proof
let v, y be Element of L; :: according to WAYBEL_0:def_1 ::_thesis: ( not v in waybelow x or not y in waybelow x or ex b1 being Element of the carrier of L st
( b1 in waybelow x & v <= b1 & y <= b1 ) )
assume that
A1: v in waybelow x and
A2: y in waybelow x ; ::_thesis: ex b1 being Element of the carrier of L st
( b1 in waybelow x & v <= b1 & y <= b1 )
A3: v << x by A1, Th7;
A4: y << x by A2, Th7;
then A5: ex_sup_of {v,y},L by A3, Th3;
take z = v "\/" y; ::_thesis: ( z in waybelow x & v <= z & y <= z )
 z << x by A3, A4, Th3;
hence  z in waybelow x ; ::_thesis: ( v <= z & y <= z )
thus  ( v <= z & y <= z ) by A5, YELLOW_0:18; ::_thesis: verum
end;
end;

registration
let L be non empty connected RelStr ;
cluster  ->  directed filtered for Element of K10( the carrier of L);
coherence
 for b1 being Subset of L holds
( b1 is directed & b1 is filtered )
proof
let X be Subset of L; ::_thesis: ( X is directed & X is filtered )
thus  X is directed ::_thesis: X is filtered
proof
let x, y be Element of L; :: according to WAYBEL_0:def_1 ::_thesis: ( not x in X or not y in X or ex b1 being Element of the carrier of L st
( b1 in X & x <= b1 & y <= b1 ) )
 ( ( x <= y & y <= y ) or ( x >= x & x >= y ) ) by WAYBEL_0:def_29;
hence  ( not x in X or not y in X or ex b1 being Element of the carrier of L st
( b1 in X & x <= b1 & y <= b1 ) ) ; ::_thesis: verum
end;
let x, y be Element of L; :: according to WAYBEL_0:def_2 ::_thesis: ( not x in X or not y in X or ex b1 being Element of the carrier of L st
( b1 in X & b1 <= x & b1 <= y ) )
 ( ( x >= y & y <= y ) or ( x >= x & x <= y ) ) by WAYBEL_0:def_29;
hence  ( not x in X or not y in X or ex b1 being Element of the carrier of L st
( b1 in X & b1 <= x & b1 <= y ) ) ; ::_thesis: verum
end;
end;

registration
cluster non empty reflexive transitive antisymmetric lower-bounded connected up-complete  ->  complete for RelStr ;
coherence
 for b1 being Chain st b1 is up-complete & b1 is lower-bounded holds
b1 is complete
proof
let L be Chain; ::_thesis: ( L is up-complete & L is lower-bounded implies L is complete )
assume A1: ( L is up-complete & L is lower-bounded ) ; ::_thesis: L is complete
now__::_thesis:_for_X_being_Subset_of_L_holds_ex_sup_of_X,L
let X be Subset of L; ::_thesis: ex_sup_of X,L
 ( X = {} or X <> {} ) ;
hence  ex_sup_of X,L by A1, WAYBEL_0:75, YELLOW_0:42; ::_thesis: verum
end;
hence  L is complete by YELLOW_0:53; ::_thesis: verum
end;
end;

registration
cluster non empty V233() reflexive transitive antisymmetric complete connected for RelStr ;
existence
 ex b1 being Chain st b1 is complete
proof
set x = the set ;
set O = the Order of { the set };
 RelStr(# { the set }, the Order of { the set } #) is 1 -element RelStr ;
hence  ex b1 being Chain st b1 is complete ; ::_thesis: verum
end;
end;

theorem Th13: :: WAYBEL_3:13
for L being up-complete Chain
for x, y being Element of L st x < y holds
x << y
proof
let L be up-complete Chain; ::_thesis: for x, y being Element of L st x < y holds
x << y
let x, y be Element of L; ::_thesis: ( x < y implies x << y )
assume that
A1: x <= y and
A2: x <> y ; :: according to ORDERS_2:def_6 ::_thesis: x << y
let D be non empty directed Subset of L; :: according to WAYBEL_3:def_1 ::_thesis: ( y <= sup D implies ex d being Element of L st
( d in D & x <= d ) )
assume that
A3: y <= sup D and
A4: for d being Element of L st d in D holds
not x <= d ; ::_thesis: contradiction
A5: ex_sup_of D,L by WAYBEL_0:75;
 x is_>=_than D
proof
let z be Element of L; :: according to LATTICE3:def_9 ::_thesis: ( not z in D or z <= x )
assume  z in D ; ::_thesis: z <= x
then  not x <= z by A4;
hence  z <= x by WAYBEL_0:def_29; ::_thesis: verum
end;
then  x >= sup D by A5, YELLOW_0:def_9;
then  x >= y by A3, ORDERS_2:3;
hence  contradiction by A1, A2, ORDERS_2:2; ::_thesis: verum
end;

theorem :: WAYBEL_3:14
for L being non empty reflexive antisymmetric RelStr
for x, y being Element of L st not x is compact & x << y holds
x < y
proof
let L be non empty reflexive antisymmetric RelStr ; ::_thesis: for x, y being Element of L st not x is compact & x << y holds
x < y
let x, y be Element of L; ::_thesis: ( not x is compact & x << y implies x < y )
assume that
A1: not x << x and
A2: x << y ; :: according to WAYBEL_3:def_2 ::_thesis: x < y
thus  ( x <= y & x <> y ) by A1, A2, Th1; :: according to ORDERS_2:def_6 ::_thesis: verum
end;

theorem :: WAYBEL_3:15
for L being non empty reflexive antisymmetric lower-bounded RelStr holds Bottom L is compact
proof
let L be non empty reflexive antisymmetric lower-bounded RelStr ; ::_thesis: Bottom L is compact
thus  Bottom L << Bottom L by Th4; :: according to WAYBEL_3:def_2 ::_thesis: verum
end;

theorem Th16: :: WAYBEL_3:16
for L being non empty up-complete Poset
for D being non empty finite directed Subset of L holds sup D in D
proof
let L be non empty up-complete Poset; ::_thesis: for D being non empty finite directed Subset of L holds sup D in D
let D be non empty finite directed Subset of L; ::_thesis: sup D in D
 D c= D ;
then consider d being Element of L such that
A1: d in D and
A2: d is_>=_than D by WAYBEL_0:1;
A3: ex_sup_of D,L by WAYBEL_0:75;
then A4: sup D is_>=_than D by YELLOW_0:30;
A5: sup D <= d by A2, A3, YELLOW_0:30;
 sup D >= d by A1, A4, LATTICE3:def_9;
hence  sup D in D by A1, A5, ORDERS_2:2; ::_thesis: verum
end;

theorem :: WAYBEL_3:17
for L being non empty up-complete Poset st L is finite holds
for x being Element of L holds x is isolated_from_below
proof
let L be non empty up-complete Poset; ::_thesis: ( L is finite implies for x being Element of L holds x is isolated_from_below )
assume A1: the carrier of L is finite ; :: according to STRUCT_0:def_11 ::_thesis: for x being Element of L holds x is isolated_from_below
let x be Element of L; ::_thesis: x is isolated_from_below
let D be non empty directed Subset of L; :: according to WAYBEL_3:def_1,WAYBEL_3:def_2 ::_thesis: ( x <= sup D implies ex d being Element of L st
( d in D & x <= d ) )
assume  x <= sup D ; ::_thesis: ex d being Element of L st
( d in D & x <= d )
hence  ex d being Element of L st
( d in D & x <= d ) by A1, Th16; ::_thesis: verum
end;

begin

theorem Th18: :: WAYBEL_3:18
for L being complete LATTICE
for x, y being Element of L st x << y holds
for X being Subset of L st y <= sup X holds
ex A being finite Subset of L st
( A c= X & x <= sup A )
proof
let L be complete LATTICE; ::_thesis: for x, y being Element of L st x << y holds
for X being Subset of L st y <= sup X holds
ex A being finite Subset of L st
( A c= X & x <= sup A )
let x, y be Element of L; ::_thesis: ( x << y implies for X being Subset of L st y <= sup X holds
ex A being finite Subset of L st
( A c= X & x <= sup A ) )
assume A1: x << y ; ::_thesis: for X being Subset of L st y <= sup X holds
ex A being finite Subset of L st
( A c= X & x <= sup A )
let X be Subset of L; ::_thesis: ( y <= sup X implies ex A being finite Subset of L st
( A c= X & x <= sup A ) )
assume A2: y <= sup X ; ::_thesis: ex A being finite Subset of L st
( A c= X & x <= sup A )
defpred S1[ set ] means  ex Y being finite Subset of X st
( ex_sup_of Y,L & $1 = "\/" (Y,L) );
consider F being Subset of L such that
A3: for a being Element of L holds
( a in F iff S1[a] ) from SUBSET_1:sch_3();
A4: now__::_thesis:_for_Y_being_finite_Subset_of_X_st_Y_<>_{}_holds_
"\/"_(Y,L)_in_F
let Y be finite Subset of X; ::_thesis: ( Y <> {} implies "\/" (Y,L) in F )
assume  Y <> {} ; ::_thesis: "\/" (Y,L) in F
 ex_sup_of Y,L by YELLOW_0:17;
hence  "\/" (Y,L) in F by A3; ::_thesis: verum
end;
A5: for Y being finite Subset of X st Y <> {} holds
ex_sup_of Y,L by YELLOW_0:17;
A6: {} c= X by XBOOLE_1:2;
 ex_sup_of {} ,L by YELLOW_0:17;
then  "\/" ({},L) in F by A3, A6;
then reconsider F = F as non empty directed Subset of L by A3, A4, A5, WAYBEL_0:51;
 ex_sup_of X,L by YELLOW_0:17;
then  sup X = sup F by A3, A4, A5, WAYBEL_0:54;
then consider d being Element of L such that
A7: d in F and
A8: x <= d by A1, A2, Def1;
consider Y being finite Subset of X such that
 ex_sup_of Y,L and
A9: d = "\/" (Y,L) by A3, A7;
reconsider Y = Y as finite Subset of L by XBOOLE_1:1;
take  Y ; ::_thesis: ( Y c= X & x <= sup Y )
thus  ( Y c= X & x <= sup Y ) by A8, A9; ::_thesis: verum
end;

theorem :: WAYBEL_3:19
for L being complete LATTICE
for x, y being Element of L st ( for X being Subset of L st y <= sup X holds
ex A being finite Subset of L st
( A c= X & x <= sup A ) ) holds
x << y
proof
let L be complete LATTICE; ::_thesis: for x, y being Element of L st ( for X being Subset of L st y <= sup X holds
ex A being finite Subset of L st
( A c= X & x <= sup A ) ) holds
x << y
let x, y be Element of L; ::_thesis: ( ( for X being Subset of L st y <= sup X holds
ex A being finite Subset of L st
( A c= X & x <= sup A ) ) implies x << y )
assume A1: for X being Subset of L st y <= sup X holds
ex A being finite Subset of L st
( A c= X & x <= sup A ) ; ::_thesis: x << y
let D be non empty directed Subset of L; :: according to WAYBEL_3:def_1 ::_thesis: ( y <= sup D implies ex d being Element of L st
( d in D & x <= d ) )
assume  y <= sup D ; ::_thesis: ex d being Element of L st
( d in D & x <= d )
then consider A being finite Subset of L such that
A2: A c= D and
A3: x <= sup A by A1;
reconsider B = A as finite Subset of D by A2;
consider a being Element of L such that
A4: a in D and
A5: a is_>=_than B by WAYBEL_0:1;
take  a ; ::_thesis: ( a in D & x <= a )
 a >= sup A by A5, YELLOW_0:32;
hence  ( a in D & x <= a ) by A3, A4, YELLOW_0:def_2; ::_thesis: verum
end;

theorem :: WAYBEL_3:20
for L being non empty reflexive transitive RelStr
for x, y being Element of L st x << y holds
for I being Ideal of L st y <= sup I holds
x in I
proof
let L be non empty reflexive transitive RelStr ; ::_thesis: for x, y being Element of L st x << y holds
for I being Ideal of L st y <= sup I holds
x in I
let x, y be Element of L; ::_thesis: ( x << y implies for I being Ideal of L st y <= sup I holds
x in I )
assume A1: x << y ; ::_thesis: for I being Ideal of L st y <= sup I holds
x in I
let I be Ideal of L; ::_thesis: ( y <= sup I implies x in I )
assume  y <= sup I ; ::_thesis: x in I
then  ex d being Element of L st
( d in I & x <= d ) by A1, Def1;
hence  x in I by WAYBEL_0:def_19; ::_thesis: verum
end;

theorem Th21: :: WAYBEL_3:21
for L being non empty up-complete Poset
for x, y being Element of L st ( for I being Ideal of L st y <= sup I holds
x in I ) holds
x << y
proof
let L be non empty up-complete Poset; ::_thesis: for x, y being Element of L st ( for I being Ideal of L st y <= sup I holds
x in I ) holds
x << y
let x, y be Element of L; ::_thesis: ( ( for I being Ideal of L st y <= sup I holds
x in I ) implies x << y )
assume A1: for I being Ideal of L st y <= sup I holds
x in I ; ::_thesis: x << y
let D be non empty directed Subset of L; :: according to WAYBEL_3:def_1 ::_thesis: ( y <= sup D implies ex d being Element of L st
( d in D & x <= d ) )
assume A2: y <= sup D ; ::_thesis: ex d being Element of L st
( d in D & x <= d )
 ex_sup_of D,L by WAYBEL_0:75;
then  sup D = sup (downarrow D) by WAYBEL_0:33;
then  x in downarrow D by A1, A2;
then  ex d being Element of L st
( x <= d & d in D ) by WAYBEL_0:def_15;
hence  ex d being Element of L st
( d in D & x <= d ) ; ::_thesis: verum
end;

theorem :: WAYBEL_3:22
for L being lower-bounded LATTICE st L is meet-continuous holds
for x, y being Element of L holds
( x << y iff for I being Ideal of L st y = sup I holds
x in I )
proof
let L be lower-bounded LATTICE; ::_thesis: ( L is meet-continuous implies for x, y being Element of L holds
( x << y iff for I being Ideal of L st y = sup I holds
x in I ) )
assume A1: ( L is up-complete & L is satisfying_MC ) ; :: according to WAYBEL_2:def_7 ::_thesis: for x, y being Element of L holds
( x << y iff for I being Ideal of L st y = sup I holds
x in I )
let x, y be Element of L; ::_thesis: ( x << y iff for I being Ideal of L st y = sup I holds
x in I )
hereby  ::_thesis: ( ( for I being Ideal of L st y = sup I holds
x in I ) implies x << y )
assume A2: x << y ; ::_thesis: for I being Ideal of L st y = sup I holds
x in I
let I be Ideal of L; ::_thesis: ( y = sup I implies x in I )
assume  y = sup I ; ::_thesis: x in I
then  ex d being Element of L st
( d in I & x <= d ) by A2, Def1;
hence  x in I by WAYBEL_0:def_19; ::_thesis: verum
end;
assume A3: for I being Ideal of L st y = sup I holds
x in I ; ::_thesis: x << y
now__::_thesis:_for_I_being_Ideal_of_L_st_y_<=_sup_I_holds_
x_in_I
let I be Ideal of L; ::_thesis: ( y <= sup I implies x in I )
A4: ex_sup_of finsups ({y} "/\" I),L by A1, WAYBEL_0:75;
assume  y <= sup I ; ::_thesis: x in I
then  y "/\" (sup I) = y by YELLOW_0:25;
then y = sup ({y} "/\" I) by A1, WAYBEL_2:def_6
.= sup (finsups ({y} "/\" I)) by A1, WAYBEL_0:55
.= sup (downarrow (finsups ({y} "/\" I))) by A4, WAYBEL_0:33 ;
then  x in downarrow (finsups ({y} "/\" I)) by A3;
then consider z being Element of L such that
A5: x <= z and
A6: z in finsups ({y} "/\" I) by WAYBEL_0:def_15;
consider Y being finite Subset of ({y} "/\" I) such that
A7: z = "\/" (Y,L) and
 ex_sup_of Y,L by A6;
set i = the Element of I;
reconsider i = the Element of I as Element of L ;
A8: ex_sup_of {i},L by YELLOW_0:38;
A9: sup {i} = i by YELLOW_0:39;
 ex_sup_of {} ,L by A1, YELLOW_0:17;
then  "\/" ({},L) <= sup {i} by A8, XBOOLE_1:2, YELLOW_0:34;
then A10: "\/" ({},L) in I by A9, WAYBEL_0:def_19;
 Y c= I
proof
let a be set ; :: according to TARSKI:def_3 ::_thesis: ( not a in Y or a in I )
assume  a in Y ; ::_thesis: a in I
then  a in {y} "/\" I ;
then  a in  {  (y "/\" j) where j is Element of L : j in I  }  by YELLOW_4:42;
then consider j being Element of L such that
A11: a = y "/\" j and
A12: j in I ;
 y "/\" j <= j by YELLOW_0:23;
hence  a in I by A11, A12, WAYBEL_0:def_19; ::_thesis: verum
end;
then  z in I by A7, A10, WAYBEL_0:42;
hence  x in I by A5, WAYBEL_0:def_19; ::_thesis: verum
end;
hence  x << y by A1, Th21; ::_thesis: verum
end;

theorem :: WAYBEL_3:23
for L being complete LATTICE holds
( ( for x being Element of L holds x is compact ) iff for X being non empty Subset of L ex x being Element of L st
( x in X & ( for y being Element of L st y in X holds
not x < y ) ) )
proof
let L be complete LATTICE; ::_thesis: ( ( for x being Element of L holds x is compact ) iff for X being non empty Subset of L ex x being Element of L st
( x in X & ( for y being Element of L st y in X holds
not x < y ) ) )
hereby  ::_thesis: ( ( for X being non empty Subset of L ex x being Element of L st
( x in X & ( for y being Element of L st y in X holds
not x < y ) ) ) implies for x being Element of L holds x is compact )
assume A1: for x being Element of L holds x is compact ; ::_thesis: for Y being non empty Subset of L ex x being Element of L st
( x in Y & ( for y being Element of L holds
( not y in Y or not x < y ) ) )
given Y being non empty Subset of L such that A2: for x being Element of L st x in Y holds
ex y being Element of L st
( y in Y & x < y ) ; ::_thesis: contradiction
defpred S1[ set , set ] means ( [$1,$2] in the InternalRel of L & $1 <> $2 );
A3: now__::_thesis:_for_x_being_set_st_x_in_Y_holds_
ex_u_being_set_st_
(_u_in_Y_&_S1[x,u]_)
let x be set ; ::_thesis: ( x in Y implies ex u being set st
( u in Y & S1[x,u] ) )
assume A4: x in Y ; ::_thesis: ex u being set st
( u in Y & S1[x,u] )
then reconsider y = x as Element of L ;
consider z being Element of L such that
A5: z in Y and
A6: y < z by A2, A4;
reconsider u = z as set ;
take u = u; ::_thesis: ( u in Y & S1[x,u] )
 y <= z by A6, ORDERS_2:def_6;
hence  ( u in Y & S1[x,u] ) by A5, A6, ORDERS_2:def_5; ::_thesis: verum
end;
consider f being Function such that
A7: ( dom f = Y & rng f c= Y & ( for x being set st x in Y holds
S1[x,f . x] ) ) from FUNCT_1:sch_5(A3);
set x = the Element of Y;
set x1 = the Element of Y;
set Z =  {  ((iter (f,n)) . the Element of Y) where n is Element of NAT : verum  }  ;
 f . the Element of Y in rng f by A7, FUNCT_1:def_3;
then  f . the Element of Y in Y by A7;
then reconsider x = the Element of Y, x9 = f . the Element of Y as Element of L ;
A8: [x,(f . x)] in the InternalRel of L by A7;
A9: x <> f . x by A7;
A10: x9 = (iter (f,1)) . x by FUNCT_7:70;
A11: x <= x9 by A8, ORDERS_2:def_5;
A12: x9 in  {  ((iter (f,n)) . the Element of Y) where n is Element of NAT : verum  }  by A10;
A13: x < x9 by A9, A11, ORDERS_2:def_6;
A14:  {  ((iter (f,n)) . the Element of Y) where n is Element of NAT : verum  }  c= Y
proof
let a be set ; :: according to TARSKI:def_3 ::_thesis: ( not a in  {  ((iter (f,n)) . the Element of Y) where n is Element of NAT : verum  }  or a in Y )
assume  a in  {  ((iter (f,n)) . the Element of Y) where n is Element of NAT : verum  }  ; ::_thesis: a in Y
then consider n being Element of NAT  such that
A15: a = (iter (f,n)) . x ;
 dom (iter (f,n)) = Y by A7, FUNCT_7:74;
then A16: a in rng (iter (f,n)) by A15, FUNCT_1:def_3;
 rng (iter (f,n)) c= Y by A7, FUNCT_7:74;
hence  a in Y by A16; ::_thesis: verum
end;
then reconsider Z =  {  ((iter (f,n)) . the Element of Y) where n is Element of NAT : verum  }  as Subset of L by XBOOLE_1:1;
A17: now__::_thesis:_for_i,_k_being_Element_of_NAT_st_i_<=_k_holds_
for_z,_y_being_Element_of_L_st_z_=_(iter_(f,i))_._x_&_y_=_(iter_(f,k))_._x_holds_
z_<=_y
let i be Element of NAT ; ::_thesis: for k being Element of NAT st i <= k holds
for z, y being Element of L st z = (iter (f,i)) . x & y = (iter (f,k)) . x holds
z <= y
defpred S2[ Element of NAT ] means  ex z, y being Element of L st
( z = (iter (f,i)) . x & y = (iter (f,(i + $1))) . x & z <= y );
 (iter (f,i)) . x in Z ;
then A18: S2[ 0 ] ;
A19: for k being Element of NAT st S2[k] holds
S2[k + 1]
proof
let k be Element of NAT ; ::_thesis: ( S2[k] implies S2[k + 1] )
given z, y being Element of L such that A20: z = (iter (f,i)) . x and
A21: y = (iter (f,(i + k))) . x and
A22: z <= y ; ::_thesis: S2[k + 1]
take  z ; ::_thesis: ex y being Element of L st
( z = (iter (f,i)) . x & y = (iter (f,(i + (k + 1)))) . x & z <= y )
A23: rng (iter (f,(i + k))) c= Y by A7, FUNCT_7:74;
A24: dom (iter (f,(i + k))) = Y by A7, FUNCT_7:74;
then A25: y in rng (iter (f,(i + k))) by A21, FUNCT_1:def_3;
then  f . y in rng f by A7, A23, FUNCT_1:def_3;
then  f . y in Y by A7;
then reconsider yy = f . y as Element of L ;
take  yy ; ::_thesis: ( z = (iter (f,i)) . x & yy = (iter (f,(i + (k + 1)))) . x & z <= yy )
thus  z = (iter (f,i)) . x by A20; ::_thesis: ( yy = (iter (f,(i + (k + 1)))) . x & z <= yy )
 iter (f,((k + i) + 1)) = f * (iter (f,(k + i))) by FUNCT_7:71;
hence  yy = (iter (f,(i + (k + 1)))) . x by A21, A24, FUNCT_1:13; ::_thesis: z <= yy
 [y,yy] in the InternalRel of L by A7, A23, A25;
then  y <= yy by ORDERS_2:def_5;
hence  z <= yy by A22, ORDERS_2:3; ::_thesis: verum
end;
A26: for k being Element of NAT holds S2[k] from NAT_1:sch_1(A18, A19);
let k be Element of NAT ; ::_thesis: ( i <= k implies for z, y being Element of L st z = (iter (f,i)) . x & y = (iter (f,k)) . x holds
z <= y )
assume  i <= k ; ::_thesis: for z, y being Element of L st z = (iter (f,i)) . x & y = (iter (f,k)) . x holds
z <= y
then consider n being Nat such that
A27: k = i + n by NAT_1:10;
reconsider n = n as Element of NAT by ORDINAL1:def_12;
A28: ex z, y being Element of L st
( z = (iter (f,i)) . x & y = (iter (f,(i + n))) . x & z <= y ) by A26;
let z, y be Element of L; ::_thesis: ( z = (iter (f,i)) . x & y = (iter (f,k)) . x implies z <= y )
assume that
A29: z = (iter (f,i)) . x and
A30: y = (iter (f,k)) . x ; ::_thesis: z <= y
thus  z <= y by A27, A28, A29, A30; ::_thesis: verum
end;
A31: now__::_thesis:_for_z,_y_being_Element_of_L_holds_
(_not_z_in_Z_or_not_y_in_Z_or_z_<=_y_or_z_>=_y_)
let z, y be Element of L; ::_thesis: ( not z in Z or not y in Z or z <= y or z >= y )
assume  z in Z ; ::_thesis: ( not y in Z or z <= y or z >= y )
then consider k1 being Element of NAT  such that
A32: z = (iter (f,k1)) . x ;
assume  y in Z ; ::_thesis: ( z <= y or z >= y )
then consider k2 being Element of NAT  such that
A33: y = (iter (f,k2)) . x ;
 ( k1 <= k2 or k2 <= k1 ) ;
hence  ( z <= y or z >= y ) by A17, A32, A33; ::_thesis: verum
end;
 sup Z is compact by A1;
then  sup Z << sup Z by Def2;
then consider A being finite Subset of L such that
A34: A c= Z and
A35: sup Z <= sup A by Th18;
A36: now__::_thesis:_not_A_=_{}
assume  A = {} ; ::_thesis: contradiction
then  x is_>=_than A by YELLOW_0:6;
then  sup A <= x by YELLOW_0:32;
then A37: sup A < x9 by A13, ORDERS_2:7;
A38: Z is_<=_than sup Z by YELLOW_0:32;
A39: sup Z < x9 by A35, A37, ORDERS_2:7;
 x9 <= sup Z by A12, A38, LATTICE3:def_9;
hence  contradiction by A39, ORDERS_2:6; ::_thesis: verum
end;
A40: A is finite ;
defpred S2[ set ] means ( $1 <> {} implies "\/" ($1,L) in $1 );
A41: S2[ {} ] ;
A42: now__::_thesis:_for_x,_B_being_set_st_x_in_A_&_B_c=_A_&_S2[B]_holds_
S2[B_\/_{x}]
let x, B be set ; ::_thesis: ( x in A & B c= A & S2[B] implies S2[B \/ {x}] )
assume that
A43: x in A and
A44: B c= A ; ::_thesis: ( S2[B] implies S2[B \/ {x}] )
reconsider x9 = x as Element of L by A43;
assume A45: S2[B] ; ::_thesis: S2[B \/ {x}]
thus  S2[B \/ {x}] ::_thesis: verum
proof
assume  B \/ {x} <> {} ; ::_thesis: "\/" ((B \/ {x}),L) in B \/ {x}
A46: ex_sup_of B,L by YELLOW_0:17;
A47: ex_sup_of {x},L by YELLOW_0:17;
 ex_sup_of B \/ {x},L by YELLOW_0:17;
then A48: "\/" ((B \/ {x}),L) = ("\/" (B,L)) "\/" ("\/" ({x},L)) by A46, A47, YELLOW_0:36;
A49: sup {x9} = x by YELLOW_0:39;
percases ( B = {} or B <> {} ) ;
suppose B = {} ; ::_thesis: "\/" ((B \/ {x}),L) in B \/ {x}
hence  "\/" ((B \/ {x}),L) in B \/ {x} by A49, TARSKI:def_1; ::_thesis: verum
end;
suppose B <> {} ; ::_thesis: "\/" ((B \/ {x}),L) in B \/ {x}
then  "\/" (B,L) in A by A44, A45;
then  ( x9 <= "\/" (B,L) or x9 >= "\/" (B,L) ) by A31, A34, A43;
then  ( ("\/" (B,L)) "\/" x9 = "\/" (B,L) or ( ("\/" (B,L)) "\/" x9 = x9 "\/" ("\/" (B,L)) & x9 "\/" ("\/" (B,L)) = x9 ) ) by YELLOW_0:24;
then  ( "\/" ((B \/ {x}),L) in B or "\/" ((B \/ {x}),L) in {x} ) by A45, A48, A49, TARSKI:def_1;
hence  "\/" ((B \/ {x}),L) in B \/ {x} by XBOOLE_0:def_3; ::_thesis: verum
end;
end;
end;
end;
 S2[A] from FINSET_1:sch_2(A40, A41, A42);
then A50: sup A in Z by A34, A36;
then consider n being Element of NAT  such that
A51: sup A = (iter (f,n)) . x ;
A52: [(sup A),(f . (sup A))] in the InternalRel of L by A7, A14, A50;
A53: sup A <> f . (sup A) by A7, A14, A50;
reconsider xSn = f . (sup A) as Element of L by A52, ZFMISC_1:87;
A54: iter (f,(n + 1)) = f * (iter (f,n)) by FUNCT_7:71;
A55: dom (iter (f,n)) = Y by A7, FUNCT_7:74;
A56: sup A <= xSn by A52, ORDERS_2:def_5;
A57: f . (sup A) = (iter (f,(n + 1))) . x by A51, A54, A55, FUNCT_1:13;
A58: sup A < xSn by A53, A56, ORDERS_2:def_6;
A59: xSn in Z by A57;
 Z is_<=_than sup Z by YELLOW_0:32;
then A60: xSn <= sup Z by A59, LATTICE3:def_9;
 sup Z < xSn by A35, A58, ORDERS_2:7;
hence  contradiction by A60, ORDERS_2:6; ::_thesis: verum
end;
assume A61: for X being non empty Subset of L ex x being Element of L st
( x in X & ( for y being Element of L st y in X holds
not x < y ) ) ; ::_thesis: for x being Element of L holds x is compact
let x be Element of L; ::_thesis: x is compact
let D be non empty directed Subset of L; :: according to WAYBEL_3:def_1,WAYBEL_3:def_2 ::_thesis: ( x <= sup D implies ex d being Element of L st
( d in D & x <= d ) )
consider y being Element of L such that
A62: y in D and
A63: for z being Element of L st z in D holds
not y < z by A61;
 D is_<=_than y
proof
let a be Element of L; :: according to LATTICE3:def_9 ::_thesis: ( not a in D or a <= y )
assume  a in D ; ::_thesis: a <= y
then consider b being Element of L such that
A64: b in D and
A65: a <= b and
A66: y <= b by A62, WAYBEL_0:def_1;
 not y < b by A63, A64;
hence  a <= y by A65, A66, ORDERS_2:def_6; ::_thesis: verum
end;
then A67: sup D <= y by YELLOW_0:32;
 sup D is_>=_than D by YELLOW_0:32;
then  y <= sup D by A62, LATTICE3:def_9;
then  sup D = y by A67, ORDERS_2:2;
hence  ( x <= sup D implies ex d being Element of L st
( d in D & x <= d ) ) by A62; ::_thesis: verum
end;

begin

definition
let L be non empty reflexive RelStr ;
attrL is satisfying_axiom_of_approximation  means :Def5: :: WAYBEL_3:def 5
 for x being Element of L holds x = sup (waybelow x);
end;

:: deftheorem Def5 defines satisfying_axiom_of_approximation WAYBEL_3:def_5_:_
 for L being non empty reflexive RelStr holds
( L is satisfying_axiom_of_approximation iff for x being Element of L holds x = sup (waybelow x) );

registration
cluster1 -element reflexive  -> 1 -element reflexive satisfying_axiom_of_approximation for RelStr ;
coherence
 for b1 being 1 -element reflexive RelStr holds b1 is satisfying_axiom_of_approximation
proof
let L be 1 -element reflexive RelStr ; ::_thesis: L is satisfying_axiom_of_approximation
thus  for x being Element of L holds x = sup (waybelow x) by ZFMISC_1:def_10; :: according to WAYBEL_3:def_5 ::_thesis: verum
end;
end;

definition
let L be non empty reflexive RelStr ;
attrL is continuous  means :Def6: :: WAYBEL_3:def 6
( ( for x being Element of L holds
( not waybelow x is empty & waybelow x is directed ) ) & L is up-complete & L is satisfying_axiom_of_approximation );
end;

:: deftheorem Def6 defines continuous WAYBEL_3:def_6_:_
 for L being non empty reflexive RelStr holds
( L is continuous iff ( ( for x being Element of L holds
( not waybelow x is empty & waybelow x is directed ) ) & L is up-complete & L is satisfying_axiom_of_approximation ) );

registration
cluster non empty reflexive continuous  ->  non empty reflexive up-complete satisfying_axiom_of_approximation for RelStr ;
coherence
 for b1 being non empty reflexive RelStr st b1 is continuous holds
( b1 is up-complete & b1 is satisfying_axiom_of_approximation ) by Def6;
cluster reflexive transitive antisymmetric lower-bounded with_suprema up-complete satisfying_axiom_of_approximation  ->  lower-bounded continuous for RelStr ;
coherence
 for b1 being lower-bounded sup-Semilattice st b1 is up-complete & b1 is satisfying_axiom_of_approximation holds
b1 is continuous
proof
let L be lower-bounded sup-Semilattice; ::_thesis: ( L is up-complete & L is satisfying_axiom_of_approximation implies L is continuous )
assume A1: ( L is up-complete & L is satisfying_axiom_of_approximation ) ; ::_thesis: L is continuous
thus  for x being Element of L holds
( not waybelow x is empty & waybelow x is directed ) ; :: according to WAYBEL_3:def_6 ::_thesis: ( L is up-complete & L is satisfying_axiom_of_approximation )
thus  ( L is up-complete & L is satisfying_axiom_of_approximation ) by A1; ::_thesis: verum
end;
end;

registration
cluster non empty strict V233() reflexive transitive antisymmetric with_suprema with_infima complete continuous for RelStr ;
existence
 ex b1 being LATTICE st
( b1 is continuous & b1 is complete & b1 is strict )
proof
set x = the set ;
set R = the Order of { the set };
 RelStr(# { the set }, the Order of { the set } #) is 1 -element RelStr ;
hence  ex b1 being LATTICE st
( b1 is continuous & b1 is complete & b1 is strict ) ; ::_thesis: verum
end;
end;

registration
let L be non empty reflexive continuous RelStr ;
let x be Element of L;
cluster waybelow x ->  non empty directed ;
coherence
 ( not waybelow x is empty & waybelow x is directed ) by Def6;
end;

theorem :: WAYBEL_3:24
for L being up-complete Semilattice st ( for x being Element of L holds
( not waybelow x is empty & waybelow x is directed ) ) holds
( L is satisfying_axiom_of_approximation iff for x, y being Element of L st not x <= y holds
ex u being Element of L st
( u << x & not u <= y ) )
proof
let L be up-complete Semilattice; ::_thesis: ( ( for x being Element of L holds
( not waybelow x is empty & waybelow x is directed ) ) implies ( L is satisfying_axiom_of_approximation iff for x, y being Element of L st not x <= y holds
ex u being Element of L st
( u << x & not u <= y ) ) )
assume A1: for x being Element of L holds
( not waybelow x is empty & waybelow x is directed ) ; ::_thesis: ( L is satisfying_axiom_of_approximation iff for x, y being Element of L st not x <= y holds
ex u being Element of L st
( u << x & not u <= y ) )
hereby  ::_thesis: ( ( for x, y being Element of L st not x <= y holds
ex u being Element of L st
( u << x & not u <= y ) ) implies L is satisfying_axiom_of_approximation )
assume A2: L is satisfying_axiom_of_approximation ; ::_thesis: for x, y being Element of L st not x <= y holds
ex u being Element of L st
( u << x & not u <= y )
let x, y be Element of L; ::_thesis: ( not x <= y implies ex u being Element of L st
( u << x & not u <= y ) )
assume A3: not x <= y ; ::_thesis: ex u being Element of L st
( u << x & not u <= y )
A4: ( not waybelow x is empty & waybelow x is directed ) by A1;
A5: x = sup (waybelow x) by A2, Def5;
 ex_sup_of waybelow x,L by A4, WAYBEL_0:75;
then  ( y is_>=_than waybelow x implies y >= x ) by A5, YELLOW_0:def_9;
then consider u being Element of L such that
A6: u in waybelow x and
A7: not u <= y by A3, LATTICE3:def_9;
take u = u; ::_thesis: ( u << x & not u <= y )
thus  ( u << x & not u <= y ) by A6, A7, Th7; ::_thesis: verum
end;
assume A8: for x, y being Element of L st not x <= y holds
ex u being Element of L st
( u << x & not u <= y ) ; ::_thesis: L is satisfying_axiom_of_approximation
let x be Element of L; :: according to WAYBEL_3:def_5 ::_thesis: x = sup (waybelow x)
 ( not waybelow x is empty & waybelow x is directed ) by A1;
then A9: ex_sup_of waybelow x,L by WAYBEL_0:75;
A10: x is_>=_than waybelow x by Th9;
now__::_thesis:_for_y_being_Element_of_L_st_y_is_>=_than_waybelow_x_holds_
x_<=_y
let y be Element of L; ::_thesis: ( y is_>=_than waybelow x implies x <= y )
assume that
A11: y is_>=_than waybelow x and
A12: not x <= y ; ::_thesis: contradiction
consider u being Element of L such that
A13: u << x and
A14: not u <= y by A8, A12;
 u in waybelow x by A13;
hence  contradiction by A11, A14, LATTICE3:def_9; ::_thesis: verum
end;
hence  x = sup (waybelow x) by A9, A10, YELLOW_0:def_9; ::_thesis: verum
end;

theorem :: WAYBEL_3:25
for L being continuous LATTICE
for x, y being Element of L holds
( x <= y iff waybelow x c= waybelow y )
proof
let L be continuous LATTICE; ::_thesis: for x, y being Element of L holds
( x <= y iff waybelow x c= waybelow y )
let x, y be Element of L; ::_thesis: ( x <= y iff waybelow x c= waybelow y )
thus  ( x <= y implies waybelow x c= waybelow y ) by Th12; ::_thesis: ( waybelow x c= waybelow y implies x <= y )
assume A1: waybelow x c= waybelow y ; ::_thesis: x <= y
A2: ex_sup_of waybelow x,L by WAYBEL_0:75;
 ex_sup_of waybelow y,L by WAYBEL_0:75;
then  sup (waybelow x) <= sup (waybelow y) by A1, A2, YELLOW_0:34;
then  x <= sup (waybelow y) by Def5;
hence  x <= y by Def5; ::_thesis: verum
end;

registration
cluster non empty reflexive transitive antisymmetric complete connected  ->  satisfying_axiom_of_approximation for RelStr ;
coherence
 for b1 being Chain st b1 is complete holds
b1 is satisfying_axiom_of_approximation
proof
let L be Chain; ::_thesis: ( L is complete implies L is satisfying_axiom_of_approximation )
assume  L is complete ; ::_thesis: L is satisfying_axiom_of_approximation
then reconsider S = L as complete Chain ;
 S is satisfying_axiom_of_approximation
proof
let x be Element of S; :: according to WAYBEL_3:def_5 ::_thesis: x = sup (waybelow x)
A1: ex_sup_of waybelow x,S by YELLOW_0:17;
A2: x is_>=_than waybelow x by Th9;
now__::_thesis:_for_y_being_Element_of_S_st_y_is_>=_than_waybelow_x_holds_
x_<=_y
let y be Element of S; ::_thesis: ( y is_>=_than waybelow x implies x <= y )
assume that
A3: y is_>=_than waybelow x and
A4: not x <= y ; ::_thesis: contradiction
 x >= y by A4, WAYBEL_0:def_29;
then  x > y by A4, ORDERS_2:def_6;
then  x >> y by Th13;
then  y in waybelow x ;
then  for z being Element of S st z is_>=_than waybelow x holds
z >= y by LATTICE3:def_9;
then A5: sup (waybelow x) = y by A1, A3, YELLOW_0:def_9;
 x << x
proof
let D be non empty directed Subset of S; :: according to WAYBEL_3:def_1 ::_thesis: ( x <= sup D implies ex d being Element of S st
( d in D & x <= d ) )
assume A6: x <= sup D ; ::_thesis: ex d being Element of S st
( d in D & x <= d )
assume A7: for d being Element of S st d in D holds
not x <= d ; ::_thesis: contradiction
A8: D c= waybelow x
proof
let a be set ; :: according to TARSKI:def_3 ::_thesis: ( not a in D or a in waybelow x )
assume A9: a in D ; ::_thesis: a in waybelow x
then reconsider a = a as Element of S ;
A10: not x <= a by A7, A9;
then  a <= x by WAYBEL_0:def_29;
then  a < x by A10, ORDERS_2:def_6;
then  a << x by Th13;
hence  a in waybelow x ; ::_thesis: verum
end;
 ex_sup_of D,S by YELLOW_0:17;
then  sup D <= sup (waybelow x) by A1, A8, YELLOW_0:34;
hence  contradiction by A4, A5, A6, ORDERS_2:3; ::_thesis: verum
end;
then  x in waybelow x ;
hence  contradiction by A3, A4, LATTICE3:def_9; ::_thesis: verum
end;
hence  x = sup (waybelow x) by A1, A2, YELLOW_0:def_9; ::_thesis: verum
end;
hence  L is satisfying_axiom_of_approximation ; ::_thesis: verum
end;
end;

theorem :: WAYBEL_3:26
for L being complete LATTICE st ( for x being Element of L holds x is compact ) holds
L is satisfying_axiom_of_approximation
proof
let L be complete LATTICE; ::_thesis: ( ( for x being Element of L holds x is compact ) implies L is satisfying_axiom_of_approximation )
assume A1: for x being Element of L holds x is compact ; ::_thesis: L is satisfying_axiom_of_approximation
let x be Element of L; :: according to WAYBEL_3:def_5 ::_thesis: x = sup (waybelow x)
 x is compact by A1;
then  x << x by Def2;
then A2: x in waybelow x ;
 waybelow x is_<=_than sup (waybelow x) by YELLOW_0:32;
then A3: x <= sup (waybelow x) by A2, LATTICE3:def_9;
A4: ex_sup_of waybelow x,L by YELLOW_0:17;
A5: ex_sup_of downarrow x,L by WAYBEL_0:34;
 sup (downarrow x) = x by WAYBEL_0:34;
then  x >= sup (waybelow x) by A4, A5, Th11, YELLOW_0:34;
hence  x = sup (waybelow x) by A3, ORDERS_2:2; ::_thesis: verum
end;

begin

definition
let f be Relation;
attrf is non-Empty  means :Def7: :: WAYBEL_3:def 7
 for S being 1-sorted st S in rng f holds
not S is empty ;
attrf is reflexive-yielding  means :Def8: :: WAYBEL_3:def 8
 for S being RelStr st S in rng f holds
S is reflexive ;
end;

:: deftheorem Def7 defines non-Empty WAYBEL_3:def_7_:_
 for f being Relation holds
( f is non-Empty iff for S being 1-sorted st S in rng f holds
not S is empty );

:: deftheorem Def8 defines reflexive-yielding WAYBEL_3:def_8_:_
 for f being Relation holds
( f is reflexive-yielding iff for S being RelStr st S in rng f holds
S is reflexive );

registration
let I be set ;
cluster Relation-like I -defined Function-like V31(I) RelStr-yielding non-Empty reflexive-yielding for set ;
existence
 ex b1 being ManySortedSet of I st
( b1 is RelStr-yielding & b1 is non-Empty & b1 is reflexive-yielding )
proof
set R = the non empty reflexive RelStr ;
set J = I --> the non empty reflexive RelStr ;
A1: rng (I --> the non empty reflexive RelStr ) c= { the non empty reflexive RelStr } by FUNCOP_1:13;
reconsider J = I --> the non empty reflexive RelStr as ManySortedSet of I ;
take  J ; ::_thesis: ( J is RelStr-yielding & J is non-Empty & J is reflexive-yielding )
thus  J is RelStr-yielding ; ::_thesis: ( J is non-Empty & J is reflexive-yielding )
thus  J is non-Empty ::_thesis: J is reflexive-yielding
proof
let S be 1-sorted ; :: according to WAYBEL_3:def_7 ::_thesis: ( S in rng J implies not S is empty )
assume  S in rng J ; ::_thesis: not S is empty
hence  not S is empty by A1, TARSKI:def_1; ::_thesis: verum
end;
let S be RelStr ; :: according to WAYBEL_3:def_8 ::_thesis: ( S in rng J implies S is reflexive )
assume  S in rng J ; ::_thesis: S is reflexive
hence  S is reflexive by A1, TARSKI:def_1; ::_thesis: verum
end;
end;

registration
let I be set ;
let J be RelStr-yielding non-Empty ManySortedSet of I;
cluster product J ->  non empty ;
coherence
 not product J is empty
proof
A1: the carrier of (product J) = product (Carrier J) by YELLOW_1:def_4;
now__::_thesis:_not_{}_in_rng_(Carrier_J)
assume  {} in rng (Carrier J) ; ::_thesis: contradiction
then consider i being set  such that
A2: i in dom (Carrier J) and
A3: {} = (Carrier J) . i by FUNCT_1:def_3;
A4: dom (Carrier J) = I by PARTFUN1:def_2;
A5: dom J = I by PARTFUN1:def_2;
consider R being 1-sorted  such that
A6: R = J . i and
A7: {} = the carrier of R by A2, A3, A4, PRALG_1:def_13;
 R in rng J by A2, A4, A5, A6, FUNCT_1:def_3;
then reconsider R = R as non empty RelStr by Def7, YELLOW_1:def_3;
 the carrier of R = {} by A7;
hence  contradiction ; ::_thesis: verum
end;
then  the carrier of (product J) <> {} by A1, CARD_3:26;
hence  not product J is empty ; ::_thesis: verum
end;
end;

definition
let I be non empty set ;
let J be RelStr-yielding ManySortedSet of I;
let i be Element of I;
:: original: .
redefine funcJ . i ->  RelStr ;
coherence
 J . i is RelStr
proof
 dom J = I by PARTFUN1:def_2;
then  J . i in rng J by FUNCT_1:def_3;
hence  J . i is RelStr ; ::_thesis: verum
end;
end;

registration
let I be non empty set ;
let J be RelStr-yielding non-Empty ManySortedSet of I;
let i be Element of I;
clusterJ . i ->  non empty for RelStr ;
coherence
 for b1 being RelStr st b1 = J . i holds
not b1 is empty
proof
 dom J = I by PARTFUN1:def_2;
then  J . i in rng J by FUNCT_1:def_3;
hence  for b1 being RelStr st b1 = J . i holds
not b1 is empty by Def7; ::_thesis: verum
end;
end;

registration
let I be set ;
let J be RelStr-yielding non-Empty ManySortedSet of I;
cluster product J ->  constituted-Functions ;
coherence
 product J is constituted-Functions
proof
 the carrier of (product J) = product (Carrier J) by YELLOW_1:def_4;
hence  product J is constituted-Functions by MONOID_0:80; ::_thesis: verum
end;
end;

definition
let I be non empty set ;
let J be RelStr-yielding non-Empty ManySortedSet of I;
let x be Element of (product J);
let i be Element of I;
:: original: .
redefine funcx . i ->  Element of (J . i);
coherence
 x . i is Element of (J . i)
proof
A1: ex R being 1-sorted st
( R = J . i & (Carrier J) . i = the carrier of R ) by PRALG_1:def_13;
A2: the carrier of (product J) = product (Carrier J) by YELLOW_1:def_4;
 dom (Carrier J) = I by PARTFUN1:def_2;
hence  x . i is Element of (J . i) by A1, A2, CARD_3:9; ::_thesis: verum
end;
end;

definition
let I be non empty set ;
let J be RelStr-yielding non-Empty ManySortedSet of I;
let i be Element of I;
let X be Subset of (product J);
:: original: pi
redefine func pi (X,i) ->  Subset of (J . i);
coherence
 pi (X,i) is Subset of (J . i)
proof
set Y = the carrier of (product J);
A1: the carrier of (product J) = product (Carrier J) by YELLOW_1:def_4;
A2: dom (Carrier J) = I by PARTFUN1:def_2;
 X \/ the carrier of (product J) = the carrier of (product J) by XBOOLE_1:12;
then  pi ( the carrier of (product J),i) = (pi (X,i)) \/ (pi ( the carrier of (product J),i)) by CARD_3:16;
then A3: pi (X,i) c= pi ( the carrier of (product J),i) by XBOOLE_1:7;
 ex R being 1-sorted st
( R = J . i & (Carrier J) . i = the carrier of R ) by PRALG_1:def_13;
hence  pi (X,i) is Subset of (J . i) by A1, A2, A3, CARD_3:12; ::_thesis: verum
end;
end;

theorem Th27: :: WAYBEL_3:27
for I being non empty set
for J being RelStr-yielding non-Empty ManySortedSet of I
for x being Function holds
( x is Element of (product J) iff ( dom x = I & ( for i being Element of I holds x . i is Element of (J . i) ) ) )
proof
let I be non empty set ; ::_thesis: for J being RelStr-yielding non-Empty ManySortedSet of I
for x being Function holds
( x is Element of (product J) iff ( dom x = I & ( for i being Element of I holds x . i is Element of (J . i) ) ) )
let J be RelStr-yielding non-Empty ManySortedSet of I; ::_thesis: for x being Function holds
( x is Element of (product J) iff ( dom x = I & ( for i being Element of I holds x . i is Element of (J . i) ) ) )
let x be Function; ::_thesis: ( x is Element of (product J) iff ( dom x = I & ( for i being Element of I holds x . i is Element of (J . i) ) ) )
A1: the carrier of (product J) = product (Carrier J) by YELLOW_1:def_4;
A2: dom (Carrier J) = I by PARTFUN1:def_2;
hereby  ::_thesis: ( dom x = I & ( for i being Element of I holds x . i is Element of (J . i) ) implies x is Element of (product J) )
assume A3: x is Element of (product J) ; ::_thesis: ( dom x = I & ( for i being Element of I holds x . i is Element of (J . i) ) )
hence  dom x = I by A1, A2, CARD_3:9; ::_thesis: for i being Element of I holds x . i is Element of (J . i)
let i be Element of I; ::_thesis: x . i is Element of (J . i)
reconsider y = x as Element of (product J) by A3;
 y . i is Element of (J . i) ;
hence  x . i is Element of (J . i) ; ::_thesis: verum
end;
assume that
A4: dom x = I and
A5: for i being Element of I holds x . i is Element of (J . i) ; ::_thesis: x is Element of (product J)
now__::_thesis:_for_i_being_set_st_i_in_dom_(Carrier_J)_holds_
x_._i_in_(Carrier_J)_._i
let i be set ; ::_thesis: ( i in dom (Carrier J) implies x . i in (Carrier J) . i )
assume  i in dom (Carrier J) ; ::_thesis: x . i in (Carrier J) . i
then reconsider j = i as Element of I by PARTFUN1:def_2;
A6: x . j is Element of (J . j) by A5;
 ex R being 1-sorted st
( R = J . j & (Carrier J) . j = the carrier of R ) by PRALG_1:def_13;
hence  x . i in (Carrier J) . i by A6; ::_thesis: verum
end;
hence  x is Element of (product J) by A1, A2, A4, CARD_3:9; ::_thesis: verum
end;

theorem Th28: :: WAYBEL_3:28
for I being non empty set
for J being RelStr-yielding non-Empty ManySortedSet of I
for x, y being Element of (product J) holds
( x <= y iff for i being Element of I holds x . i <= y . i )
proof
let I be non empty set ; ::_thesis: for J being RelStr-yielding non-Empty ManySortedSet of I
for x, y being Element of (product J) holds
( x <= y iff for i being Element of I holds x . i <= y . i )
let J be RelStr-yielding non-Empty ManySortedSet of I; ::_thesis: for x, y being Element of (product J) holds
( x <= y iff for i being Element of I holds x . i <= y . i )
set L = product J;
let x, y be Element of (product J); ::_thesis: ( x <= y iff for i being Element of I holds x . i <= y . i )
A1: the carrier of (product J) = product (Carrier J) by YELLOW_1:def_4;
hereby  ::_thesis: ( ( for i being Element of I holds x . i <= y . i ) implies x <= y )
assume A2: x <= y ; ::_thesis: for i being Element of I holds x . i <= y . i
let i be Element of I; ::_thesis: x . i <= y . i
 ex f, g being Function st
( f = x & g = y & ( for i being set st i in I holds
ex R being RelStr ex xi, yi being Element of R st
( R = J . i & xi = f . i & yi = g . i & xi <= yi ) ) ) by A1, A2, YELLOW_1:def_4;
then  ex R being RelStr ex xi, yi being Element of R st
( R = J . i & xi = x . i & yi = y . i & xi <= yi ) ;
hence  x . i <= y . i ; ::_thesis: verum
end;
assume A3: for i being Element of I holds x . i <= y . i ; ::_thesis: x <= y
 ex f, g being Function st
( f = x & g = y & ( for i being set st i in I holds
ex R being RelStr ex xi, yi being Element of R st
( R = J . i & xi = f . i & yi = g . i & xi <= yi ) ) )
proof
take f = x; ::_thesis: ex g being Function st
( f = x & g = y & ( for i being set st i in I holds
ex R being RelStr ex xi, yi being Element of R st
( R = J . i & xi = f . i & yi = g . i & xi <= yi ) ) )
take g = y; ::_thesis: ( f = x & g = y & ( for i being set st i in I holds
ex R being RelStr ex xi, yi being Element of R st
( R = J . i & xi = f . i & yi = g . i & xi <= yi ) ) )
thus  ( f = x & g = y ) ; ::_thesis: for i being set st i in I holds
ex R being RelStr ex xi, yi being Element of R st
( R = J . i & xi = f . i & yi = g . i & xi <= yi )
let i be set ; ::_thesis: ( i in I implies ex R being RelStr ex xi, yi being Element of R st
( R = J . i & xi = f . i & yi = g . i & xi <= yi ) )
assume  i in I ; ::_thesis: ex R being RelStr ex xi, yi being Element of R st
( R = J . i & xi = f . i & yi = g . i & xi <= yi )
then reconsider j = i as Element of I ;
take  J . j ; ::_thesis: ex xi, yi being Element of (J . j) st
( J . j = J . i & xi = f . i & yi = g . i & xi <= yi )
take  x . j ; ::_thesis: ex yi being Element of (J . j) st
( J . j = J . i & x . j = f . i & yi = g . i & x . j <= yi )
take  y . j ; ::_thesis: ( J . j = J . i & x . j = f . i & y . j = g . i & x . j <= y . j )
thus  ( J . j = J . i & x . j = f . i & y . j = g . i & x . j <= y . j ) by A3; ::_thesis: verum
end;
hence  x <= y by A1, YELLOW_1:def_4; ::_thesis: verum
end;

registration
let I be non empty set ;
let J be RelStr-yielding reflexive-yielding ManySortedSet of I;
let i be Element of I;
clusterJ . i ->  reflexive for RelStr ;
coherence
 for b1 being RelStr st b1 = J . i holds
b1 is reflexive
proof
 dom J = I by PARTFUN1:def_2;
then  J . i in rng J by FUNCT_1:def_3;
hence  for b1 being RelStr st b1 = J . i holds
b1 is reflexive by Def8; ::_thesis: verum
end;
end;

registration
let I be non empty set ;
let J be RelStr-yielding non-Empty reflexive-yielding ManySortedSet of I;
cluster product J ->  reflexive ;
coherence
 product J is reflexive
proof
thus  product J is reflexive ::_thesis: verum
proof
let x be Element of (product J); :: according to YELLOW_0:def_1 ::_thesis: x <= x
 for i being Element of I holds x . i <= x . i ;
hence  x <= x by Th28; ::_thesis: verum
end;
end;
end;

theorem Th29: :: WAYBEL_3:29
for I being non empty set
for J being RelStr-yielding non-Empty ManySortedSet of I st ( for i being Element of I holds J . i is transitive ) holds
product J is transitive
proof
let I be non empty set ; ::_thesis: for J being RelStr-yielding non-Empty ManySortedSet of I st ( for i being Element of I holds J . i is transitive ) holds
product J is transitive
let J be RelStr-yielding non-Empty ManySortedSet of I; ::_thesis: ( ( for i being Element of I holds J . i is transitive ) implies product J is transitive )
assume A1: for i being Element of I holds J . i is transitive ; ::_thesis: product J is transitive
let x, y, z be Element of (product J); :: according to YELLOW_0:def_2 ::_thesis: ( not x <= y or not y <= z or x <= z )
assume that
A2: x <= y and
A3: y <= z ; ::_thesis: x <= z
now__::_thesis:_for_i_being_Element_of_I_holds_x_._i_<=_z_._i
let i be Element of I; ::_thesis: x . i <= z . i
A4: x . i <= y . i by A2, Th28;
A5: y . i <= z . i by A3, Th28;
 J . i is transitive by A1;
hence  x . i <= z . i by A4, A5, YELLOW_0:def_2; ::_thesis: verum
end;
hence  x <= z by Th28; ::_thesis: verum
end;

theorem Th30: :: WAYBEL_3:30
for I being non empty set
for J being RelStr-yielding non-Empty ManySortedSet of I st ( for i being Element of I holds J . i is antisymmetric ) holds
product J is antisymmetric
proof
let I be non empty set ; ::_thesis: for J being RelStr-yielding non-Empty ManySortedSet of I st ( for i being Element of I holds J . i is antisymmetric ) holds
product J is antisymmetric
let J be RelStr-yielding non-Empty ManySortedSet of I; ::_thesis: ( ( for i being Element of I holds J . i is antisymmetric ) implies product J is antisymmetric )
assume A1: for i being Element of I holds J . i is antisymmetric ; ::_thesis: product J is antisymmetric
let x, y be Element of (product J); :: according to YELLOW_0:def_3 ::_thesis: ( not x <= y or not y <= x or x = y )
assume that
A2: x <= y and
A3: y <= x ; ::_thesis: x = y
A4: dom x = I by Th27;
A5: dom y = I by Th27;
now__::_thesis:_for_j_being_set_st_j_in_I_holds_
x_._j_=_y_._j
let j be set ; ::_thesis: ( j in I implies x . j = y . j )
assume  j in I ; ::_thesis: x . j = y . j
then reconsider i = j as Element of I ;
A6: x . i <= y . i by A2, Th28;
A7: y . i <= x . i by A3, Th28;
 J . i is antisymmetric by A1;
hence  x . j = y . j by A6, A7, YELLOW_0:def_3; ::_thesis: verum
end;
hence  x = y by A4, A5, FUNCT_1:2; ::_thesis: verum
end;

theorem Th31: :: WAYBEL_3:31
for I being non empty set
for J being RelStr-yielding non-Empty reflexive-yielding ManySortedSet of I st ( for i being Element of I holds J . i is complete LATTICE ) holds
product J is complete LATTICE
proof
let I be non empty set ; ::_thesis: for J being RelStr-yielding non-Empty reflexive-yielding ManySortedSet of I st ( for i being Element of I holds J . i is complete LATTICE ) holds
product J is complete LATTICE
let J be RelStr-yielding non-Empty reflexive-yielding ManySortedSet of I; ::_thesis: ( ( for i being Element of I holds J . i is complete LATTICE ) implies product J is complete LATTICE )
assume A1: for i being Element of I holds J . i is complete LATTICE ; ::_thesis: product J is complete LATTICE
then A2: for i being Element of I holds J . i is transitive ;
 for i being Element of I holds J . i is antisymmetric by A1;
then reconsider L = product J as non empty Poset by A2, Th29, Th30;
now__::_thesis:_for_X_being_Subset_of_(product_J)_holds_ex_sup_of_X,_product_J
let X be Subset of (product J); ::_thesis: ex_sup_of X, product J
deffunc H1( Element of I) ->  Element of the carrier of (J . $1) = sup (pi (X,$1));
consider f being ManySortedSet of I such that
A3: for i being Element of I holds f . i = H1(i) from PBOOLE:sch_5();
A4: dom f = I by PARTFUN1:def_2;
now__::_thesis:_for_i_being_Element_of_I_holds_f_._i_is_Element_of_(J_._i)
let i be Element of I; ::_thesis: f . i is Element of (J . i)
 f . i = sup (pi (X,i)) by A3;
hence  f . i is Element of (J . i) ; ::_thesis: verum
end;
then reconsider f = f as Element of (product J) by A4, Th27;
A5: f is_>=_than X
proof
let x be Element of (product J); :: according to LATTICE3:def_9 ::_thesis: ( not x in X or x <= f )
assume A6: x in X ; ::_thesis: x <= f
now__::_thesis:_for_i_being_Element_of_I_holds_x_._i_<=_f_._i
let i be Element of I; ::_thesis: x . i <= f . i
A7: x . i in pi (X,i) by A6, CARD_3:def_6;
A8: J . i is complete LATTICE by A1;
 f . i = sup (pi (X,i)) by A3;
hence  x . i <= f . i by A7, A8, YELLOW_2:22; ::_thesis: verum
end;
hence  x <= f by Th28; ::_thesis: verum
end;
now__::_thesis:_for_g_being_Element_of_(product_J)_st_X_is_<=_than_g_holds_
f_<=_g
let g be Element of (product J); ::_thesis: ( X is_<=_than g implies f <= g )
assume A9: X is_<=_than g ; ::_thesis: f <= g
now__::_thesis:_(_L_=_L_&_(_for_i_being_Element_of_I_holds_f_._i_<=_g_._i_)_)
thus  L = L ; ::_thesis: for i being Element of I holds f . i <= g . i
let i be Element of I; ::_thesis: f . i <= g . i
A10: f . i = sup (pi (X,i)) by A3;
A11: J . i is complete LATTICE by A1;
 g . i is_>=_than pi (X,i)
proof
let a be Element of (J . i); :: according to LATTICE3:def_9 ::_thesis: ( not a in pi (X,i) or a <= g . i )
assume  a in pi (X,i) ; ::_thesis: a <= g . i
then consider h being Function such that
A12: h in X and
A13: a = h . i by CARD_3:def_6;
reconsider h = h as Element of (product J) by A12;
 h <= g by A9, A12, LATTICE3:def_9;
hence  a <= g . i by A13, Th28; ::_thesis: verum
end;
hence  f . i <= g . i by A10, A11, YELLOW_0:32; ::_thesis: verum
end;
hence  f <= g by Th28; ::_thesis: verum
end;
then  ex_sup_of X,L by A5, YELLOW_0:15;
hence  ex_sup_of X, product J ; ::_thesis: verum
end;
then  L is non empty complete Poset by YELLOW_0:53;
hence  product J is complete LATTICE ; ::_thesis: verum
end;

theorem Th32: :: WAYBEL_3:32
for I being non empty set
for J being RelStr-yielding non-Empty reflexive-yielding ManySortedSet of I st ( for i being Element of I holds J . i is complete LATTICE ) holds
for X being Subset of (product J)
for i being Element of I holds (sup X) . i = sup (pi (X,i))
proof
let I be non empty set ; ::_thesis: for J being RelStr-yielding non-Empty reflexive-yielding ManySortedSet of I st ( for i being Element of I holds J . i is complete LATTICE ) holds
for X being Subset of (product J)
for i being Element of I holds (sup X) . i = sup (pi (X,i))
let J be RelStr-yielding non-Empty reflexive-yielding ManySortedSet of I; ::_thesis: ( ( for i being Element of I holds J . i is complete LATTICE ) implies for X being Subset of (product J)
for i being Element of I holds (sup X) . i = sup (pi (X,i)) )
assume A1: for i being Element of I holds J . i is complete LATTICE ; ::_thesis: for X being Subset of (product J)
for i being Element of I holds (sup X) . i = sup (pi (X,i))
then reconsider L = product J as complete LATTICE by Th31;
A2: L is complete ;
let X be Subset of (product J); ::_thesis: for i being Element of I holds (sup X) . i = sup (pi (X,i))
let i be Element of I; ::_thesis: (sup X) . i = sup (pi (X,i))
A3: sup X is_>=_than X by A2, YELLOW_0:32;
A4: (sup X) . i is_>=_than pi (X,i)
proof
let a be Element of (J . i); :: according to LATTICE3:def_9 ::_thesis: ( not a in pi (X,i) or a <= (sup X) . i )
assume  a in pi (X,i) ; ::_thesis: a <= (sup X) . i
then consider f being Function such that
A5: f in X and
A6: a = f . i by CARD_3:def_6;
reconsider f = f as Element of (product J) by A5;
 sup X >= f by A3, A5, LATTICE3:def_9;
hence  a <= (sup X) . i by A6, Th28; ::_thesis: verum
end;
A7: J . i is complete LATTICE by A1;
now__::_thesis:_for_a_being_Element_of_(J_._i)_st_a_is_>=_than_pi_(X,i)_holds_
(sup_X)_._i_<=_a
let a be Element of (J . i); ::_thesis: ( a is_>=_than pi (X,i) implies (sup X) . i <= a )
assume A8: a is_>=_than pi (X,i) ; ::_thesis: (sup X) . i <= a
set f = (sup X) +* (i,a);
A9: dom ((sup X) +* (i,a)) = dom (sup X) by FUNCT_7:30;
A10: dom (sup X) = I by Th27;
now__::_thesis:_for_j_being_Element_of_I_holds_((sup_X)_+*_(i,a))_._j_is_Element_of_(J_._j)
let j be Element of I; ::_thesis: ((sup X) +* (i,a)) . j is Element of (J . j)
 ( j = i or j <> i ) ;
then  ( ((sup X) +* (i,a)) . j = (sup X) . j or ( ((sup X) +* (i,a)) . j = a & j = i ) ) by A10, FUNCT_7:31, FUNCT_7:32;
hence  ((sup X) +* (i,a)) . j is Element of (J . j) ; ::_thesis: verum
end;
then reconsider f = (sup X) +* (i,a) as Element of (product J) by A9, Th27;
 f is_>=_than X
proof
let g be Element of (product J); :: according to LATTICE3:def_9 ::_thesis: ( not g in X or g <= f )
assume A11: g in X ; ::_thesis: g <= f
then A12: g <= sup X by A2, YELLOW_2:22;
A13: g . i in pi (X,i) by A11, CARD_3:def_6;
now__::_thesis:_for_j_being_Element_of_I_holds_f_._j_>=_g_._j
let j be Element of I; ::_thesis: f . j >= g . j
 ( j = i or j <> i ) ;
then  ( f . j = (sup X) . j or ( f . j = a & j = i ) ) by A10, FUNCT_7:31, FUNCT_7:32;
hence  f . j >= g . j by A8, A12, A13, Th28, LATTICE3:def_9; ::_thesis: verum
end;
hence  g <= f by Th28; ::_thesis: verum
end;
then A14: f >= sup X by A2, YELLOW_0:32;
 f . i = a by A10, FUNCT_7:31;
hence  (sup X) . i <= a by A14, Th28; ::_thesis: verum
end;
hence  (sup X) . i = sup (pi (X,i)) by A4, A7, YELLOW_0:32; ::_thesis: verum
end;

theorem :: WAYBEL_3:33
for I being non empty set
for J being RelStr-yielding non-Empty reflexive-yielding ManySortedSet of I st ( for i being Element of I holds J . i is complete LATTICE ) holds
for x, y being Element of (product J) holds
( x << y iff ( ( for i being Element of I holds x . i << y . i ) & ex K being finite Subset of I st
for i being Element of I st not i in K holds
x . i = Bottom (J . i) ) )
proof
let I be non empty set ; ::_thesis: for J being RelStr-yielding non-Empty reflexive-yielding ManySortedSet of I st ( for i being Element of I holds J . i is complete LATTICE ) holds
for x, y being Element of (product J) holds
( x << y iff ( ( for i being Element of I holds x . i << y . i ) & ex K being finite Subset of I st
for i being Element of I st not i in K holds
x . i = Bottom (J . i) ) )
let J be RelStr-yielding non-Empty reflexive-yielding ManySortedSet of I; ::_thesis: ( ( for i being Element of I holds J . i is complete LATTICE ) implies for x, y being Element of (product J) holds
( x << y iff ( ( for i being Element of I holds x . i << y . i ) & ex K being finite Subset of I st
for i being Element of I st not i in K holds
x . i = Bottom (J . i) ) ) )
set L = product J;
assume A1: for i being Element of I holds J . i is complete LATTICE ; ::_thesis: for x, y being Element of (product J) holds
( x << y iff ( ( for i being Element of I holds x . i << y . i ) & ex K being finite Subset of I st
for i being Element of I st not i in K holds
x . i = Bottom (J . i) ) )
then reconsider L9 = product J as complete LATTICE by Th31;
let x, y be Element of (product J); ::_thesis: ( x << y iff ( ( for i being Element of I holds x . i << y . i ) & ex K being finite Subset of I st
for i being Element of I st not i in K holds
x . i = Bottom (J . i) ) )
hereby  ::_thesis: ( ( for i being Element of I holds x . i << y . i ) & ex K being finite Subset of I st
for i being Element of I st not i in K holds
x . i = Bottom (J . i) implies x << y )
assume A2: x << y ; ::_thesis: ( ( for i being Element of I holds x . i << y . i ) & ex K being finite Subset of I st
for i being Element of I st not i in K holds
not x . i <> Bottom (J . i) )
hereby  ::_thesis: ex K being finite Subset of I st
for i being Element of I st not i in K holds
not x . i <> Bottom (J . i)
let i be Element of I; ::_thesis: x . i << y . i
thus  x . i << y . i ::_thesis: verum
proof
let Di be non empty directed Subset of (J . i); :: according to WAYBEL_3:def_1 ::_thesis: ( y . i <= sup Di implies ex d being Element of (J . i) st
( d in Di & x . i <= d ) )
assume A3: y . i <= sup Di ; ::_thesis: ex d being Element of (J . i) st
( d in Di & x . i <= d )
A4: dom y = I by Th27;
set D =  {  (y +* (i,z)) where z is Element of (J . i) : z in Di  }  ;
  {  (y +* (i,z)) where z is Element of (J . i) : z in Di  }  c= the carrier of (product J)
proof
let a be set ; :: according to TARSKI:def_3 ::_thesis: ( not a in  {  (y +* (i,z)) where z is Element of (J . i) : z in Di  }  or a in the carrier of (product J) )
assume  a in  {  (y +* (i,z)) where z is Element of (J . i) : z in Di  }  ; ::_thesis: a in the carrier of (product J)
then consider z being Element of (J . i) such that
A5: a = y +* (i,z) and
 z in Di ;
A6: dom (y +* (i,z)) = I by A4, FUNCT_7:30;
now__::_thesis:_for_j_being_Element_of_I_holds_(y_+*_(i,z))_._j_is_Element_of_(J_._j)
let j be Element of I; ::_thesis: (y +* (i,z)) . j is Element of (J . j)
 ( i = j or i <> j ) ;
then  ( ( (y +* (i,z)) . j = z & i = j ) or (y +* (i,z)) . j = y . j ) by A4, FUNCT_7:31, FUNCT_7:32;
hence  (y +* (i,z)) . j is Element of (J . j) ; ::_thesis: verum
end;
then  a is Element of (product J) by A5, A6, Th27;
hence  a in the carrier of (product J) ; ::_thesis: verum
end;
then reconsider D =  {  (y +* (i,z)) where z is Element of (J . i) : z in Di  }  as Subset of (product J) ;
set di = the Element of Di;
reconsider di = the Element of Di as Element of (J . i) ;
A7: y +* (i,di) in D ;
A8: dom y = I by Th27;
reconsider D = D as non empty Subset of (product J) by A7;
 D is directed
proof
let z1, z2 be Element of (product J); :: according to WAYBEL_0:def_1 ::_thesis: ( not z1 in D or not z2 in D or ex b1 being Element of the carrier of (product J) st
( b1 in D & z1 <= b1 & z2 <= b1 ) )
assume  z1 in D ; ::_thesis: ( not z2 in D or ex b1 being Element of the carrier of (product J) st
( b1 in D & z1 <= b1 & z2 <= b1 ) )
then consider a1 being Element of (J . i) such that
A9: z1 = y +* (i,a1) and
A10: a1 in Di ;
assume  z2 in D ; ::_thesis: ex b1 being Element of the carrier of (product J) st
( b1 in D & z1 <= b1 & z2 <= b1 )
then consider a2 being Element of (J . i) such that
A11: z2 = y +* (i,a2) and
A12: a2 in Di ;
consider a being Element of (J . i) such that
A13: a in Di and
A14: a >= a1 and
A15: a >= a2 by A10, A12, WAYBEL_0:def_1;
 y +* (i,a) in D by A13;
then reconsider z = y +* (i,a) as Element of (product J) ;
take  z ; ::_thesis: ( z in D & z1 <= z & z2 <= z )
thus  z in D by A13; ::_thesis: ( z1 <= z & z2 <= z )
A16: dom y = I by Th27;
now__::_thesis:_for_j_being_Element_of_I_holds_z_._j_>=_z1_._j
let j be Element of I; ::_thesis: z . j >= z1 . j
 ( i = j or i <> j ) ;
then  ( ( z . j = a & z1 . j = a1 & i = j ) or ( z . j = y . j & z1 . j = y . j ) ) by A9, A16, FUNCT_7:31, FUNCT_7:32;
hence  z . j >= z1 . j by A14, YELLOW_0:def_1; ::_thesis: verum
end;
hence  z >= z1 by Th28; ::_thesis: z2 <= z
now__::_thesis:_for_j_being_Element_of_I_holds_z_._j_>=_z2_._j
let j be Element of I; ::_thesis: z . j >= z2 . j
 ( i = j or i <> j ) ;
then  ( ( z . j = a & z2 . j = a2 & i = j ) or ( z . j = y . j & z2 . j = y . j ) ) by A11, A16, FUNCT_7:31, FUNCT_7:32;
hence  z . j >= z2 . j by A15, YELLOW_0:def_1; ::_thesis: verum
end;
hence  z2 <= z by Th28; ::_thesis: verum
end;
then reconsider D = D as non empty directed Subset of (product J) ;
now__::_thesis:_for_j_being_Element_of_I_holds_(sup_D)_._j_>=_y_._j
let j be Element of I; ::_thesis: (sup D) . j >= y . j
A17: J . i is complete LATTICE by A1;
A18: J . j is complete LATTICE by A1;
A19: ex_sup_of Di,J . i by A17, YELLOW_0:17;
A20: ex_sup_of pi (D,i),J . i by A17, YELLOW_0:17;
 Di c= pi (D,i)
proof
let a be set ; :: according to TARSKI:def_3 ::_thesis: ( not a in Di or a in pi (D,i) )
assume A21: a in Di ; ::_thesis: a in pi (D,i)
then reconsider a = a as Element of (J . i) ;
 y +* (i,a) in D by A21;
then  (y +* (i,a)) . i in pi (D,i) by CARD_3:def_6;
hence  a in pi (D,i) by A8, FUNCT_7:31; ::_thesis: verum
end;
then A22: sup Di <= sup (pi (D,i)) by A19, A20, YELLOW_0:34;
A23: (sup D) . j = sup (pi (D,j)) by A1, Th32;
now__::_thesis:_(_j_<>_i_implies_y_._j_in_pi_(D,j)_)
assume  j <> i ; ::_thesis: y . j in pi (D,j)
then  (y +* (i,di)) . j = y . j by FUNCT_7:32;
hence  y . j in pi (D,j) by A7, CARD_3:def_6; ::_thesis: verum
end;
hence  (sup D) . j >= y . j by A3, A18, A22, A23, YELLOW_0:def_2, YELLOW_2:22; ::_thesis: verum
end;
then  sup D >= y by Th28;
then consider d being Element of (product J) such that
A24: d in D and
A25: d >= x by A2, Def1;
consider z being Element of (J . i) such that
A26: d = y +* (i,z) and
A27: z in Di by A24;
take  z ; ::_thesis: ( z in Di & x . i <= z )
 d . i = z by A4, A26, FUNCT_7:31;
hence  ( z in Di & x . i <= z ) by A25, A27, Th28; ::_thesis: verum
end;
end;
set K =  {  i where i is Element of I : x . i <> Bottom (J . i)  }  ;
  {  i where i is Element of I : x . i <> Bottom (J . i)  }  c= I
proof
let a be set ; :: according to TARSKI:def_3 ::_thesis: ( not a in  {  i where i is Element of I : x . i <> Bottom (J . i)  }  or a in I )
assume  a in  {  i where i is Element of I : x . i <> Bottom (J . i)  }  ; ::_thesis: a in I
then  ex i being Element of I st
( a = i & x . i <> Bottom (J . i) ) ;
hence  a in I ; ::_thesis: verum
end;
then reconsider K =  {  i where i is Element of I : x . i <> Bottom (J . i)  }  as Subset of I ;
deffunc H1( Element of I) ->  Element of the carrier of (J . $1) = Bottom (J . $1);
consider f being ManySortedSet of I such that
A28: for i being Element of I holds f . i = H1(i) from PBOOLE:sch_5();
A29: dom f = I by PARTFUN1:def_2;
now__::_thesis:_for_i_being_Element_of_I_holds_f_._i_is_Element_of_(J_._i)
let i be Element of I; ::_thesis: f . i is Element of (J . i)
 f . i = Bottom (J . i) by A28;
hence  f . i is Element of (J . i) ; ::_thesis: verum
end;
then reconsider f = f as Element of (product J) by A29, Th27;
set X =  {  (f +* (y | a)) where a is finite Subset of I : verum  }  ;
  {  (f +* (y | a)) where a is finite Subset of I : verum  }  c= the carrier of (product J)
proof
let a be set ; :: according to TARSKI:def_3 ::_thesis: ( not a in  {  (f +* (y | a)) where a is finite Subset of I : verum  }  or a in the carrier of (product J) )
assume  a in  {  (f +* (y | a)) where a is finite Subset of I : verum  }  ; ::_thesis: a in the carrier of (product J)
then consider b being finite Subset of I such that
A30: a = f +* (y | b) ;
 dom y = I by Th27;
then A31: dom (y | b) = b by RELAT_1:62;
then A32: I = I \/ (dom (y | b)) by XBOOLE_1:12
.= dom (f +* (y | b)) by A29, FUNCT_4:def_1 ;
now__::_thesis:_for_i_being_Element_of_I_holds_(f_+*_(y_|_b))_._i_is_Element_of_(J_._i)
let i be Element of I; ::_thesis: (f +* (y | b)) . i is Element of (J . i)
 ( (f +* (y | b)) . i = f . i or ( (f +* (y | b)) . i = (y | b) . i & (y | b) . i = y . i ) ) by A31, FUNCT_1:47, FUNCT_4:11, FUNCT_4:13;
hence  (f +* (y | b)) . i is Element of (J . i) ; ::_thesis: verum
end;
then  a is Element of (product J) by A30, A32, Th27;
hence  a in the carrier of (product J) ; ::_thesis: verum
end;
then reconsider X =  {  (f +* (y | a)) where a is finite Subset of I : verum  }  as Subset of (product J) ;
 f +* (y | ({} I)) in X ;
then reconsider X = X as non empty Subset of (product J) ;
 X is directed
proof
let z1, z2 be Element of (product J); :: according to WAYBEL_0:def_1 ::_thesis: ( not z1 in X or not z2 in X or ex b1 being Element of the carrier of (product J) st
( b1 in X & z1 <= b1 & z2 <= b1 ) )
assume  z1 in X ; ::_thesis: ( not z2 in X or ex b1 being Element of the carrier of (product J) st
( b1 in X & z1 <= b1 & z2 <= b1 ) )
then consider a1 being finite Subset of I such that
A33: z1 = f +* (y | a1) ;
assume  z2 in X ; ::_thesis: ex b1 being Element of the carrier of (product J) st
( b1 in X & z1 <= b1 & z2 <= b1 )
then consider a2 being finite Subset of I such that
A34: z2 = f +* (y | a2) ;
reconsider a = a1 \/ a2 as finite Subset of I ;
 f +* (y | a) in X ;
then reconsider z = f +* (y | a) as Element of (product J) ;
take  z ; ::_thesis: ( z in X & z1 <= z & z2 <= z )
thus  z in X ; ::_thesis: ( z1 <= z & z2 <= z )
A35: dom y = I by Th27;
then A36: dom (y | a) = a by RELAT_1:62;
A37: dom (y | a1) = a1 by A35, RELAT_1:62;
A38: dom (y | a2) = a2 by A35, RELAT_1:62;
now__::_thesis:_for_i_being_Element_of_I_holds_z_._i_>=_z1_._i
let i be Element of I; ::_thesis: z . b1 >= z1 . b1
 J . i is complete LATTICE by A1;
then A39: Bottom (J . i) <= y . i by YELLOW_0:44;
A40: f . i = Bottom (J . i) by A28;
percases ( ( not i in a1 & i in a ) or ( not i in a & not i in a1 ) or ( i in a1 & i in a ) ) by XBOOLE_0:def_3;
supposeA41: ( not i in a1 & i in a ) ; ::_thesis: z . b1 >= z1 . b1
then A42: z . i = (y | a) . i by A36, FUNCT_4:13;
 (y | a) . i = y . i by A36, A41, FUNCT_1:47;
hence  z . i >= z1 . i by A33, A37, A39, A40, A41, A42, FUNCT_4:11; ::_thesis: verum
end;
supposeA43: ( not i in a & not i in a1 ) ; ::_thesis: z . b1 >= z1 . b1
then A44: z . i = f . i by A36, FUNCT_4:11;
 z1 . i = f . i by A33, A37, A43, FUNCT_4:11;
hence  z . i >= z1 . i by A44, YELLOW_0:def_1; ::_thesis: verum
end;
supposeA45: ( i in a1 & i in a ) ; ::_thesis: z . b1 >= z1 . b1
then A46: z . i = (y | a) . i by A36, FUNCT_4:13;
A47: (y | a) . i = y . i by A36, A45, FUNCT_1:47;
A48: z1 . i = (y | a1) . i by A33, A37, A45, FUNCT_4:13;
 (y | a1) . i = y . i by A37, A45, FUNCT_1:47;
hence  z . i >= z1 . i by A46, A47, A48, YELLOW_0:def_1; ::_thesis: verum
end;
end;
end;
hence  z >= z1 by Th28; ::_thesis: z2 <= z
now__::_thesis:_for_i_being_Element_of_I_holds_z_._i_>=_z2_._i
let i be Element of I; ::_thesis: z . b1 >= z2 . b1
 J . i is complete LATTICE by A1;
then A49: Bottom (J . i) <= y . i by YELLOW_0:44;
A50: f . i = Bottom (J . i) by A28;
percases ( ( not i in a2 & i in a ) or ( not i in a & not i in a2 ) or ( i in a2 & i in a ) ) by XBOOLE_0:def_3;
supposeA51: ( not i in a2 & i in a ) ; ::_thesis: z . b1 >= z2 . b1
then A52: z . i = (y | a) . i by A36, FUNCT_4:13;
 (y | a) . i = y . i by A36, A51, FUNCT_1:47;
hence  z . i >= z2 . i by A34, A38, A49, A50, A51, A52, FUNCT_4:11; ::_thesis: verum
end;
supposeA53: ( not i in a & not i in a2 ) ; ::_thesis: z . b1 >= z2 . b1
then A54: z . i = f . i by A36, FUNCT_4:11;
 z2 . i = f . i by A34, A38, A53, FUNCT_4:11;
hence  z . i >= z2 . i by A54, YELLOW_0:def_1; ::_thesis: verum
end;
supposeA55: ( i in a2 & i in a ) ; ::_thesis: z . b1 >= z2 . b1
then A56: z . i = (y | a) . i by A36, FUNCT_4:13;
A57: (y | a) . i = y . i by A36, A55, FUNCT_1:47;
A58: z2 . i = (y | a2) . i by A34, A38, A55, FUNCT_4:13;
 (y | a2) . i = y . i by A38, A55, FUNCT_1:47;
hence  z . i >= z2 . i by A56, A57, A58, YELLOW_0:def_1; ::_thesis: verum
end;
end;
end;
hence  z2 <= z by Th28; ::_thesis: verum
end;
then reconsider X = X as non empty directed Subset of (product J) ;
now__::_thesis:_for_i_being_Element_of_I_holds_(sup_X)_._i_>=_y_._i
let i be Element of I; ::_thesis: (sup X) . i >= y . i
reconsider a = {i} as finite Subset of I ;
A59: f +* (y | a) in X ;
A60: product J = L9 ;
reconsider z = f +* (y | a) as Element of (product J) by A59;
A61: dom y = I by Th27;
A62: i in a by TARSKI:def_1;
then A63: (y | a) . i = y . i by FUNCT_1:49;
A64: dom (y | a) = a by A61, RELAT_1:62;
A65: z <= sup X by A59, A60, YELLOW_2:22;
 z . i = y . i by A62, A63, A64, FUNCT_4:13;
hence  (sup X) . i >= y . i by A65, Th28; ::_thesis: verum
end;
then  y <= sup X by Th28;
then consider d being Element of (product J) such that
A66: d in X and
A67: x <= d by A2, Def1;
consider a being finite Subset of I such that
A68: d = f +* (y | a) by A66;
 K c= a
proof
let j be set ; :: according to TARSKI:def_3 ::_thesis: ( not j in K or j in a )
assume  j in K ; ::_thesis: j in a
then consider i being Element of I such that
A69: j = i and
A70: x . i <> Bottom (J . i) ;
assume A71: not j in a ; ::_thesis: contradiction
 dom y = I by Th27;
then  dom (y | a) = a by RELAT_1:62;
then A72: d . i = f . i by A68, A69, A71, FUNCT_4:11
.= Bottom (J . i) by A28 ;
A73: J . i is complete LATTICE by A1;
A74: x . i <= d . i by A67, Th28;
 x . i >= Bottom (J . i) by A73, YELLOW_0:44;
hence  contradiction by A70, A72, A73, A74, ORDERS_2:2; ::_thesis: verum
end;
then reconsider K = K as finite Subset of I ;
take K = K; ::_thesis: for i being Element of I st not i in K holds
not x . i <> Bottom (J . i)
thus  for i being Element of I st not i in K holds
not x . i <> Bottom (J . i) ; ::_thesis: verum
end;
assume A75: for i being Element of I holds x . i << y . i ; ::_thesis: ( for K being finite Subset of I ex i being Element of I st
( not i in K & not x . i = Bottom (J . i) ) or x << y )
given K being finite Subset of I such that A76: for i being Element of I st not i in K holds
x . i = Bottom (J . i) ; ::_thesis: x << y
let D be non empty directed Subset of (product J); :: according to WAYBEL_3:def_1 ::_thesis: ( y <= sup D implies ex d being Element of (product J) st
( d in D & x <= d ) )
assume A77: y <= sup D ; ::_thesis: ex d being Element of (product J) st
( d in D & x <= d )
defpred S1[ set , set ] means  ex i being Element of I ex z being Element of (product J) st
( $1 = i & $2 = z & z . i >= x . i );
A78: now__::_thesis:_for_k_being_set_st_k_in_K_holds_
ex_a_being_set_st_
(_a_in_D_&_S1[k,a]_)
let k be set ; ::_thesis: ( k in K implies ex a being set st
( a in D & S1[k,a] ) )
assume  k in K ; ::_thesis: ex a being set st
( a in D & S1[k,a] )
then reconsider i = k as Element of I ;
A79: pi (D,i) is directed
proof
let a, b be Element of (J . i); :: according to WAYBEL_0:def_1 ::_thesis: ( not a in pi (D,i) or not b in pi (D,i) or ex b1 being Element of the carrier of (J . i) st
( b1 in pi (D,i) & a <= b1 & b <= b1 ) )
assume  a in pi (D,i) ; ::_thesis: ( not b in pi (D,i) or ex b1 being Element of the carrier of (J . i) st
( b1 in pi (D,i) & a <= b1 & b <= b1 ) )
then consider f being Function such that
A80: f in D and
A81: a = f . i by CARD_3:def_6;
assume  b in pi (D,i) ; ::_thesis: ex b1 being Element of the carrier of (J . i) st
( b1 in pi (D,i) & a <= b1 & b <= b1 )
then consider g being Function such that
A82: g in D and
A83: b = g . i by CARD_3:def_6;
reconsider f = f, g = g as Element of (product J) by A80, A82;
consider h being Element of (product J) such that
A84: h in D and
A85: h >= f and
A86: h >= g by A80, A82, WAYBEL_0:def_1;
take  h . i ; ::_thesis: ( h . i in pi (D,i) & a <= h . i & b <= h . i )
thus  ( h . i in pi (D,i) & a <= h . i & b <= h . i ) by A81, A83, A84, A85, A86, Th28, CARD_3:def_6; ::_thesis: verum
end;
set dd = the Element of D;
reconsider dd = the Element of D as Element of (product J) ;
A87: dd . i in pi (D,i) by CARD_3:def_6;
A88: x . i << y . i by A75;
A89: y . i <= (sup D) . i by A77, Th28;
 (sup D) . i = sup (pi (D,i)) by A1, Th32;
then consider zi being Element of (J . i) such that
A90: zi in pi (D,i) and
A91: zi >= x . i by A79, A87, A88, A89, Def1;
consider a being Function such that
A92: a in D and
A93: zi = a . i by A90, CARD_3:def_6;
reconsider a = a as set ;
take a = a; ::_thesis: ( a in D & S1[k,a] )
thus  a in D by A92; ::_thesis: S1[k,a]
thus  S1[k,a] by A91, A92, A93; ::_thesis: verum
end;
consider F being Function such that
A94: ( dom F = K & rng F c= D ) and
A95: for k being set st k in K holds
S1[k,F . k] from FUNCT_1:sch_5(A78);
reconsider Y = rng F as finite Subset of D by A94, FINSET_1:8;
 product J = L9 ;
then consider d being Element of (product J) such that
A96: d in D and
A97: d is_>=_than Y by WAYBEL_0:1;
take  d ; ::_thesis: ( d in D & x <= d )
thus  d in D by A96; ::_thesis: x <= d
now__::_thesis:_for_i_being_Element_of_I_holds_d_._i_>=_x_._i
let i be Element of I; ::_thesis: d . b1 >= x . b1
A98: J . i is complete LATTICE by A1;
percases ( i in K or not i in K ) ;
supposeA99: i in K ; ::_thesis: d . b1 >= x . b1
then consider j being Element of I, z being Element of (product J) such that
A100: i = j and
A101: F . i = z and
A102: z . j >= x . j by A95;
 z in Y by A94, A99, A101, FUNCT_1:def_3;
then  d >= z by A97, LATTICE3:def_9;
then  d . i >= z . i by Th28;
hence  d . i >= x . i by A98, A100, A102, YELLOW_0:def_2; ::_thesis: verum
end;
suppose not i in K ; ::_thesis: d . b1 >= x . b1
then  x . i = Bottom (J . i) by A76;
hence  d . i >= x . i by A98, YELLOW_0:44; ::_thesis: verum
end;
end;
end;
hence  x <= d by Th28; ::_thesis: verum
end;

begin

theorem Th34: :: WAYBEL_3:34
for T being non empty TopSpace
for x, y being Element of (InclPoset the topology of T) st x is_way_below y holds
for F being Subset-Family of T st F is open & y c= union F holds
ex G being finite Subset of F st x c= union G
proof
let T be non empty TopSpace; ::_thesis: for x, y being Element of (InclPoset the topology of T) st x is_way_below y holds
for F being Subset-Family of T st F is open & y c= union F holds
ex G being finite Subset of F st x c= union G
set L = InclPoset the topology of T;
let x, y be Element of (InclPoset the topology of T); ::_thesis: ( x is_way_below y implies for F being Subset-Family of T st F is open & y c= union F holds
ex G being finite Subset of F st x c= union G )
assume A1: x << y ; ::_thesis: for F being Subset-Family of T st F is open & y c= union F holds
ex G being finite Subset of F st x c= union G
let F be Subset-Family of T; ::_thesis: ( F is open & y c= union F implies ex G being finite Subset of F st x c= union G )
assume that
A2: F is open and
A3: y c= union F ; ::_thesis: ex G being finite Subset of F st x c= union G
reconsider A = F as Subset of (InclPoset the topology of T) by A2, YELLOW_1:25;
 sup A = union F by YELLOW_1:22;
then  y <= sup A by A3, YELLOW_1:3;
then consider B being finite Subset of (InclPoset the topology of T) such that
A4: B c= A and
A5: x <= sup B by A1, Th18;
reconsider G = B as finite Subset of F by A4;
take  G ; ::_thesis: x c= union G
 sup B = union G by YELLOW_1:22;
hence  x c= union G by A5, YELLOW_1:3; ::_thesis: verum
end;

theorem Th35: :: WAYBEL_3:35
for T being non empty TopSpace
for x, y being Element of (InclPoset the topology of T) st ( for F being Subset-Family of T st F is open & y c= union F holds
ex G being finite Subset of F st x c= union G ) holds
x is_way_below y
proof
let T be non empty TopSpace; ::_thesis: for x, y being Element of (InclPoset the topology of T) st ( for F being Subset-Family of T st F is open & y c= union F holds
ex G being finite Subset of F st x c= union G ) holds
x is_way_below y
set L = InclPoset the topology of T;
A1: InclPoset the topology of T = RelStr(# the topology of T,(RelIncl the topology of T) #) by YELLOW_1:def_1;
let x, y be Element of (InclPoset the topology of T); ::_thesis: ( ( for F being Subset-Family of T st F is open & y c= union F holds
ex G being finite Subset of F st x c= union G ) implies x is_way_below y )
assume A2: for F being Subset-Family of T st F is open & y c= union F holds
ex G being finite Subset of F st x c= union G ; ::_thesis: x is_way_below y
now__::_thesis:_for_I_being_Ideal_of_(InclPoset_the_topology_of_T)_st_y_<=_sup_I_holds_
x_in_I
let I be Ideal of (InclPoset the topology of T); ::_thesis: ( y <= sup I implies x in I )
reconsider F = I as Subset-Family of T by A1, XBOOLE_1:1;
assume  y <= sup I ; ::_thesis: x in I
then  y c= sup I by YELLOW_1:3;
then A3: y c= union F by YELLOW_1:22;
 F is open by YELLOW_1:25;
then consider G being finite Subset of F such that
A4: x c= union G by A2, A3;
reconsider G = G as finite Subset of (InclPoset the topology of T) by XBOOLE_1:1;
consider z being Element of (InclPoset the topology of T) such that
A5: z in I and
A6: z is_>=_than G by WAYBEL_0:1;
A7: union G = sup G by YELLOW_1:22;
A8: z >= sup G by A6, YELLOW_0:32;
A9: x <= sup G by A4, A7, YELLOW_1:3;
 sup G in I by A5, A8, WAYBEL_0:def_19;
hence  x in I by A9, WAYBEL_0:def_19; ::_thesis: verum
end;
hence  x is_way_below y by Th21; ::_thesis: verum
end;

theorem Th36: :: WAYBEL_3:36
for T being non empty TopSpace
for x being Element of (InclPoset the topology of T)
for X being Subset of T st x = X holds
( x is compact iff X is compact )
proof
let T be non empty TopSpace; ::_thesis: for x being Element of (InclPoset the topology of T)
for X being Subset of T st x = X holds
( x is compact iff X is compact )
let x be Element of (InclPoset the topology of T); ::_thesis: for X being Subset of T st x = X holds
( x is compact iff X is compact )
let X be Subset of T; ::_thesis: ( x = X implies ( x is compact iff X is compact ) )
assume A1: x = X ; ::_thesis: ( x is compact iff X is compact )
hereby  ::_thesis: ( X is compact implies x is compact )
assume  x is compact ; ::_thesis: X is compact
then A2: x << x by Def2;
thus  X is compact ::_thesis: verum
proof
let F be Subset-Family of T; :: according to COMPTS_1:def_4 ::_thesis: ( not F is Cover of X or not F is open or ex b1 being Element of K10(K10( the carrier of T)) st
( b1 c= F & b1 is Cover of X & b1 is finite ) )
assume that
A3: X c= union F and
A4: F is open ; :: according to SETFAM_1:def_11 ::_thesis: ex b1 being Element of K10(K10( the carrier of T)) st
( b1 c= F & b1 is Cover of X & b1 is finite )
consider G being finite Subset of F such that
A5: x c= union G by A1, A2, A3, A4, Th34;
reconsider G = G as Subset-Family of T by XBOOLE_1:1;
take  G ; ::_thesis: ( G c= F & G is Cover of X & G is finite )
thus  ( G c= F & X c= union G & G is finite ) by A1, A5; :: according to SETFAM_1:def_11 ::_thesis: verum
end;
end;
assume A6: for F being Subset-Family of T st F is Cover of X & F is open holds
ex G being Subset-Family of T st
( G c= F & G is Cover of X & G is finite ) ; :: according to COMPTS_1:def_4 ::_thesis: x is compact
now__::_thesis:_for_F_being_Subset-Family_of_T_st_F_is_open_&_x_c=_union_F_holds_
ex_G_being_finite_Subset_of_F_st_x_c=_union_G
let F be Subset-Family of T; ::_thesis: ( F is open & x c= union F implies ex G being finite Subset of F st x c= union G )
assume that
A7: F is open and
A8: x c= union F ; ::_thesis: ex G being finite Subset of F st x c= union G
 F is Cover of X by A1, A8, SETFAM_1:def_11;
then consider G being Subset-Family of T such that
A9: G c= F and
A10: G is Cover of X and
A11: G is finite by A6, A7;
 x c= union G by A1, A10, SETFAM_1:def_11;
hence  ex G being finite Subset of F st x c= union G by A9, A11; ::_thesis: verum
end;
hence  x << x by Th35; :: according to WAYBEL_3:def_2 ::_thesis: verum
end;

theorem :: WAYBEL_3:37
for T being non empty TopSpace
for x being Element of (InclPoset the topology of T) st x = the carrier of T holds
( x is compact iff T is compact )
proof
let T be non empty TopSpace; ::_thesis: for x being Element of (InclPoset the topology of T) st x = the carrier of T holds
( x is compact iff T is compact )
let x be Element of (InclPoset the topology of T); ::_thesis: ( x = the carrier of T implies ( x is compact iff T is compact ) )
assume A1: x = the carrier of T ; ::_thesis: ( x is compact iff T is compact )
 ( T is compact iff [#] T is compact ) by COMPTS_1:1;
hence  ( x is compact iff T is compact ) by A1, Th36; ::_thesis: verum
end;

definition
let T be non empty TopSpace;
attrT is locally-compact  means :Def9: :: WAYBEL_3:def 9
 for x being Point of T
for X being Subset of T st x in X & X is open holds
ex Y being Subset of T st
( x in Int Y & Y c= X & Y is compact );
end;

:: deftheorem Def9 defines locally-compact WAYBEL_3:def_9_:_
 for T being non empty TopSpace holds
( T is locally-compact iff for x being Point of T
for X being Subset of T st x in X & X is open holds
ex Y being Subset of T st
( x in Int Y & Y c= X & Y is compact ) );

registration
cluster non empty TopSpace-like T_2 compact  ->  non empty regular normal locally-compact for TopStruct ;
coherence
 for b1 being non empty TopSpace st b1 is compact & b1 is T_2 holds
( b1 is regular & b1 is normal & b1 is locally-compact )
proof
let T be non empty TopSpace; ::_thesis: ( T is compact & T is T_2 implies ( T is regular & T is normal & T is locally-compact ) )
assume A1: ( T is compact & T is T_2 ) ; ::_thesis: ( T is regular & T is normal & T is locally-compact )
hence A2: ( T is regular & T is normal ) by COMPTS_1:12, COMPTS_1:13; ::_thesis: T is locally-compact
A3: [#] T is compact by A1, COMPTS_1:1;
let x be Point of T; :: according to WAYBEL_3:def_9 ::_thesis: for X being Subset of T st x in X & X is open holds
ex Y being Subset of T st
( x in Int Y & Y c= X & Y is compact )
let X be Subset of T; ::_thesis: ( x in X & X is open implies ex Y being Subset of T st
( x in Int Y & Y c= X & Y is compact ) )
assume that
A4: x in X and
A5: X is open ; ::_thesis: ex Y being Subset of T st
( x in Int Y & Y c= X & Y is compact )
consider Y being open Subset of T such that
A6: x in Y and
A7: Cl Y c= X by A2, A4, A5, URYSOHN1:21;
take Z = Cl Y; ::_thesis: ( x in Int Z & Z c= X & Z is compact )
 Y c= Int Z by PRE_TOPC:18, TOPS_1:24;
hence  ( x in Int Z & Z c= X & Z is compact ) by A3, A6, A7, COMPTS_1:9; ::_thesis: verum
end;
end;

registration
cluster non empty TopSpace-like T_2 compact for TopStruct ;
existence
 ex b1 being non empty TopSpace st
( b1 is compact & b1 is T_2 )
proof
take  1TopSp {0} ; ::_thesis: ( 1TopSp {0} is compact & 1TopSp {0} is T_2 )
thus  ( 1TopSp {0} is compact & 1TopSp {0} is T_2 ) ; ::_thesis: verum
end;
end;

theorem Th38: :: WAYBEL_3:38
for T being non empty TopSpace
for x, y being Element of (InclPoset the topology of T) st ex Z being Subset of T st
( x c= Z & Z c= y & Z is compact ) holds
x << y
proof
let T be non empty TopSpace; ::_thesis: for x, y being Element of (InclPoset the topology of T) st ex Z being Subset of T st
( x c= Z & Z c= y & Z is compact ) holds
x << y
set L = InclPoset the topology of T;
let x, y be Element of (InclPoset the topology of T); ::_thesis: ( ex Z being Subset of T st
( x c= Z & Z c= y & Z is compact ) implies x << y )
given Z being Subset of T such that A1: x c= Z and
A2: Z c= y and
A3: Z is compact ; ::_thesis: x << y
A4: InclPoset the topology of T = RelStr(# the topology of T,(RelIncl the topology of T) #) by YELLOW_1:def_1;
then A5: x in the topology of T ;
 y in the topology of T by A4;
then reconsider X = x, Y = y as Subset of T by A5;
let D be non empty directed Subset of (InclPoset the topology of T); :: according to WAYBEL_3:def_1 ::_thesis: ( y <= sup D implies ex d being Element of (InclPoset the topology of T) st
( d in D & x <= d ) )
A6: sup D = union D by YELLOW_1:22;
reconsider F = D as Subset-Family of T by A4, XBOOLE_1:1;
reconsider F = F as Subset-Family of T ;
A7: F is open
proof
let a be Subset of T; :: according to TOPS_2:def_1 ::_thesis: ( not a in F or a is open )
assume  a in F ; ::_thesis: a is open
hence  a in the topology of T by A4; :: according to PRE_TOPC:def_2 ::_thesis: verum
end;
assume  y <= sup D ; ::_thesis: ex d being Element of (InclPoset the topology of T) st
( d in D & x <= d )
then  Y c= union F by A6, YELLOW_1:3;
then  Z c= union F by A2, XBOOLE_1:1;
then  F is Cover of Z by SETFAM_1:def_11;
then consider G being Subset-Family of T such that
A8: G c= F and
A9: G is Cover of Z and
A10: G is finite by A3, A7, COMPTS_1:def_4;
consider d being Element of (InclPoset the topology of T) such that
A11: d in D and
A12: d is_>=_than G by A8, A10, WAYBEL_0:1;
take  d ; ::_thesis: ( d in D & x <= d )
thus  d in D by A11; ::_thesis: x <= d
A13: now__::_thesis:_for_B_being_set_st_B_in_G_holds_
B_c=_d
let B be set ; ::_thesis: ( B in G implies B c= d )
assume A14: B in G ; ::_thesis: B c= d
then  B in D by A8;
then reconsider e = B as Element of (InclPoset the topology of T) ;
 d >= e by A12, A14, LATTICE3:def_9;
hence  B c= d by YELLOW_1:3; ::_thesis: verum
end;
A15: Z c= union G by A9, SETFAM_1:def_11;
 union G c= d by A13, ZFMISC_1:76;
then  Z c= d by A15, XBOOLE_1:1;
then  X c= d by A1, XBOOLE_1:1;
hence  x <= d by YELLOW_1:3; ::_thesis: verum
end;

theorem Th39: :: WAYBEL_3:39
for T being non empty TopSpace st T is locally-compact holds
for x, y being Element of (InclPoset the topology of T) st x << y holds
ex Z being Subset of T st
( x c= Z & Z c= y & Z is compact )
proof
let T be non empty TopSpace; ::_thesis: ( T is locally-compact implies for x, y being Element of (InclPoset the topology of T) st x << y holds
ex Z being Subset of T st
( x c= Z & Z c= y & Z is compact ) )
assume A1: for x being Point of T
for X being Subset of T st x in X & X is open holds
ex Y being Subset of T st
( x in Int Y & Y c= X & Y is compact ) ; :: according to WAYBEL_3:def_9 ::_thesis: for x, y being Element of (InclPoset the topology of T) st x << y holds
ex Z being Subset of T st
( x c= Z & Z c= y & Z is compact )
set L = InclPoset the topology of T;
A2: InclPoset the topology of T = RelStr(# the topology of T,(RelIncl the topology of T) #) by YELLOW_1:def_1;
let x, y be Element of (InclPoset the topology of T); ::_thesis: ( x << y implies ex Z being Subset of T st
( x c= Z & Z c= y & Z is compact ) )
assume A3: x << y ; ::_thesis: ex Z being Subset of T st
( x c= Z & Z c= y & Z is compact )
A4: x in the topology of T by A2;
 y in the topology of T by A2;
then reconsider X = x, Y = y as Subset of T by A4;
A5: Y is open by A2, PRE_TOPC:def_2;
set VV =  {  (Int Z) where Z is Subset of T : ( Z c= Y & Z is compact )  }  ;
reconsider e = {} T as Subset of T ;
A6: {} c= Y by XBOOLE_1:2;
 Int ({} T) = {} ;
then A7: e in  {  (Int Z) where Z is Subset of T : ( Z c= Y & Z is compact )  }  by A6;
  {  (Int Z) where Z is Subset of T : ( Z c= Y & Z is compact )  }  c= bool the carrier of T
proof
let a be set ; :: according to TARSKI:def_3 ::_thesis: ( not a in  {  (Int Z) where Z is Subset of T : ( Z c= Y & Z is compact )  }  or a in bool the carrier of T )
assume  a in  {  (Int Z) where Z is Subset of T : ( Z c= Y & Z is compact )  }  ; ::_thesis: a in bool the carrier of T
then  ex Z being Subset of T st
( a = Int Z & Z c= Y & Z is compact ) ;
hence  a in bool the carrier of T ; ::_thesis: verum
end;
then reconsider VV =  {  (Int Z) where Z is Subset of T : ( Z c= Y & Z is compact )  }  as non empty Subset-Family of T by A7;
set V = union VV;
 VV is open
proof
let a be Subset of T; :: according to TOPS_2:def_1 ::_thesis: ( not a in VV or a is open )
assume  a in VV ; ::_thesis: a is open
then  ex Z being Subset of T st
( a = Int Z & Z c= Y & Z is compact ) ;
hence  a is open ; ::_thesis: verum
end;
then reconsider A = VV as Subset of (InclPoset the topology of T) by YELLOW_1:25;
A8: sup A = union VV by YELLOW_1:22;
 Y c= union VV
proof
let a be set ; :: according to TARSKI:def_3 ::_thesis: ( not a in Y or a in union VV )
assume A9: a in Y ; ::_thesis: a in union VV
then reconsider a = a as Point of T ;
consider Z being Subset of T such that
A10: a in Int Z and
A11: Z c= Y and
A12: Z is compact by A1, A5, A9;
 Int Z in VV by A11, A12;
hence  a in union VV by A10, TARSKI:def_4; ::_thesis: verum
end;
then  y <= sup A by A8, YELLOW_1:3;
then consider B being finite Subset of (InclPoset the topology of T) such that
A13: B c= A and
A14: x <= sup B by A3, Th18;
defpred S1[ set , set ] means  ex Z being Subset of T st
( $2 = Z & $1 = Int Z & Z c= Y & Z is compact );
A15: now__::_thesis:_for_z_being_set_st_z_in_B_holds_
ex_s_being_set_st_S1[z,s]
let z be set ; ::_thesis: ( z in B implies ex s being set st S1[z,s] )
assume  z in B ; ::_thesis: ex s being set st S1[z,s]
then  z in A by A13;
then consider Z being Subset of T such that
A16: z = Int Z and
A17: Z c= Y and
A18: Z is compact ;
reconsider s = Z as set ;
take s = s; ::_thesis: S1[z,s]
thus  S1[z,s] by A16, A17, A18; ::_thesis: verum
end;
consider f being Function such that
A19: dom f = B and
A20: for z being set st z in B holds
S1[z,f . z] from CLASSES1:sch_1(A15);
reconsider W = B as Subset-Family of T by A2, XBOOLE_1:1;
 sup B = union W by YELLOW_1:22;
then A21: X c= union W by A14, YELLOW_1:3;
now__::_thesis:_for_z_being_set_st_z_in_rng_f_holds_
z_c=_the_carrier_of_T
let z be set ; ::_thesis: ( z in rng f implies z c= the carrier of T )
assume  z in rng f ; ::_thesis: z c= the carrier of T
then consider a being set  such that
A22: a in B and
A23: z = f . a by A19, FUNCT_1:def_3;
 ex Z being Subset of T st
( z = Z & a = Int Z & Z c= Y & Z is compact ) by A20, A22, A23;
hence  z c= the carrier of T ; ::_thesis: verum
end;
then reconsider Z = union (rng f) as Subset of T by ZFMISC_1:76;
take  Z ; ::_thesis: ( x c= Z & Z c= y & Z is compact )
thus  x c= Z ::_thesis: ( Z c= y & Z is compact )
proof
let z be set ; :: according to TARSKI:def_3 ::_thesis: ( not z in x or z in Z )
assume  z in x ; ::_thesis: z in Z
then consider a being set  such that
A24: z in a and
A25: a in W by A21, TARSKI:def_4;
consider Z being Subset of T such that
A26: f . a = Z and
A27: a = Int Z and
 Z c= Y and
 Z is compact by A20, A25;
A28: Int Z c= Z by TOPS_1:16;
 Z in rng f by A19, A25, A26, FUNCT_1:def_3;
hence  z in Z by A24, A27, A28, TARSKI:def_4; ::_thesis: verum
end;
thus  Z c= y ::_thesis: Z is compact
proof
let z be set ; :: according to TARSKI:def_3 ::_thesis: ( not z in Z or z in y )
assume  z in Z ; ::_thesis: z in y
then consider a being set  such that
A29: z in a and
A30: a in rng f by TARSKI:def_4;
consider Z being set  such that
A31: Z in W and
A32: a = f . Z by A19, A30, FUNCT_1:def_3;
 ex S being Subset of T st
( a = S & Z = Int S & S c= Y & S is compact ) by A20, A31, A32;
hence  z in y by A29; ::_thesis: verum
end;
A33: rng f is finite by A19, FINSET_1:8;
defpred S2[ set ] means  ex A being Subset of T st
( A = union $1 & A is compact );
 union {} = {} T by ZFMISC_1:2;
then A34: S2[ {} ] ;
A35: now__::_thesis:_for_x,_B_being_set_st_x_in_rng_f_&_B_c=_rng_f_&_S2[B]_holds_
S2[B_\/_{x}]
let x, B be set ; ::_thesis: ( x in rng f & B c= rng f & S2[B] implies S2[B \/ {x}] )
assume that
A36: x in rng f and
 B c= rng f ; ::_thesis: ( S2[B] implies S2[B \/ {x}] )
assume  S2[B] ; ::_thesis: S2[B \/ {x}]
then consider A being Subset of T such that
A37: A = union B and
A38: A is compact ;
thus  S2[B \/ {x}] ::_thesis: verum
proof
consider Z being set  such that
A39: Z in W and
A40: x = f . Z by A19, A36, FUNCT_1:def_3;
consider S being Subset of T such that
A41: x = S and
 Z = Int S and
 S c= Y and
A42: S is compact by A20, A39, A40;
reconsider Bx = A \/ S as Subset of T ;
take  Bx ; ::_thesis: ( Bx = union (B \/ {x}) & Bx is compact )
thus Bx = (union B) \/ (union {x}) by A37, A41, ZFMISC_1:25
.= union (B \/ {x}) by ZFMISC_1:78 ; ::_thesis: Bx is compact
thus  Bx is compact by A38, A42, COMPTS_1:10; ::_thesis: verum
end;
end;
 S2[ rng f] from FINSET_1:sch_2(A33, A34, A35);
hence  Z is compact ; ::_thesis: verum
end;

theorem :: WAYBEL_3:40
for T being non empty TopSpace st T is locally-compact & T is T_2 holds
for x, y being Element of (InclPoset the topology of T) st x << y holds
ex Z being Subset of T st
( Z = x & Cl Z c= y & Cl Z is compact )
proof
let T be non empty TopSpace; ::_thesis: ( T is locally-compact & T is T_2 implies for x, y being Element of (InclPoset the topology of T) st x << y holds
ex Z being Subset of T st
( Z = x & Cl Z c= y & Cl Z is compact ) )
assume that
A1: T is locally-compact and
A2: T is T_2 ; ::_thesis: for x, y being Element of (InclPoset the topology of T) st x << y holds
ex Z being Subset of T st
( Z = x & Cl Z c= y & Cl Z is compact )
set L = InclPoset the topology of T;
A3: InclPoset the topology of T = RelStr(# the topology of T,(RelIncl the topology of T) #) by YELLOW_1:def_1;
let x, y be Element of (InclPoset the topology of T); ::_thesis: ( x << y implies ex Z being Subset of T st
( Z = x & Cl Z c= y & Cl Z is compact ) )
assume  x << y ; ::_thesis: ex Z being Subset of T st
( Z = x & Cl Z c= y & Cl Z is compact )
then consider Z being Subset of T such that
A4: x c= Z and
A5: Z c= y and
A6: Z is compact by A1, Th39;
 x in the topology of T by A3;
then reconsider X = x as Subset of T ;
take  X ; ::_thesis: ( X = x & Cl X c= y & Cl X is compact )
thus  X = x ; ::_thesis: ( Cl X c= y & Cl X is compact )
 Cl X c= Z by A2, A4, A6, TOPS_1:5;
hence  ( Cl X c= y & Cl X is compact ) by A5, A6, COMPTS_1:9, XBOOLE_1:1; ::_thesis: verum
end;

theorem :: WAYBEL_3:41
for X being non empty TopSpace st X is regular & InclPoset the topology of X is continuous holds
X is locally-compact
proof
let T be non empty TopSpace; ::_thesis: ( T is regular & InclPoset the topology of T is continuous implies T is locally-compact )
set L = InclPoset the topology of T;
A1: InclPoset the topology of T = RelStr(# the topology of T,(RelIncl the topology of T) #) by YELLOW_1:def_1;
assume that
A2: T is regular and
A3: InclPoset the topology of T is continuous ; ::_thesis: T is locally-compact
let x be Point of T; :: according to WAYBEL_3:def_9 ::_thesis: for X being Subset of T st x in X & X is open holds
ex Y being Subset of T st
( x in Int Y & Y c= X & Y is compact )
let X be Subset of T; ::_thesis: ( x in X & X is open implies ex Y being Subset of T st
( x in Int Y & Y c= X & Y is compact ) )
assume that
A4: x in X and
A5: X is open ; ::_thesis: ex Y being Subset of T st
( x in Int Y & Y c= X & Y is compact )
reconsider a = X as Element of (InclPoset the topology of T) by A1, A5, PRE_TOPC:def_2;
a = sup (waybelow a) by A3, Def5
.= union (waybelow a) by YELLOW_1:22 ;
then consider Y being set  such that
A6: x in Y and
A7: Y in waybelow a by A4, TARSKI:def_4;
 Y in the carrier of (InclPoset the topology of T) by A7;
then reconsider Y = Y as Subset of T by A1;
consider y being Element of (InclPoset the topology of T) such that
A8: Y = y and
A9: y << a by A7;
 Y is open by A1, A7, PRE_TOPC:def_2;
then consider W being open Subset of T such that
A10: x in W and
A11: Cl W c= Y by A2, A6, URYSOHN1:21;
take Z = Cl W; ::_thesis: ( x in Int Z & Z c= X & Z is compact )
 W c= Z by PRE_TOPC:18;
hence  x in Int Z by A10, TOPS_1:22; ::_thesis: ( Z c= X & Z is compact )
 y <= a by A9, Th1;
then  Y c= X by A8, YELLOW_1:3;
hence  Z c= X by A11, XBOOLE_1:1; ::_thesis: Z is compact
let F be Subset-Family of T; :: according to COMPTS_1:def_4 ::_thesis: ( not F is Cover of Z or not F is open or ex b1 being Element of K10(K10( the carrier of T)) st
( b1 c= F & b1 is Cover of Z & b1 is finite ) )
assume that
A12: F is Cover of Z and
A13: F is open ; ::_thesis: ex b1 being Element of K10(K10( the carrier of T)) st
( b1 c= F & b1 is Cover of Z & b1 is finite )
reconsider ZZ = {(Z `)} as Subset-Family of T ;
reconsider ZZ = ZZ as Subset-Family of T ;
reconsider FZ = F \/ ZZ as Subset-Family of T ;
 for x being Subset of T st x in ZZ holds
x is open by TARSKI:def_1;
then  ZZ is open by TOPS_2:def_1;
then  FZ is open by A13, TOPS_2:13;
then reconsider FF = FZ as Subset of (InclPoset the topology of T) by YELLOW_1:25;
A14: sup FF = union FZ by YELLOW_1:22
.= (union F) \/ (union ZZ) by ZFMISC_1:78
.= (union F) \/ (Z `) by ZFMISC_1:25 ;
 Z c= union F by A12, SETFAM_1:def_11;
then  Z \/ (Z `) c= sup FF by A14, XBOOLE_1:9;
then  [#] T c= sup FF by PRE_TOPC:2;
then  X c= sup FF by XBOOLE_1:1;
then  a <= sup FF by YELLOW_1:3;
then consider A being finite Subset of (InclPoset the topology of T) such that
A15: A c= FF and
A16: y <= sup A by A9, Th18;
A17: sup A = union A by YELLOW_1:22;
reconsider G = A \ ZZ as Subset-Family of T by A1, XBOOLE_1:1;
take  G ; ::_thesis: ( G c= F & G is Cover of Z & G is finite )
thus  G c= F by A15, XBOOLE_1:43; ::_thesis: ( G is Cover of Z & G is finite )
thus  Z c= union G :: according to SETFAM_1:def_11 ::_thesis: G is finite
proof
let z be set ; :: according to TARSKI:def_3 ::_thesis: ( not z in Z or z in union G )
assume A18: z in Z ; ::_thesis: z in union G
then A19: z in Y by A11;
A20: Y c= union A by A8, A16, A17, YELLOW_1:3;
A21: not z in Z ` by A18, XBOOLE_0:def_5;
consider B being set  such that
A22: z in B and
A23: B in A by A19, A20, TARSKI:def_4;
 not B in ZZ by A21, A22, TARSKI:def_1;
then  B in G by A23, XBOOLE_0:def_5;
hence  z in union G by A22, TARSKI:def_4; ::_thesis: verum
end;
thus  G is finite ; ::_thesis: verum
end;

theorem :: WAYBEL_3:42
for T being non empty TopSpace st T is locally-compact holds
InclPoset the topology of T is continuous
proof
let T be non empty TopSpace; ::_thesis: ( T is locally-compact implies InclPoset the topology of T is continuous )
assume A1: T is locally-compact ; ::_thesis: InclPoset the topology of T is continuous
set L = InclPoset the topology of T;
A2: InclPoset the topology of T = RelStr(# the topology of T,(RelIncl the topology of T) #) by YELLOW_1:def_1;
thus  for x being Element of (InclPoset the topology of T) holds
( not waybelow x is empty & waybelow x is directed ) ; :: according to WAYBEL_3:def_6 ::_thesis: ( InclPoset the topology of T is up-complete & InclPoset the topology of T is satisfying_axiom_of_approximation )
thus  InclPoset the topology of T is up-complete ; ::_thesis: InclPoset the topology of T is satisfying_axiom_of_approximation
let x be Element of (InclPoset the topology of T); :: according to WAYBEL_3:def_5 ::_thesis: x = sup (waybelow x)
 x in the topology of T by A2;
then reconsider X = x as Subset of T ;
thus  x c= sup (waybelow x) :: according to XBOOLE_0:def_10 ::_thesis: sup (waybelow x) c= x
proof
let a be set ; :: according to TARSKI:def_3 ::_thesis: ( not a in x or a in sup (waybelow x) )
assume A3: a in x ; ::_thesis: a in sup (waybelow x)
 X is open by A2, PRE_TOPC:def_2;
then consider Y being Subset of T such that
A4: a in Int Y and
A5: Y c= X and
A6: Y is compact by A1, A3, Def9;
reconsider iY = Int Y as Subset of T ;
reconsider y = iY as Element of (InclPoset the topology of T) by A2, PRE_TOPC:def_2;
 y << x by A5, A6, Th38, TOPS_1:16;
then  y in waybelow x ;
then  y c= union (waybelow x) by ZFMISC_1:74;
then  y c= sup (waybelow x) by YELLOW_1:22;
hence  a in sup (waybelow x) by A4; ::_thesis: verum
end;
let a be set ; :: according to TARSKI:def_3 ::_thesis: ( not a in sup (waybelow x) or a in x )
assume  a in sup (waybelow x) ; ::_thesis: a in x
then  a in union (waybelow x) by YELLOW_1:22;
then consider Y being set  such that
A7: a in Y and
A8: Y in waybelow x by TARSKI:def_4;
consider y being Element of (InclPoset the topology of T) such that
A9: Y = y and
A10: y << x by A8;
 y <= x by A10, Th1;
then  Y c= x by A9, YELLOW_1:3;
hence  a in x by A7; ::_thesis: verum
end;