:: LATTICE7 semantic presentation

begin

definition
let L be 1-sorted ;
let A, B be Subset of L;
:: original: c=
redefine predA c= B means :: LATTICE7:def 1
 for x being Element of L st x in A holds
x in B;
compatibility
 ( A c= B iff for x being Element of L st x in A holds
x in B )
proof
 ( ( for x being Element of L st x in A holds
x in B ) implies A c= B )
proof
assume A1: for x being Element of L st x in A holds
x in B ; ::_thesis: A c= B
thus  A c= B ::_thesis: verum
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in A or x in B )
assume  x in A ; ::_thesis: x in B
hence  x in B by A1; ::_thesis: verum
end;
end;
hence  ( A c= B iff for x being Element of L st x in A holds
x in B ) ; ::_thesis: verum
end;
end;

:: deftheorem  defines c= LATTICE7:def_1_:_
 for L being 1-sorted
for A, B being Subset of L holds
( A c= B iff for x being Element of L st x in A holds
x in B );

registration
let L be LATTICE;
cluster non empty strongly_connected for Element of bool the carrier of L;
existence
 not for b1 being Chain of L holds b1 is empty
proof
 {(Bottom L)} is Chain of L by ORDERS_2:8;
hence  not for b1 being Chain of L holds b1 is empty ; ::_thesis: verum
end;
end;

definition
let L be LATTICE;
let x, y be Element of L;
assume B1: x <= y ;
mode Chain of x,y ->  non empty Chain of L means :Def2: :: LATTICE7:def 2
( x in it & y in it & ( for z being Element of L st z in it holds
( x <= z & z <= y ) ) );
existence
 ex b1 being non empty Chain of L st
( x in b1 & y in b1 & ( for z being Element of L st z in b1 holds
( x <= z & z <= y ) ) )
proof
reconsider A = {x,y} as non empty Chain of L by B1, ORDERS_2:9;
A1: for z being Element of L st z in A holds
( x <= z & z <= y )
proof
let z be Element of L; ::_thesis: ( z in A implies ( x <= z & z <= y ) )
assume A2: z in A ; ::_thesis: ( x <= z & z <= y )
percases ( z = x or z = y ) by A2, TARSKI:def_2;
suppose z = x ; ::_thesis: ( x <= z & z <= y )
hence  ( x <= z & z <= y ) by B1; ::_thesis: verum
end;
suppose z = y ; ::_thesis: ( x <= z & z <= y )
hence  ( x <= z & z <= y ) by B1; ::_thesis: verum
end;
end;
end;
 ( y in A & x in A ) by TARSKI:def_2;
hence  ex b1 being non empty Chain of L st
( x in b1 & y in b1 & ( for z being Element of L st z in b1 holds
( x <= z & z <= y ) ) ) by A1; ::_thesis: verum
end;
end;

:: deftheorem Def2 defines Chain LATTICE7:def_2_:_
 for L being LATTICE
for x, y being Element of L st x <= y holds
for b4 being non empty Chain of L holds
( b4 is Chain of x,y iff ( x in b4 & y in b4 & ( for z being Element of L st z in b4 holds
( x <= z & z <= y ) ) ) );

theorem Th1: :: LATTICE7:1
for L being LATTICE
for x, y being Element of L st x <= y holds
{x,y} is Chain of x,y
proof
let L be LATTICE; ::_thesis: for x, y being Element of L st x <= y holds
{x,y} is Chain of x,y
let x, y be Element of L; ::_thesis: ( x <= y implies {x,y} is Chain of x,y )
A1: ( x in {x,y} & y in {x,y} ) by TARSKI:def_2;
assume A2: x <= y ; ::_thesis: {x,y} is Chain of x,y
A3: for z being Element of L st z in {x,y} holds
( x <= z & z <= y )
proof
let z be Element of L; ::_thesis: ( z in {x,y} implies ( x <= z & z <= y ) )
assume A4: z in {x,y} ; ::_thesis: ( x <= z & z <= y )
percases ( z = x or z = y ) by A4, TARSKI:def_2;
suppose z = x ; ::_thesis: ( x <= z & z <= y )
hence  ( x <= z & z <= y ) by A2; ::_thesis: verum
end;
suppose z = y ; ::_thesis: ( x <= z & z <= y )
hence  ( x <= z & z <= y ) by A2; ::_thesis: verum
end;
end;
end;
 {x,y} is Chain of L by A2, ORDERS_2:9;
hence  {x,y} is Chain of x,y by A2, A1, A3, Def2; ::_thesis: verum
end;


definition
let L be finite LATTICE;
let x be Element of L;
func height x ->  Element of NAT  means :Def3: :: LATTICE7:def 3
( ex A being Chain of Bottom L,x st it = card A & ( for A being Chain of Bottom L,x holds card A <= it ) );
existence
 ex b1 being Element of NAT st
( ex A being Chain of Bottom L,x st b1 = card A & ( for A being Chain of Bottom L,x holds card A <= b1 ) )
proof
defpred S1[ Nat] means  ex A being Chain of Bottom L,x st $1 = card A;
A1: {(Bottom L),x} is Chain of Bottom L,x by Th1, YELLOW_0:44;
 ex k being Element of NAT st
( S1[k] & ( for n being Element of NAT st S1[n] holds
n <= k ) )
proof
 S1[ card {(Bottom L),x}] by A1;
then A2: ex k being Nat st S1[k] ;
A3: for k being Nat st S1[k] holds
k <= card the carrier of L by NAT_1:43;
consider k being Nat such that
A4: ( S1[k] & ( for n being Nat st S1[n] holds
n <= k ) ) from NAT_1:sch_6(A3, A2);
reconsider k = k as Element of NAT by ORDINAL1:def_12;
take  k ; ::_thesis: ( S1[k] & ( for n being Element of NAT st S1[n] holds
n <= k ) )
thus  ( S1[k] & ( for n being Element of NAT st S1[n] holds
n <= k ) ) by A4; ::_thesis: verum
end;
then consider k being Element of NAT  such that
A5: ( S1[k] & ( for n being Element of NAT st S1[n] holds
n <= k ) ) ;
take  k ; ::_thesis: ( ex A being Chain of Bottom L,x st k = card A & ( for A being Chain of Bottom L,x holds card A <= k ) )
thus  ( ex A being Chain of Bottom L,x st k = card A & ( for A being Chain of Bottom L,x holds card A <= k ) ) by A5; ::_thesis: verum
end;
uniqueness
 for b1, b2 being Element of NAT st ex A being Chain of Bottom L,x st b1 = card A & ( for A being Chain of Bottom L,x holds card A <= b1 ) & ex A being Chain of Bottom L,x st b2 = card A & ( for A being Chain of Bottom L,x holds card A <= b2 ) holds
b1 = b2
proof
let a, b be Element of NAT ; ::_thesis: ( ex A being Chain of Bottom L,x st a = card A & ( for A being Chain of Bottom L,x holds card A <= a ) & ex A being Chain of Bottom L,x st b = card A & ( for A being Chain of Bottom L,x holds card A <= b ) implies a = b )
assume  ( ex A being Chain of Bottom L,x st a = card A & ( for A being Chain of Bottom L,x holds card A <= a ) & ex B being Chain of Bottom L,x st b = card B & ( for A being Chain of Bottom L,x holds card A <= b ) ) ; ::_thesis: a = b
then  ( a <= b & b <= a ) ;
hence  a = b by XXREAL_0:1; ::_thesis: verum
end;
end;

:: deftheorem Def3 defines height LATTICE7:def_3_:_
 for L being finite LATTICE
for x being Element of L
for b3 being Element of NAT holds
( b3 = height x iff ( ex A being Chain of Bottom L,x st b3 = card A & ( for A being Chain of Bottom L,x holds card A <= b3 ) ) );

theorem Th2: :: LATTICE7:2
for L being finite LATTICE
for a, b being Element of L st a < b holds
height a < height b
proof
let L be finite LATTICE; ::_thesis: for a, b being Element of L st a < b holds
height a < height b
let a, b be Element of L; ::_thesis: ( a < b implies height a < height b )
 ( ex A being Chain of Bottom L,a st height a = card A & ( for C being Chain of Bottom L,a holds card C <= height a ) ) by Def3;
then consider A being Chain of Bottom L,a such that
A1: height a = card A and
 for C being Chain of Bottom L,a holds card C <= height a ;
set C = A \/ {b};
 b in {b} by TARSKI:def_1;
then A2: b in A \/ {b} by XBOOLE_0:def_3;
A3: Bottom L <= a by YELLOW_0:44;
then  Bottom L in A by Def2;
then A4: Bottom L in A \/ {b} by XBOOLE_0:def_3;
assume A5: a < b ; ::_thesis: height a < height b
 not b in A
proof
assume  b in A ; ::_thesis: contradiction
then  b <= a by A3, Def2;
hence  contradiction by A5, ORDERS_2:6; ::_thesis: verum
end;
then A6: card (A \/ {b}) = (card A) + 1 by CARD_2:41;
 the InternalRel of L is_strongly_connected_in A \/ {b}
proof
let x, y be set ; :: according to RELAT_2:def_7 ::_thesis: ( not x in A \/ {b} or not y in A \/ {b} or [x,y] in the InternalRel of L or [y,x] in the InternalRel of L )
 ( x in A \/ {b} & y in A \/ {b} & not [x,y] in the InternalRel of L implies [y,x] in the InternalRel of L )
proof
assume A7: ( x in A \/ {b} & y in A \/ {b} ) ; ::_thesis: ( [x,y] in the InternalRel of L or [y,x] in the InternalRel of L )
percases ( ( x in A & y in A ) or ( x in A & y in {b} ) or ( x in {b} & y in A ) or ( x in {b} & y in {b} ) ) by A7, XBOOLE_0:def_3;
supposeA8: ( x in A & y in A ) ; ::_thesis: ( [x,y] in the InternalRel of L or [y,x] in the InternalRel of L )
then reconsider x = x, y = y as Element of L ;
 ( x <= y or y <= x ) by A8, ORDERS_2:11;
hence  ( [x,y] in the InternalRel of L or [y,x] in the InternalRel of L ) by ORDERS_2:def_5; ::_thesis: verum
end;
supposeA9: ( x in A & y in {b} ) ; ::_thesis: ( [x,y] in the InternalRel of L or [y,x] in the InternalRel of L )
then reconsider x = x as Element of L ;
 Bottom L <= a by YELLOW_0:44;
then  x <= a by A9, Def2;
then  x < b by A5, ORDERS_2:7;
then A10: x <= b by ORDERS_2:def_6;
 y = b by A9, TARSKI:def_1;
hence  ( [x,y] in the InternalRel of L or [y,x] in the InternalRel of L ) by A10, ORDERS_2:def_5; ::_thesis: verum
end;
supposeA11: ( x in {b} & y in A ) ; ::_thesis: ( [x,y] in the InternalRel of L or [y,x] in the InternalRel of L )
then reconsider y = y as Element of L ;
 Bottom L <= a by YELLOW_0:44;
then  y <= a by A11, Def2;
then  y < b by A5, ORDERS_2:7;
then A12: y <= b by ORDERS_2:def_6;
 x = b by A11, TARSKI:def_1;
hence  ( [x,y] in the InternalRel of L or [y,x] in the InternalRel of L ) by A12, ORDERS_2:def_5; ::_thesis: verum
end;
supposeA13: ( x in {b} & y in {b} ) ; ::_thesis: ( [x,y] in the InternalRel of L or [y,x] in the InternalRel of L )
then reconsider x = x, y = y as Element of L ;
 x = b by A13, TARSKI:def_1;
then  x <= y by A13, TARSKI:def_1;
hence  ( [x,y] in the InternalRel of L or [y,x] in the InternalRel of L ) by ORDERS_2:def_5; ::_thesis: verum
end;
end;
end;
hence  ( not x in A \/ {b} or not y in A \/ {b} or [x,y] in the InternalRel of L or [y,x] in the InternalRel of L ) ; ::_thesis: verum
end;
then A14: A \/ {b} is strongly_connected Subset of L by ORDERS_2:def_7;
A15: for z being Element of L st z in A \/ {b} holds
( Bottom L <= z & z <= b )
proof
let z be Element of L; ::_thesis: ( z in A \/ {b} implies ( Bottom L <= z & z <= b ) )
assume A16: z in A \/ {b} ; ::_thesis: ( Bottom L <= z & z <= b )
percases ( z in A or z in {b} ) by A16, XBOOLE_0:def_3;
supposeA17: z in A ; ::_thesis: ( Bottom L <= z & z <= b )
thus  Bottom L <= z by YELLOW_0:44; ::_thesis: z <= b
 z <= a by A3, A17, Def2;
then  z < b by A5, ORDERS_2:7;
hence  z <= b by ORDERS_2:def_6; ::_thesis: verum
end;
suppose z in {b} ; ::_thesis: ( Bottom L <= z & z <= b )
hence  ( Bottom L <= z & z <= b ) by TARSKI:def_1, YELLOW_0:44; ::_thesis: verum
end;
end;
end;
 Bottom L <= b by YELLOW_0:44;
then  A \/ {b} is Chain of Bottom L,b by A4, A2, A15, A14, Def2;
then  (height a) + 1 <= height b by A1, A6, Def3;
hence  height a < height b by NAT_1:13; ::_thesis: verum
end;

theorem Th3: :: LATTICE7:3
for L being finite LATTICE
for C being Chain of L
for x, y being Element of L st x in C & y in C holds
( x < y iff height x < height y )
proof
let L be finite LATTICE; ::_thesis: for C being Chain of L
for x, y being Element of L st x in C & y in C holds
( x < y iff height x < height y )
let C be Chain of L; ::_thesis: for x, y being Element of L st x in C & y in C holds
( x < y iff height x < height y )
let x, y be Element of L; ::_thesis: ( x in C & y in C implies ( x < y iff height x < height y ) )
assume A1: ( x in C & y in C ) ; ::_thesis: ( x < y iff height x < height y )
 ( height x < height y implies x < y )
proof
assume A2: height x < height y ; ::_thesis: x < y
percases ( x <= y or y <= x ) by A1, ORDERS_2:11;
suppose x <= y ; ::_thesis: x < y
hence  x < y by A2, ORDERS_2:def_6; ::_thesis: verum
end;
suppose y <= x ; ::_thesis: x < y
then  ( x = y or y < x ) by ORDERS_2:def_6;
hence  x < y by A2, Th2; ::_thesis: verum
end;
end;
end;
hence  ( x < y iff height x < height y ) by Th2; ::_thesis: verum
end;

theorem Th4: :: LATTICE7:4
for L being finite LATTICE
for C being Chain of L
for x, y being Element of L st x in C & y in C holds
( x = y iff height x = height y )
proof
let L be finite LATTICE; ::_thesis: for C being Chain of L
for x, y being Element of L st x in C & y in C holds
( x = y iff height x = height y )
let C be Chain of L; ::_thesis: for x, y being Element of L st x in C & y in C holds
( x = y iff height x = height y )
let x, y be Element of L; ::_thesis: ( x in C & y in C implies ( x = y iff height x = height y ) )
assume A1: ( x in C & y in C ) ; ::_thesis: ( x = y iff height x = height y )
thus  ( x = y implies height x = height y ) ; ::_thesis: ( height x = height y implies x = y )
 ( height x = height y implies x = y )
proof
assume that
A2: height x = height y and
A3: x <> y ; ::_thesis: contradiction
A4: ( x <= y or y <= x ) by A1, ORDERS_2:11;
 height x <> height y
proof
percases ( x < y or y < x ) by A3, A4, ORDERS_2:def_6;
suppose x < y ; ::_thesis: height x <> height y
hence  height x <> height y by A1, Th3; ::_thesis: verum
end;
suppose y < x ; ::_thesis: height x <> height y
hence  height x <> height y by A1, Th3; ::_thesis: verum
end;
end;
end;
hence  contradiction by A2; ::_thesis: verum
end;
hence  ( height x = height y implies x = y ) ; ::_thesis: verum
end;

theorem Th5: :: LATTICE7:5
for L being finite LATTICE
for C being Chain of L
for x, y being Element of L st x in C & y in C holds
( x <= y iff height x <= height y )
proof
let L be finite LATTICE; ::_thesis: for C being Chain of L
for x, y being Element of L st x in C & y in C holds
( x <= y iff height x <= height y )
let C be Chain of L; ::_thesis: for x, y being Element of L st x in C & y in C holds
( x <= y iff height x <= height y )
let x, y be Element of L; ::_thesis: ( x in C & y in C implies ( x <= y iff height x <= height y ) )
assume A1: ( x in C & y in C ) ; ::_thesis: ( x <= y iff height x <= height y )
A2: ( height x <= height y implies x <= y )
proof
assume  height x <= height y ; ::_thesis: x <= y
then  ( height x < height y or height x = height y ) by XXREAL_0:1;
then  ( x < y or height x = height y ) by A1, Th3;
hence  x <= y by A1, Th4, ORDERS_2:def_6; ::_thesis: verum
end;
 ( x <= y implies height x <= height y )
proof
assume  x <= y ; ::_thesis: height x <= height y
then  ( x < y or x = y ) by ORDERS_2:def_6;
hence  height x <= height y by A1, Th3; ::_thesis: verum
end;
hence  ( x <= y iff height x <= height y ) by A2; ::_thesis: verum
end;

theorem :: LATTICE7:6
for L being finite LATTICE
for x being Element of L holds
( height x = 1 iff x = Bottom L )
proof
let L be finite LATTICE; ::_thesis: for x being Element of L holds
( height x = 1 iff x = Bottom L )
let x be Element of L; ::_thesis: ( height x = 1 iff x = Bottom L )
A1: ( x = Bottom L implies height x = 1 )
proof
A2: for B being Chain of Bottom L, Bottom L holds B = {(Bottom L)}
proof
let B be Chain of Bottom L, Bottom L; ::_thesis: B = {(Bottom L)}
A3: B c= {(Bottom L)}
proof
let r be set ; :: according to LATTICE7:def_1 ::_thesis: ( r is Element of L & r in B implies r in {(Bottom L)} )
 ( r in B implies r in {(Bottom L)} )
proof
assume  r in B ; ::_thesis: r in {(Bottom L)}
then reconsider r = r as Element of B ;
 ( Bottom L <= r & r <= Bottom L ) by Def2;
then  Bottom L = r by ORDERS_2:2;
hence  r in {(Bottom L)} by TARSKI:def_1; ::_thesis: verum
end;
hence  ( r is Element of L & r in B implies r in {(Bottom L)} ) ; ::_thesis: verum
end;
 {(Bottom L)} c= B
proof
let r be set ; :: according to LATTICE7:def_1 ::_thesis: ( r is Element of L & r in {(Bottom L)} implies r in B )
 ( r in {(Bottom L)} implies r in B )
proof
assume  r in {(Bottom L)} ; ::_thesis: r in B
then  r = Bottom L by TARSKI:def_1;
hence  r in B by Def2; ::_thesis: verum
end;
hence  ( r is Element of L & r in {(Bottom L)} implies r in B ) ; ::_thesis: verum
end;
hence  B = {(Bottom L)} by A3, XBOOLE_0:def_10; ::_thesis: verum
end;
assume A4: x = Bottom L ; ::_thesis: height x = 1
 ( ex A being Chain of Bottom L, Bottom L st height (Bottom L) = card A & card {(Bottom L)} = 1 ) by Def3, CARD_1:30;
hence  height x = 1 by A4, A2; ::_thesis: verum
end;
 ( height x = 1 implies x = Bottom L )
proof
A5: for z being Element of L st z in {(Bottom L),x} holds
( Bottom L <= z & z <= x )
proof
let z be Element of L; ::_thesis: ( z in {(Bottom L),x} implies ( Bottom L <= z & z <= x ) )
assume A6: z in {(Bottom L),x} ; ::_thesis: ( Bottom L <= z & z <= x )
percases ( z = Bottom L or z = x ) by A6, TARSKI:def_2;
suppose z = Bottom L ; ::_thesis: ( Bottom L <= z & z <= x )
hence  ( Bottom L <= z & z <= x ) by YELLOW_0:44; ::_thesis: verum
end;
suppose z = x ; ::_thesis: ( Bottom L <= z & z <= x )
hence  ( Bottom L <= z & z <= x ) by YELLOW_0:44; ::_thesis: verum
end;
end;
end;
A7: ( x in {(Bottom L),x} & Bottom L in {(Bottom L),x} ) by TARSKI:def_2;
A8: Bottom L <= x by YELLOW_0:44;
then  {(Bottom L),x} is Chain of L by ORDERS_2:9;
then A9: {(Bottom L),x} is Chain of Bottom L,x by A8, A7, A5, Def2;
assume that
A10: height x = 1 and
A11: x <> Bottom L ; ::_thesis: contradiction
 card {(Bottom L),x} = 2 by A11, CARD_2:57;
hence  contradiction by A10, A9, Def3; ::_thesis: verum
end;
hence  ( height x = 1 iff x = Bottom L ) by A1; ::_thesis: verum
end;

theorem Th7: :: LATTICE7:7
for L being non empty finite LATTICE
for x being Element of L holds height x >= 1
proof
let L be non empty finite LATTICE; ::_thesis: for x being Element of L holds height x >= 1
let x be Element of L; ::_thesis: height x >= 1
A1: {(Bottom L),x} is Chain of Bottom L,x by Th1, YELLOW_0:44;
then A2: card {(Bottom L),x} <= height x by Def3;
percases ( x <> Bottom L or x = Bottom L ) ;
suppose x <> Bottom L ; ::_thesis: height x >= 1
then  card {(Bottom L),x} = 2 by CARD_2:57;
hence  height x >= 1 by A2, XXREAL_0:2; ::_thesis: verum
end;
supposeA3: x = Bottom L ; ::_thesis: height x >= 1
A4: {(Bottom L)} c= {(Bottom L),(Bottom L)}
proof
let d be Element of L; :: according to LATTICE7:def_1 ::_thesis: ( d in {(Bottom L)} implies d in {(Bottom L),(Bottom L)} )
assume  d in {(Bottom L)} ; ::_thesis: d in {(Bottom L),(Bottom L)}
then  d = Bottom L by TARSKI:def_1;
hence  d in {(Bottom L),(Bottom L)} by TARSKI:def_2; ::_thesis: verum
end;
 {(Bottom L),(Bottom L)} c= {(Bottom L)}
proof
let d be Element of L; :: according to LATTICE7:def_1 ::_thesis: ( d in {(Bottom L),(Bottom L)} implies d in {(Bottom L)} )
assume  d in {(Bottom L),(Bottom L)} ; ::_thesis: d in {(Bottom L)}
then  ( d = Bottom L or d = Bottom L ) by TARSKI:def_2;
hence  d in {(Bottom L)} by TARSKI:def_1; ::_thesis: verum
end;
then A5: {(Bottom L),(Bottom L)} = {(Bottom L)} by A4, XBOOLE_0:def_10;
 card {(Bottom L),(Bottom L)} <= height (Bottom L) by A1, A3, Def3;
hence  height x >= 1 by A3, A5, CARD_1:30; ::_thesis: verum
end;
end;
end;

scheme :: LATTICE7:sch 1
LattInd{ F1() ->  finite LATTICE, P1[ set ] } :
 for x being Element of F1() holds P1[x]
provided
A1: for x being Element of F1() st ( for b being Element of F1() st b < x holds
P1[b] ) holds
P1[x]
proof
defpred S1[ Element of NAT ] means  for x being Element of F1() st height x <= $1 holds
P1[x];
A2: for n being Element of NAT st S1[n] holds
S1[n + 1]
proof
let n be Element of NAT ; ::_thesis: ( S1[n] implies S1[n + 1] )
assume A3: S1[n] ; ::_thesis: S1[n + 1]
 for x being Element of F1() st height x <= n + 1 holds
P1[x]
proof
let x be Element of F1(); ::_thesis: ( height x <= n + 1 implies P1[x] )
assume A4: height x <= n + 1 ; ::_thesis: P1[x]
percases ( height x = n + 1 or P1[x] ) by A3, A4, NAT_1:8;
supposeA5: height x = n + 1 ; ::_thesis: P1[x]
 for y being Element of F1() st y < x holds
P1[y]
proof
let y be Element of F1(); ::_thesis: ( y < x implies P1[y] )
assume  y < x ; ::_thesis: P1[y]
then  height y < height x by Th2;
then  height y <= n by A5, NAT_1:13;
hence  P1[y] by A3; ::_thesis: verum
end;
hence  P1[x] by A1; ::_thesis: verum
end;
suppose P1[x] ; ::_thesis: P1[x]
hence  P1[x] ; ::_thesis: verum
end;
end;
end;
hence  S1[n + 1] ; ::_thesis: verum
end;
let x be Element of F1(); ::_thesis: P1[x]
A6: ( ( for x being Element of F1() st height x <= height x holds
P1[x] ) implies for x being Element of F1() holds P1[x] )
proof
assume that
A7: for x being Element of F1() st height x <= height x holds
P1[x] and
A8: not for x being Element of F1() holds P1[x] ; ::_thesis: contradiction
consider x being Element of F1() such that
A9: P1[x] by A8;
 ( height x <= height x implies P1[x] ) by A7;
hence  contradiction by A9; ::_thesis: verum
end;
A10: S1[ 0 ] by Th7;
 for n being Element of NAT holds S1[n] from NAT_1:sch_1(A10, A2);
hence  P1[x] by A6; ::_thesis: verum
end;

begin

registration
cluster non empty finite V117() reflexive transitive antisymmetric distributive with_suprema with_infima for RelStr ;
existence
 ex b1 being LATTICE st
( b1 is distributive & b1 is finite )
proof
set D = {{}};
set R = the Order of {{}};
reconsider A = RelStr(# {{}}, the Order of {{}} #) as with_suprema with_infima Poset ;
take  A ; ::_thesis: ( A is distributive & A is finite )
thus  ( A is distributive & A is finite ) ; ::_thesis: verum
end;
end;

definition
let L be LATTICE;
let x, y be Element of L;
predx <(1) y means :Def4: :: LATTICE7:def 4
( x < y & ( for z being Element of L holds
( not x < z or not z < y ) ) );
end;

:: deftheorem Def4 defines <(1) LATTICE7:def_4_:_
 for L being LATTICE
for x, y being Element of L holds
( x <(1) y iff ( x < y & ( for z being Element of L holds
( not x < z or not z < y ) ) ) );

theorem Th8: :: LATTICE7:8
for L being finite LATTICE
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 finite LATTICE; ::_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 ) )
let X be non empty Subset of L; ::_thesis: ex x being Element of L st
( x in X & ( for y being Element of L st y in X holds
not x < y ) )
defpred S1[ Nat] means  ex x being Element of L st
( x in X & $1 = height x );
 ex k being Element of NAT st
( S1[k] & ( for n being Element of NAT st S1[n] holds
n <= k ) )
proof
A1: for k being Nat st S1[k] holds
k <= card the carrier of L
proof
let k be Nat; ::_thesis: ( S1[k] implies k <= card the carrier of L )
assume  S1[k] ; ::_thesis: k <= card the carrier of L
then consider x being Element of L such that
 x in X and
A2: k = height x ;
 ex B being Chain of Bottom L,x st k = card B by A2, Def3;
hence  k <= card the carrier of L by NAT_1:43; ::_thesis: verum
end;
A3: ex k being Nat st S1[k]
proof
consider x being set  such that
A4: x in X by XBOOLE_0:def_1;
reconsider x = x as Element of L by A4;
 ex B being Chain of Bottom L,x st height x = card B by Def3;
hence  ex k being Nat st S1[k] by A4; ::_thesis: verum
end;
consider k being Nat such that
A5: S1[k] and
A6: for n being Nat st S1[n] holds
n <= k from NAT_1:sch_6(A1, A3);
 for n being Element of NAT st S1[n] holds
n <= k by A6;
hence  ex k being Element of NAT st
( S1[k] & ( for n being Element of NAT st S1[n] holds
n <= k ) ) by A5; ::_thesis: verum
end;
then consider k being Element of NAT  such that
A7: ( S1[k] & ( for n being Element of NAT st S1[n] holds
n <= k ) ) ;
consider x being Element of L such that
A8: x in X and
A9: ( k = height x & ( for n being Element of NAT st ex y being Element of L st
( y in X & n = height y ) holds
n <= k ) ) by A7;
 for y being Element of L st y in X holds
not x < y
proof
let y be Element of L; ::_thesis: ( y in X implies not x < y )
assume that
A10: y in X and
A11: x < y ; ::_thesis: contradiction
 height x < height y by A11, Th2;
hence  contradiction by A9, A10; ::_thesis: verum
end;
hence  ex x being Element of L st
( x in X & ( for y being Element of L st y in X holds
not x < y ) ) by A8; ::_thesis: verum
end;

definition
let L be finite LATTICE;
let A be non empty Chain of L;
func max A ->  Element of L means :Def5: :: LATTICE7:def 5
( ( for x being Element of L st x in A holds
x <= it ) & it in A );
existence
 ex b1 being Element of L st
( ( for x being Element of L st x in A holds
x <= b1 ) & b1 in A )
proof
defpred S1[ Nat] means  ex x being Element of L st
( x in A & $1 = height x );
 ex k being Element of NAT st
( S1[k] & ( for n being Element of NAT st S1[n] holds
n <= k ) )
proof
A1: for k being Nat st S1[k] holds
k <= card the carrier of L
proof
let k be Nat; ::_thesis: ( S1[k] implies k <= card the carrier of L )
assume  S1[k] ; ::_thesis: k <= card the carrier of L
then consider x being Element of L such that
 x in A and
A2: k = height x ;
 ex B being Chain of Bottom L,x st k = card B by A2, Def3;
hence  k <= card the carrier of L by NAT_1:43; ::_thesis: verum
end;
A3: ex k being Nat st S1[k]
proof
consider x being set  such that
A4: x in A by XBOOLE_0:def_1;
reconsider x = x as Element of L by A4;
 ex B being Chain of Bottom L,x st height x = card B by Def3;
hence  ex k being Nat st S1[k] by A4; ::_thesis: verum
end;
consider k being Nat such that
A5: S1[k] and
A6: for n being Nat st S1[n] holds
n <= k from NAT_1:sch_6(A1, A3);
 for n being Element of NAT st S1[n] holds
n <= k by A6;
hence  ex k being Element of NAT st
( S1[k] & ( for n being Element of NAT st S1[n] holds
n <= k ) ) by A5; ::_thesis: verum
end;
then consider k being Element of NAT  such that
A7: ( S1[k] & ( for n being Element of NAT st S1[n] holds
n <= k ) ) ;
consider x being Element of L such that
A8: x in A and
A9: ( k = height x & ( for n being Element of NAT st ex z being Element of L st
( z in A & n = height z ) holds
n <= k ) ) by A7;
take  x ; ::_thesis: ( ( for x being Element of L st x in A holds
x <= x ) & x in A )
thus  for w being Element of L st w in A holds
w <= x ::_thesis: x in A
proof
let w be Element of L; ::_thesis: ( w in A implies w <= x )
assume A10: w in A ; ::_thesis: w <= x
then  height w <= height x by A9;
hence  w <= x by A8, A10, Th5; ::_thesis: verum
end;
thus  x in A by A8; ::_thesis: verum
end;
uniqueness
 for b1, b2 being Element of L st ( for x being Element of L st x in A holds
x <= b1 ) & b1 in A & ( for x being Element of L st x in A holds
x <= b2 ) & b2 in A holds
b1 = b2
proof
let s, t be Element of L; ::_thesis: ( ( for x being Element of L st x in A holds
x <= s ) & s in A & ( for x being Element of L st x in A holds
x <= t ) & t in A implies s = t )
assume  ( ( for x being Element of L st x in A holds
x <= s ) & s in A & ( for y being Element of L st y in A holds
y <= t ) & t in A ) ; ::_thesis: s = t
then  ( t <= s & s <= t ) ;
hence  s = t by ORDERS_2:2; ::_thesis: verum
end;
end;

:: deftheorem Def5 defines max LATTICE7:def_5_:_
 for L being finite LATTICE
for A being non empty Chain of L
for b3 being Element of L holds
( b3 = max A iff ( ( for x being Element of L st x in A holds
x <= b3 ) & b3 in A ) );

theorem Th9: :: LATTICE7:9
for L being finite LATTICE
for y being Element of L st y <> Bottom L holds
ex x being Element of L st x <(1) y
proof
let L be finite LATTICE; ::_thesis: for y being Element of L st y <> Bottom L holds
ex x being Element of L st x <(1) y
let y be Element of L; ::_thesis: ( y <> Bottom L implies ex x being Element of L st x <(1) y )
 ( ex A being Chain of Bottom L,y st height y = card A & ( for A being Chain of Bottom L,y holds card A <= height y ) ) by Def3;
then consider A being Chain of Bottom L,y such that
A1: ( height y = card A & ( for A being Chain of Bottom L,y holds card A <= height y ) ) ;
set B = A \ {y};
A2: the InternalRel of L is_strongly_connected_in A \ {y}
proof
let p, q be set ; :: according to RELAT_2:def_7 ::_thesis: ( not p in A \ {y} or not q in A \ {y} or [p,q] in the InternalRel of L or [q,p] in the InternalRel of L )
 ( p in A \ {y} & q in A \ {y} & not [p,q] in the InternalRel of L implies [q,p] in the InternalRel of L )
proof
assume A3: ( p in A \ {y} & q in A \ {y} ) ; ::_thesis: ( [p,q] in the InternalRel of L or [q,p] in the InternalRel of L )
then A4: ( p in A & q in A ) by XBOOLE_0:def_5;
reconsider p = p, q = q as Element of L by A3;
 ( p <= q or q <= p ) by A4, ORDERS_2:11;
hence  ( [p,q] in the InternalRel of L or [q,p] in the InternalRel of L ) by ORDERS_2:def_5; ::_thesis: verum
end;
hence  ( not p in A \ {y} or not q in A \ {y} or [p,q] in the InternalRel of L or [q,p] in the InternalRel of L ) ; ::_thesis: verum
end;
assume A5: y <> Bottom L ; ::_thesis: ex x being Element of L st x <(1) y
 not A \ {y} is empty
proof
 Bottom L <= y by YELLOW_0:44;
then A6: Bottom L in A by Def2;
assume A7: A \ {y} is empty ; ::_thesis: contradiction
 not Bottom L in {y} by A5, TARSKI:def_1;
hence  contradiction by A7, A6, XBOOLE_0:def_5; ::_thesis: verum
end;
then reconsider B = A \ {y} as non empty Chain of L by A2, ORDERS_2:def_7;
take x = max B; ::_thesis: x <(1) y
A8: for z being Element of L holds
( not x < z or not z < y )
proof
given z being Element of L such that A9: x < z and
A10: z < y ; ::_thesis: contradiction
A11: Bottom L <= y by YELLOW_0:44;
then  y in A by Def2;
then A12: y in A \/ {z} by XBOOLE_0:def_3;
set C = A \/ {z};
 {y} c= A
proof
let h be Element of L; :: according to LATTICE7:def_1 ::_thesis: ( h in {y} implies h in A )
assume  h in {y} ; ::_thesis: h in A
then A13: h = y by TARSKI:def_1;
 Bottom L <= y by YELLOW_0:44;
hence  h in A by A13, Def2; ::_thesis: verum
end;
then A14: A = (A \ {y}) \/ {y} by XBOOLE_1:45;
 the InternalRel of L is_strongly_connected_in A \/ {z}
proof
let x1, y1 be set ; :: according to RELAT_2:def_7 ::_thesis: ( not x1 in A \/ {z} or not y1 in A \/ {z} or [x1,y1] in the InternalRel of L or [y1,x1] in the InternalRel of L )
 ( x1 in A \/ {z} & y1 in A \/ {z} & not [x1,y1] in the InternalRel of L implies [y1,x1] in the InternalRel of L )
proof
assume A15: ( x1 in A \/ {z} & y1 in A \/ {z} ) ; ::_thesis: ( [x1,y1] in the InternalRel of L or [y1,x1] in the InternalRel of L )
percases ( ( x1 in A & y1 in A ) or ( x1 in A & y1 in {z} ) or ( y1 in A & x1 in {z} ) or ( x1 in {z} & y1 in {z} ) ) by A15, XBOOLE_0:def_3;
supposeA16: ( x1 in A & y1 in A ) ; ::_thesis: ( [x1,y1] in the InternalRel of L or [y1,x1] in the InternalRel of L )
then reconsider x1 = x1, y1 = y1 as Element of L ;
 ( x1 <= y1 or y1 <= x1 ) by A16, ORDERS_2:11;
hence  ( [x1,y1] in the InternalRel of L or [y1,x1] in the InternalRel of L ) by ORDERS_2:def_5; ::_thesis: verum
end;
supposeA17: ( x1 in A & y1 in {z} ) ; ::_thesis: ( [x1,y1] in the InternalRel of L or [y1,x1] in the InternalRel of L )
then A18: y1 = z by TARSKI:def_1;
reconsider x1 = x1, y1 = y1 as Element of L by A17;
 ( x1 in A \ {y} or x1 in {y} ) by A14, A17, XBOOLE_0:def_3;
then  ( x1 <= x or x1 = y ) by Def5, TARSKI:def_1;
then  ( x1 < y1 or x1 = y ) by A9, A18, ORDERS_2:7;
then  ( x1 <= y1 or y1 < x1 ) by A10, A17, ORDERS_2:def_6, TARSKI:def_1;
then  ( x1 <= y1 or y1 <= x1 ) by ORDERS_2:def_6;
hence  ( [x1,y1] in the InternalRel of L or [y1,x1] in the InternalRel of L ) by ORDERS_2:def_5; ::_thesis: verum
end;
supposeA19: ( y1 in A & x1 in {z} ) ; ::_thesis: ( [x1,y1] in the InternalRel of L or [y1,x1] in the InternalRel of L )
then A20: x1 = z by TARSKI:def_1;
reconsider x1 = x1, y1 = y1 as Element of L by A19;
 ( y1 in A \ {y} or y1 in {y} ) by A14, A19, XBOOLE_0:def_3;
then  ( y1 <= x or y1 = y ) by Def5, TARSKI:def_1;
then  ( y1 < x1 or y1 = y ) by A9, A20, ORDERS_2:7;
then  ( y1 <= x1 or x1 <= y1 ) by A10, A20, ORDERS_2:def_6;
hence  ( [x1,y1] in the InternalRel of L or [y1,x1] in the InternalRel of L ) by ORDERS_2:def_5; ::_thesis: verum
end;
supposeA21: ( x1 in {z} & y1 in {z} ) ; ::_thesis: ( [x1,y1] in the InternalRel of L or [y1,x1] in the InternalRel of L )
then reconsider x1 = x1, y1 = y1 as Element of L ;
 x1 = z by A21, TARSKI:def_1;
then  x1 <= y1 by A21, TARSKI:def_1;
hence  ( [x1,y1] in the InternalRel of L or [y1,x1] in the InternalRel of L ) by ORDERS_2:def_5; ::_thesis: verum
end;
end;
end;
hence  ( not x1 in A \/ {z} or not y1 in A \/ {z} or [x1,y1] in the InternalRel of L or [y1,x1] in the InternalRel of L ) ; ::_thesis: verum
end;
then A22: A \/ {z} is strongly_connected Subset of L by ORDERS_2:def_7;
A23: z <= y by A10, ORDERS_2:def_6;
A24: for v being Element of L st v in A \/ {z} holds
( Bottom L <= v & v <= y )
proof
let v be Element of L; ::_thesis: ( v in A \/ {z} implies ( Bottom L <= v & v <= y ) )
assume A25: v in A \/ {z} ; ::_thesis: ( Bottom L <= v & v <= y )
percases ( v in A or v in {z} ) by A25, XBOOLE_0:def_3;
supposeA26: v in A ; ::_thesis: ( Bottom L <= v & v <= y )
thus  Bottom L <= v by YELLOW_0:44; ::_thesis: v <= y
thus  v <= y by A11, A26, Def2; ::_thesis: verum
end;
suppose v in {z} ; ::_thesis: ( Bottom L <= v & v <= y )
hence  ( Bottom L <= v & v <= y ) by A23, TARSKI:def_1, YELLOW_0:44; ::_thesis: verum
end;
end;
end;
 not z in A
proof
assume A27: z in A ; ::_thesis: contradiction
 not z in {y} by A10, TARSKI:def_1;
then  z in B by A27, XBOOLE_0:def_5;
then  z <= x by Def5;
hence  contradiction by A9, ORDERS_2:7; ::_thesis: verum
end;
then A28: card (A \/ {z}) = (card A) + 1 by CARD_2:41;
 Bottom L in A by A11, Def2;
then  Bottom L in A \/ {z} by XBOOLE_0:def_3;
then  A \/ {z} is Chain of Bottom L,y by A22, A11, A12, A24, Def2;
then  (card A) + 1 <= card A by A1, A28;
hence  contradiction by NAT_1:13; ::_thesis: verum
end;
A29: x in B by Def5;
then  not x in {y} by XBOOLE_0:def_5;
then A30: not x = y by TARSKI:def_1;
 ( Bottom L <= y & x in A ) by A29, XBOOLE_0:def_5, YELLOW_0:44;
then  x <= y by Def2;
then  x < y by A30, ORDERS_2:def_6;
hence  x <(1) y by A8, Def4; ::_thesis: verum
end;

definition
let L be LATTICE;
func Join-IRR L ->  Subset of L equals :: LATTICE7:def 6
 {  a where a is Element of L : ( a <> Bottom L & ( for b, c being Element of L holds
( not a = b "\/" c or a = b or a = c ) ) )  }  ;
coherence
  {  a where a is Element of L : ( a <> Bottom L & ( for b, c being Element of L holds
( not a = b "\/" c or a = b or a = c ) ) )  }  is Subset of L
proof
  {  a where a is Element of L : ( a <> Bottom L & ( for b, c being Element of L holds
( not a = b "\/" c or a = b or a = c ) ) )  }  c= the carrier of L
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in  {  a where a is Element of L : ( a <> Bottom L & ( for b, c being Element of L holds
( not a = b "\/" c or a = b or a = c ) ) )  }  or x in the carrier of L )
assume  x in  {  a where a is Element of L : ( a <> Bottom L & ( for b, c being Element of L holds
( not a = b "\/" c or a = b or a = c ) ) )  }  ; ::_thesis: x in the carrier of L
then  ex a being Element of L st
( x = a & a <> Bottom L & ( for b, c being Element of L holds
( not a = b "\/" c or a = b or a = c ) ) ) ;
hence  x in the carrier of L ; ::_thesis: verum
end;
hence   {  a where a is Element of L : ( a <> Bottom L & ( for b, c being Element of L holds
( not a = b "\/" c or a = b or a = c ) ) )  }  is Subset of L ; ::_thesis: verum
end;
end;

:: deftheorem  defines Join-IRR LATTICE7:def_6_:_
 for L being LATTICE holds Join-IRR L =  {  a where a is Element of L : ( a <> Bottom L & ( for b, c being Element of L holds
( not a = b "\/" c or a = b or a = c ) ) )  }  ;

theorem Th10: :: LATTICE7:10
for L being LATTICE
for x being Element of L holds
( x in Join-IRR L iff ( x <> Bottom L & ( for b, c being Element of L holds
( not x = b "\/" c or x = b or x = c ) ) ) )
proof
let L be LATTICE; ::_thesis: for x being Element of L holds
( x in Join-IRR L iff ( x <> Bottom L & ( for b, c being Element of L holds
( not x = b "\/" c or x = b or x = c ) ) ) )
let x be Element of L; ::_thesis: ( x in Join-IRR L iff ( x <> Bottom L & ( for b, c being Element of L holds
( not x = b "\/" c or x = b or x = c ) ) ) )
thus  ( x in Join-IRR L implies ( x <> Bottom L & ( for b, c being Element of L holds
( not x = b "\/" c or x = b or x = c ) ) ) ) ::_thesis: ( x <> Bottom L & ( for b, c being Element of L holds
( not x = b "\/" c or x = b or x = c ) ) implies x in Join-IRR L )
proof
assume  x in Join-IRR L ; ::_thesis: ( x <> Bottom L & ( for b, c being Element of L holds
( not x = b "\/" c or x = b or x = c ) ) )
then  ex a being Element of L st
( x = a & a <> Bottom L & ( for b, c being Element of L holds
( not a = b "\/" c or a = b or a = c ) ) ) ;
hence  ( x <> Bottom L & ( for b, c being Element of L holds
( not x = b "\/" c or x = b or x = c ) ) ) ; ::_thesis: verum
end;
thus  ( x <> Bottom L & ( for b, c being Element of L holds
( not x = b "\/" c or x = b or x = c ) ) implies x in Join-IRR L ) ; ::_thesis: verum
end;

theorem Th11: :: LATTICE7:11
for L being finite distributive LATTICE
for x being Element of L st x in Join-IRR L holds
ex z being Element of L st
( z < x & ( for y being Element of L st y < x holds
y <= z ) )
proof
let L be finite distributive LATTICE; ::_thesis: for x being Element of L st x in Join-IRR L holds
ex z being Element of L st
( z < x & ( for y being Element of L st y < x holds
y <= z ) )
let x be Element of L; ::_thesis: ( x in Join-IRR L implies ex z being Element of L st
( z < x & ( for y being Element of L st y < x holds
y <= z ) ) )
assume A1: x in Join-IRR L ; ::_thesis: ex z being Element of L st
( z < x & ( for y being Element of L st y < x holds
y <= z ) )
then  x <> Bottom L by Th10;
then consider z being Element of L such that
A2: z <(1) x by Th9;
A3: z < x by A2, Def4;
 for y being Element of L st y < x holds
y <= z
proof
let y be Element of L; ::_thesis: ( y < x implies y <= z )
consider Y being set  such that
A4: Y =  {  g where g is Element of L : ( g < x & not g <= z )  }  ;
A5: Y is empty
proof
A6: Y c= the carrier of L
proof
let f be set ; :: according to TARSKI:def_3 ::_thesis: ( not f in Y or f in the carrier of L )
assume  f in Y ; ::_thesis: f in the carrier of L
then  ex g being Element of L st
( g = f & g < x & not g <= z ) by A4;
hence  f in the carrier of L ; ::_thesis: verum
end;
assume  not Y is empty ; ::_thesis: contradiction
then consider a being Element of L such that
A7: a in Y and
A8: for b being Element of L st b in Y holds
not a < b by A6, Th8;
A9: for t being Element of L holds
( t in Y iff ( t < x & not t <= z ) )
proof
let t be Element of L; ::_thesis: ( t in Y iff ( t < x & not t <= z ) )
 ( t in Y implies ( t < x & not t <= z ) )
proof
assume  t in Y ; ::_thesis: ( t < x & not t <= z )
then  ex g being Element of L st
( g = t & g < x & not g <= z ) by A4;
hence  ( t < x & not t <= z ) ; ::_thesis: verum
end;
hence  ( t in Y iff ( t < x & not t <= z ) ) by A4; ::_thesis: verum
end;
then A10: not a <= z by A7;
A11: z <= x by A3, ORDERS_2:def_6;
 a < x by A9, A7;
then A12: a "\/" z <> x by A1, A3, Th10;
 a < x by A9, A7;
then  a <= x by ORDERS_2:def_6;
then  a "\/" z <= x by A11, YELLOW_5:9;
then A13: a "\/" z < x by A12, ORDERS_2:def_6;
 a "/\" a <= a "\/" z by YELLOW_5:5;
then A14: a <= a "\/" z by YELLOW_5:2;
 a <> a "\/" z
proof
assume  a = a "\/" z ; ::_thesis: contradiction
 z "/\" z <= a "\/" z by YELLOW_5:5;
then  z <= a "\/" z by YELLOW_5:2;
then  z < a "\/" z by A10, A14, ORDERS_2:def_6;
hence  contradiction by A2, A13, Def4; ::_thesis: verum
end;
then A15: a "\/" z > a by A14, ORDERS_2:def_6;
 not a "\/" z <= z by A10, YELLOW_5:3;
then  a "\/" z in Y by A9, A13;
hence  contradiction by A8, A15; ::_thesis: verum
end;
assume  ( y < x & not y <= z ) ; ::_thesis: contradiction
then  y in Y by A4;
hence  contradiction by A5; ::_thesis: verum
end;
hence  ex z being Element of L st
( z < x & ( for y being Element of L st y < x holds
y <= z ) ) by A3; ::_thesis: verum
end;

Lm1:  for L being finite distributive LATTICE
for a being Element of L st ( for b being Element of L st b < a holds
sup ((downarrow b) /\ (Join-IRR L)) = b ) holds
sup ((downarrow a) /\ (Join-IRR L)) = a
proof
let L be finite distributive LATTICE; ::_thesis: for a being Element of L st ( for b being Element of L st b < a holds
sup ((downarrow b) /\ (Join-IRR L)) = b ) holds
sup ((downarrow a) /\ (Join-IRR L)) = a
let a be Element of L; ::_thesis: ( ( for b being Element of L st b < a holds
sup ((downarrow b) /\ (Join-IRR L)) = b ) implies sup ((downarrow a) /\ (Join-IRR L)) = a )
assume A1: for b being Element of L st b < a holds
sup ((downarrow b) /\ (Join-IRR L)) = b ; ::_thesis: sup ((downarrow a) /\ (Join-IRR L)) = a
thus  sup ((downarrow a) /\ (Join-IRR L)) = a ::_thesis: verum
proof
percases ( a = Bottom L or ( not a in Join-IRR L & a <> Bottom L ) or a in Join-IRR L ) ;
supposeA2: a = Bottom L ; ::_thesis: sup ((downarrow a) /\ (Join-IRR L)) = a
A3: {(Bottom L)} /\ (Join-IRR L) = {}
proof
set x = the Element of {(Bottom L)} /\ (Join-IRR L);
assume A4: {(Bottom L)} /\ (Join-IRR L) <> {} ; ::_thesis: contradiction
then  the Element of {(Bottom L)} /\ (Join-IRR L) in {(Bottom L)} by XBOOLE_0:def_4;
then A5: the Element of {(Bottom L)} /\ (Join-IRR L) = Bottom L by TARSKI:def_1;
 the Element of {(Bottom L)} /\ (Join-IRR L) in Join-IRR L by A4, XBOOLE_0:def_4;
hence  contradiction by A5, Th10; ::_thesis: verum
end;
 downarrow a = {(Bottom L)} by A2, WAYBEL_4:23;
hence  sup ((downarrow a) /\ (Join-IRR L)) = a by A2, A3, YELLOW_0:def_11; ::_thesis: verum
end;
suppose ( not a in Join-IRR L & a <> Bottom L ) ; ::_thesis: sup ((downarrow a) /\ (Join-IRR L)) = a
then consider y, z being Element of L such that
A6: a = y "\/" z and
A7: a <> y and
A8: a <> z ;
A9: y <= a by A6, YELLOW_0:22;
then A10: y < a by A7, ORDERS_2:def_6;
A11: (downarrow a) /\ (Join-IRR L) c= ((downarrow y) /\ (Join-IRR L)) \/ ((downarrow z) /\ (Join-IRR L))
proof
let x be Element of L; :: according to LATTICE7:def_1 ::_thesis: ( x in (downarrow a) /\ (Join-IRR L) implies x in ((downarrow y) /\ (Join-IRR L)) \/ ((downarrow z) /\ (Join-IRR L)) )
set x1 = x;
set y1 = y;
set a1 = a;
set z1 = z;
assume A12: x in (downarrow a) /\ (Join-IRR L) ; ::_thesis: x in ((downarrow y) /\ (Join-IRR L)) \/ ((downarrow z) /\ (Join-IRR L))
then A13: x in Join-IRR L by XBOOLE_0:def_4;
 x in downarrow a by A12, XBOOLE_0:def_4;
then A14: x <= a by WAYBEL_0:17;
 x "/\" a = (x "/\" y) "\/" (x "/\" z) by A6, WAYBEL_1:def_3;
then  x = (x "/\" y) "\/" (x "/\" z) by A14, YELLOW_0:25;
then  ( x = x "/\" y or x = x "/\" z ) by A13, Th10;
then  ( x <= y or x <= z ) by YELLOW_0:25;
then  ( x in downarrow y or x in downarrow z ) by WAYBEL_0:17;
then  ( x in (downarrow y) /\ (Join-IRR L) or x in (downarrow z) /\ (Join-IRR L) ) by A13, XBOOLE_0:def_4;
hence  x in ((downarrow y) /\ (Join-IRR L)) \/ ((downarrow z) /\ (Join-IRR L)) by XBOOLE_0:def_3; ::_thesis: verum
end;
A15: ( ex_sup_of ((downarrow y) /\ (Join-IRR L)) \/ ((downarrow z) /\ (Join-IRR L)),L & ex_sup_of (downarrow y) /\ (Join-IRR L),L ) by YELLOW_0:17;
A16: ex_sup_of (downarrow z) /\ (Join-IRR L),L by YELLOW_0:17;
A17: z <= a by A6, YELLOW_0:22;
 ((downarrow y) /\ (Join-IRR L)) \/ ((downarrow z) /\ (Join-IRR L)) c= (downarrow a) /\ (Join-IRR L)
proof
let x be Element of L; :: according to LATTICE7:def_1 ::_thesis: ( x in ((downarrow y) /\ (Join-IRR L)) \/ ((downarrow z) /\ (Join-IRR L)) implies x in (downarrow a) /\ (Join-IRR L) )
 ( (downarrow y) /\ (Join-IRR L) c= (downarrow a) /\ (Join-IRR L) & (downarrow z) /\ (Join-IRR L) c= (downarrow a) /\ (Join-IRR L) ) by A9, A17, WAYBEL_0:21, XBOOLE_1:26;
then A18: ((downarrow y) /\ (Join-IRR L)) \/ ((downarrow z) /\ (Join-IRR L)) c= (downarrow a) /\ (Join-IRR L) by XBOOLE_1:8;
assume  x in ((downarrow y) /\ (Join-IRR L)) \/ ((downarrow z) /\ (Join-IRR L)) ; ::_thesis: x in (downarrow a) /\ (Join-IRR L)
hence  x in (downarrow a) /\ (Join-IRR L) by A18; ::_thesis: verum
end;
then  (downarrow a) /\ (Join-IRR L) = ((downarrow y) /\ (Join-IRR L)) \/ ((downarrow z) /\ (Join-IRR L)) by A11, XBOOLE_0:def_10;
then  sup ((downarrow a) /\ (Join-IRR L)) = (sup ((downarrow y) /\ (Join-IRR L))) "\/" (sup ((downarrow z) /\ (Join-IRR L))) by A15, A16, YELLOW_0:36;
then A19: sup ((downarrow a) /\ (Join-IRR L)) = y "\/" (sup ((downarrow z) /\ (Join-IRR L))) by A1, A10;
 z < a by A8, A17, ORDERS_2:def_6;
hence  sup ((downarrow a) /\ (Join-IRR L)) = a by A1, A6, A19; ::_thesis: verum
end;
supposeA20: a in Join-IRR L ; ::_thesis: sup ((downarrow a) /\ (Join-IRR L)) = a
 a <= a ;
then  a in downarrow a by WAYBEL_0:17;
then  a in (downarrow a) /\ (Join-IRR L) by A20, XBOOLE_0:def_4;
then A21: a <= sup ((downarrow a) /\ (Join-IRR L)) by YELLOW_0:17, YELLOW_4:1;
 ( ex_sup_of (downarrow a) /\ (Join-IRR L),L & ex_sup_of downarrow a,L ) by YELLOW_0:17;
then  sup ((downarrow a) /\ (Join-IRR L)) <= sup (downarrow a) by XBOOLE_1:17, YELLOW_0:34;
then  sup ((downarrow a) /\ (Join-IRR L)) <= a by WAYBEL_0:34;
hence  sup ((downarrow a) /\ (Join-IRR L)) = a by A21, ORDERS_2:2; ::_thesis: verum
end;
end;
end;
end;

theorem Th12: :: LATTICE7:12
for L being finite distributive LATTICE
for x being Element of L holds sup ((downarrow x) /\ (Join-IRR L)) = x
proof
let L be finite distributive LATTICE; ::_thesis: for x being Element of L holds sup ((downarrow x) /\ (Join-IRR L)) = x
let x be Element of L; ::_thesis: sup ((downarrow x) /\ (Join-IRR L)) = x
A1: x <= sup ((downarrow x) /\ (Join-IRR L))
proof
defpred S1[ Element of L] means  sup ((downarrow $1) /\ (Join-IRR L)) = $1;
A2: for x being Element of L st ( for b being Element of L st b < x holds
S1[b] ) holds
S1[x] by Lm1;
 for x being Element of L holds S1[x] from LATTICE7:sch_1(A2);
hence  x <= sup ((downarrow x) /\ (Join-IRR L)) ; ::_thesis: verum
end;
 ( ex_sup_of (downarrow x) /\ (Join-IRR L),L & ex_sup_of downarrow x,L ) by YELLOW_0:17;
then  sup ((downarrow x) /\ (Join-IRR L)) <= sup (downarrow x) by XBOOLE_1:17, YELLOW_0:34;
then  sup ((downarrow x) /\ (Join-IRR L)) <= x by WAYBEL_0:34;
hence  sup ((downarrow x) /\ (Join-IRR L)) = x by A1, ORDERS_2:2; ::_thesis: verum
end;

begin

definition
let P be RelStr ;
func LOWER P ->  non empty set  equals :: LATTICE7:def 7
 {  X where X is Subset of P : X is lower  }  ;
coherence
  {  X where X is Subset of P : X is lower  }  is non empty set
proof
 {} P in  {  X where X is Subset of P : X is lower  }  ;
hence   {  X where X is Subset of P : X is lower  }  is non empty set ; ::_thesis: verum
end;
end;

:: deftheorem  defines LOWER LATTICE7:def_7_:_
 for P being RelStr holds LOWER P =  {  X where X is Subset of P : X is lower  }  ;

theorem Th13: :: LATTICE7:13
for L being finite distributive LATTICE ex r being Function of L,(InclPoset (LOWER (subrelstr (Join-IRR L)))) st
( r is isomorphic & ( for a being Element of L holds r . a = (downarrow a) /\ (Join-IRR L) ) )
proof
let L be finite distributive LATTICE; ::_thesis: ex r being Function of L,(InclPoset (LOWER (subrelstr (Join-IRR L)))) st
( r is isomorphic & ( for a being Element of L holds r . a = (downarrow a) /\ (Join-IRR L) ) )
set I = InclPoset (LOWER (subrelstr (Join-IRR L)));
deffunc H1( Element of L) ->  Element of bool the carrier of L = (downarrow $1) /\ (Join-IRR L);
consider r being ManySortedSet of the carrier of L such that
A1: for d being Element of L holds r . d = H1(d) from PBOOLE:sch_5();
A2: rng r c= the carrier of (InclPoset (LOWER (subrelstr (Join-IRR L))))
proof
let t be set ; :: according to TARSKI:def_3 ::_thesis: ( not t in rng r or t in the carrier of (InclPoset (LOWER (subrelstr (Join-IRR L)))) )
assume  t in rng r ; ::_thesis: t in the carrier of (InclPoset (LOWER (subrelstr (Join-IRR L))))
then consider x being set  such that
A3: x in dom r and
A4: t = r . x by FUNCT_1:def_3;
reconsider x = x as Element of L by A3;
A5: t = (downarrow x) /\ (Join-IRR L) by A1, A4;
then  t c= Join-IRR L by XBOOLE_1:17;
then reconsider t = t as Subset of (subrelstr (Join-IRR L)) by YELLOW_0:def_15;
A6: t is lower
proof
let c, d be Element of (subrelstr (Join-IRR L)); :: according to WAYBEL_0:def_19 ::_thesis: ( not c in t or not d <= c or d in t )
assume that
A7: c in t and
A8: d <= c ; ::_thesis: d in t
A9: d is Element of Join-IRR L by YELLOW_0:def_15;
A10: not Join-IRR L is empty by A5, A7;
then  d in Join-IRR L by A9;
then reconsider c1 = c, d1 = d as Element of L by A5, A7;
 c in downarrow x by A5, A7, XBOOLE_0:def_4;
then A11: c1 <= x by WAYBEL_0:17;
 d1 <= c1 by A8, YELLOW_0:59;
then  d1 <= x by A11, ORDERS_2:3;
then  d1 in downarrow x by WAYBEL_0:17;
hence  d in t by A5, A10, A9, XBOOLE_0:def_4; ::_thesis: verum
end;
 the carrier of (InclPoset (LOWER (subrelstr (Join-IRR L)))) = LOWER (subrelstr (Join-IRR L)) by YELLOW_1:1;
hence  t in the carrier of (InclPoset (LOWER (subrelstr (Join-IRR L)))) by A6; ::_thesis: verum
end;
 dom r = the carrier of L by PARTFUN1:def_2;
then reconsider r = r as Function of L,(InclPoset (LOWER (subrelstr (Join-IRR L)))) by A2, FUNCT_2:def_1, RELSET_1:4;
A12: for x, y being Element of L holds
( x <= y iff r . x <= r . y )
proof
let x, y be Element of L; ::_thesis: ( x <= y iff r . x <= r . y )
thus  ( x <= y implies r . x <= r . y ) ::_thesis: ( r . x <= r . y implies x <= y )
proof
assume A13: x <= y ; ::_thesis: r . x <= r . y
 (downarrow x) /\ (Join-IRR L) c= (downarrow y) /\ (Join-IRR L)
proof
let a be Element of L; :: according to LATTICE7:def_1 ::_thesis: ( a in (downarrow x) /\ (Join-IRR L) implies a in (downarrow y) /\ (Join-IRR L) )
assume  a in (downarrow x) /\ (Join-IRR L) ; ::_thesis: a in (downarrow y) /\ (Join-IRR L)
then A14: ( a in downarrow x & a in Join-IRR L ) by XBOOLE_0:def_4;
 downarrow x c= downarrow y by A13, WAYBEL_0:21;
hence  a in (downarrow y) /\ (Join-IRR L) by A14, XBOOLE_0:def_4; ::_thesis: verum
end;
then  r . x c= (downarrow y) /\ (Join-IRR L) by A1;
then  r . x c= r . y by A1;
hence  r . x <= r . y by YELLOW_1:3; ::_thesis: verum
end;
thus  ( r . x <= r . y implies x <= y ) ::_thesis: verum
proof
 ( r . x = (downarrow x) /\ (Join-IRR L) & r . y = (downarrow y) /\ (Join-IRR L) ) by A1;
then reconsider rx = r . x, ry = r . y as Subset of L ;
assume  r . x <= r . y ; ::_thesis: x <= y
then A15: rx c= ry by YELLOW_1:3;
 ( ex_sup_of rx,L & ex_sup_of ry,L ) by YELLOW_0:17;
then  sup rx <= sup ry by A15, YELLOW_0:34;
then  sup ((downarrow x) /\ (Join-IRR L)) <= sup ry by A1;
then  sup ((downarrow x) /\ (Join-IRR L)) <= sup ((downarrow y) /\ (Join-IRR L)) by A1;
then  x <= sup ((downarrow y) /\ (Join-IRR L)) by Th12;
hence  x <= y by Th12; ::_thesis: verum
end;
end;
 the carrier of (InclPoset (LOWER (subrelstr (Join-IRR L)))) c= rng r
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in the carrier of (InclPoset (LOWER (subrelstr (Join-IRR L)))) or x in rng r )
assume A16: x in the carrier of (InclPoset (LOWER (subrelstr (Join-IRR L)))) ; ::_thesis: x in rng r
thus  x in rng r ::_thesis: verum
proof
 x in LOWER (subrelstr (Join-IRR L)) by A16, YELLOW_1:1;
then consider X being Subset of (subrelstr (Join-IRR L)) such that
A17: x = X and
A18: X is lower ;
 the carrier of (subrelstr (Join-IRR L)) c= Join-IRR L by YELLOW_0:def_15;
then  the carrier of (subrelstr (Join-IRR L)) c= the carrier of L by XBOOLE_1:1;
then reconsider X1 = X as Subset of L by XBOOLE_1:1;
 ex y being set st
( y in dom r & x = r . y )
proof
take y = sup X1; ::_thesis: ( y in dom r & x = r . y )
 dom r = the carrier of L by FUNCT_2:def_1;
hence  y in dom r ; ::_thesis: x = r . y
A19: (downarrow (sup X1)) /\ (Join-IRR L) c= X1
proof
let r be Element of L; :: according to LATTICE7:def_1 ::_thesis: ( r in (downarrow (sup X1)) /\ (Join-IRR L) implies r in X1 )
reconsider r1 = r as Element of L ;
assume A20: r in (downarrow (sup X1)) /\ (Join-IRR L) ; ::_thesis: r in X1
then  r in downarrow (sup X1) by XBOOLE_0:def_4;
then A21: r1 <= sup X1 by WAYBEL_0:17;
percases ( r1 in X1 or not r1 in X1 ) ;
suppose r1 in X1 ; ::_thesis: r in X1
hence  r in X1 ; ::_thesis: verum
end;
supposeA22: not r1 in X1 ; ::_thesis: r in X1
A23: r1 in Join-IRR L by A20, XBOOLE_0:def_4;
then consider z being Element of L such that
A24: z < r1 and
A25: for y being Element of L st y < r1 holds
y <= z by Th11;
 {r1} "/\" X1 is_<=_than z
proof
let a be Element of L; :: according to LATTICE3:def_9 ::_thesis: ( not a in {r1} "/\" X1 or a <= z )
A26: r1 in the carrier of (subrelstr (Join-IRR L)) by A23, YELLOW_0:def_15;
assume  a in {r1} "/\" X1 ; ::_thesis: a <= z
then  a in  {  (r1 "/\" k) where k is Element of L : k in X1  }  by YELLOW_4:42;
then consider x being Element of L such that
A27: a = r1 "/\" x and
A28: x in X1 ;
reconsider r9 = r1, x9 = x as Element of (subrelstr (Join-IRR L)) by A23, A28, YELLOW_0:def_15;
A29: ex_inf_of {r1,x},L by YELLOW_0:17;
then A30: a <= x by A27, YELLOW_0:19;
A31: now__::_thesis:_not_a_=_r1
assume  a = r1 ; ::_thesis: contradiction
then  r9 <= x9 by A30, A26, YELLOW_0:60;
hence  contradiction by A18, A22, A28, WAYBEL_0:def_19; ::_thesis: verum
end;
 a <= r1 by A27, A29, YELLOW_0:19;
then  a < r1 by A31, ORDERS_2:def_6;
hence  a <= z by A25; ::_thesis: verum
end;
then A32: sup ({r1} "/\" X1) <= z by YELLOW_0:32;
 ( r1 = r1 "/\" (sup X1) & r1 "/\" (sup X1) = sup ({r1} "/\" X1) ) by A21, WAYBEL_2:15, YELLOW_0:25;
hence  r in X1 by A24, A32, ORDERS_2:7; ::_thesis: verum
end;
end;
end;
 X1 c= (downarrow (sup X1)) /\ (Join-IRR L)
proof
let a be Element of L; :: according to LATTICE7:def_1 ::_thesis: ( a in X1 implies a in (downarrow (sup X1)) /\ (Join-IRR L) )
assume A33: a in X1 ; ::_thesis: a in (downarrow (sup X1)) /\ (Join-IRR L)
set A = a;
 ex_sup_of X1,L by YELLOW_0:17;
then A34: X1 is_<=_than "\/" (X1,L) by YELLOW_0:def_9;
 ex y being Element of L st
( y in {(sup X1)} & a <= y )
proof
take y = sup X1; ::_thesis: ( y in {(sup X1)} & a <= y )
thus  y in {(sup X1)} by TARSKI:def_1; ::_thesis: a <= y
thus  a <= y by A33, A34, LATTICE3:def_9; ::_thesis: verum
end;
then A35: a in downarrow {(sup X1)} by WAYBEL_0:def_15;
 X is Subset of (Join-IRR L) by YELLOW_0:def_15;
hence  a in (downarrow (sup X1)) /\ (Join-IRR L) by A33, A35, XBOOLE_0:def_4; ::_thesis: verum
end;
then  X1 = (downarrow (sup X1)) /\ (Join-IRR L) by A19, XBOOLE_0:def_10;
hence  x = r . y by A1, A17; ::_thesis: verum
end;
hence  x in rng r by FUNCT_1:def_3; ::_thesis: verum
end;
end;
then A36: rng r = the carrier of (InclPoset (LOWER (subrelstr (Join-IRR L)))) by XBOOLE_0:def_10;
 r is V13()
proof
let x, y be Element of L; :: according to WAYBEL_1:def_1 ::_thesis: ( not r . x = r . y or x = y )
 r . y = (downarrow y) /\ (Join-IRR L) by A1;
then reconsider ry = r . y as Subset of L ;
assume  r . x = r . y ; ::_thesis: x = y
then  sup ((downarrow x) /\ (Join-IRR L)) = sup ry by A1;
then  sup ((downarrow x) /\ (Join-IRR L)) = sup ((downarrow y) /\ (Join-IRR L)) by A1;
then  x = sup ((downarrow y) /\ (Join-IRR L)) by Th12;
hence  x = y by Th12; ::_thesis: verum
end;
then  r is isomorphic by A36, A12, WAYBEL_0:66;
hence  ex r being Function of L,(InclPoset (LOWER (subrelstr (Join-IRR L)))) st
( r is isomorphic & ( for a being Element of L holds r . a = (downarrow a) /\ (Join-IRR L) ) ) by A1; ::_thesis: verum
end;

theorem Th14: :: LATTICE7:14
for L being finite distributive LATTICE holds L, InclPoset (LOWER (subrelstr (Join-IRR L))) are_isomorphic
proof
let L be finite distributive LATTICE; ::_thesis: L, InclPoset (LOWER (subrelstr (Join-IRR L))) are_isomorphic
 ex r being Function of L,(InclPoset (LOWER (subrelstr (Join-IRR L)))) st
( r is isomorphic & ( for a being Element of L holds r . a = (downarrow a) /\ (Join-IRR L) ) ) by Th13;
hence  L, InclPoset (LOWER (subrelstr (Join-IRR L))) are_isomorphic by WAYBEL_1:def_8; ::_thesis: verum
end;

definition
mode Ring_of_sets  ->  set  means :Def8: :: LATTICE7:def 8
it includes_lattice_of it;
existence
 ex b1 being set st b1 includes_lattice_of b1
proof
set X = the set ;
take R = bool the set ; ::_thesis: R includes_lattice_of R
let a, b be set ; :: according to COHSP_1:def_7 ::_thesis: ( not a in R or not b in R or ( a /\ b in R & a \/ b in R ) )
assume that
A1: a in R and
A2: b in R ; ::_thesis: ( a /\ b in R & a \/ b in R )
 a /\ b c= the set by A1, XBOOLE_1:108;
hence  a /\ b in R ; ::_thesis: a \/ b in R
 a \/ b c= the set by A1, A2, XBOOLE_1:8;
hence  a \/ b in R ; ::_thesis: verum
end;
end;

:: deftheorem Def8 defines Ring_of_sets LATTICE7:def_8_:_
 for b1 being set holds
( b1 is Ring_of_sets iff b1 includes_lattice_of b1 );

registration
cluster non empty for Ring_of_sets ;
existence
 not for b1 being Ring_of_sets holds b1 is empty
proof
take A = {{}}; ::_thesis: ( A is Ring_of_sets & not A is empty )
 A includes_lattice_of A
proof
let a, b be set ; :: according to COHSP_1:def_7 ::_thesis: ( not a in A or not b in A or ( a /\ b in A & a \/ b in A ) )
assume that
A1: a in A and
A2: b in A ; ::_thesis: ( a /\ b in A & a \/ b in A )
 a = {} by A1, TARSKI:def_1;
hence  ( a /\ b in A & a \/ b in A ) by A2, TARSKI:def_1; ::_thesis: verum
end;
hence  ( A is Ring_of_sets & not A is empty ) by Def8; ::_thesis: verum
end;
end;

Lm2:  for L1, L2 being non empty RelStr
for f being Function of L1,L2 st f is infs-preserving holds
f is meet-preserving
proof
let L1, L2 be non empty RelStr ; ::_thesis: for f being Function of L1,L2 st f is infs-preserving holds
f is meet-preserving
let f be Function of L1,L2; ::_thesis: ( f is infs-preserving implies f is meet-preserving )
assume  f is infs-preserving ; ::_thesis: f is meet-preserving
then  for x, y being Element of L1 holds f preserves_inf_of {x,y} by WAYBEL_0:def_32;
hence  f is meet-preserving by WAYBEL_0:def_34; ::_thesis: verum
end;

Lm3:  for L1, L2 being non empty RelStr
for f being Function of L1,L2 st f is sups-preserving holds
f is join-preserving
proof
let L1, L2 be non empty RelStr ; ::_thesis: for f being Function of L1,L2 st f is sups-preserving holds
f is join-preserving
let f be Function of L1,L2; ::_thesis: ( f is sups-preserving implies f is join-preserving )
assume  f is sups-preserving ; ::_thesis: f is join-preserving
then  for x, y being Element of L1 holds f preserves_sup_of {x,y} by WAYBEL_0:def_33;
hence  f is join-preserving by WAYBEL_0:def_35; ::_thesis: verum
end;

registration
let X be non empty Ring_of_sets ;
cluster InclPoset X ->  distributive with_suprema with_infima ;
coherence
 ( InclPoset X is with_suprema & InclPoset X is with_infima & InclPoset X is distributive )
proof
A1: X includes_lattice_of X by Def8;
A2: InclPoset X is distributive
proof
let x, y, z be Element of (InclPoset X); :: according to WAYBEL_1:def_3 ::_thesis: x "/\" (y "\/" z) = (x "/\" y) "\/" (x "/\" z)
 x in the carrier of (InclPoset X) ;
then A3: x in X by YELLOW_1:1;
 z in the carrier of (InclPoset X) ;
then A4: z in X by YELLOW_1:1;
then A5: x /\ z in X by A1, A3, COHSP_1:def_7;
then A6: x "/\" z = x /\ z by YELLOW_1:9;
 y in the carrier of (InclPoset X) ;
then A7: y in X by YELLOW_1:1;
then A8: y \/ z in X by A1, A4, COHSP_1:def_7;
then reconsider r = y \/ z as Element of (InclPoset X) by YELLOW_1:1;
A9: x /\ y in X by A1, A3, A7, COHSP_1:def_7;
then reconsider r1 = x /\ y, r2 = x /\ z as Element of (InclPoset X) by A5, YELLOW_1:1;
 r1 in the carrier of (InclPoset X) ;
then A10: r1 in X by YELLOW_1:1;
 r in the carrier of (InclPoset X) ;
then  r in X by YELLOW_1:1;
then  x /\ r in X by A1, A3, COHSP_1:def_7;
then  x "/\" r = x /\ r by YELLOW_1:9;
then A11: ( x /\ (y \/ z) = (x /\ y) \/ (x /\ z) & x /\ (y \/ z) = x "/\" (y "\/" z) ) by A8, XBOOLE_1:23, YELLOW_1:8;
 r2 in the carrier of (InclPoset X) ;
then  r2 in X by YELLOW_1:1;
then A12: r1 \/ r2 in X by A1, A10, COHSP_1:def_7;
 x "/\" y = x /\ y by A9, YELLOW_1:9;
hence  x "/\" (y "\/" z) = (x "/\" y) "\/" (x "/\" z) by A11, A6, A12, YELLOW_1:8; ::_thesis: verum
end;
 ( ( for x, y being set st x in X & y in X holds
x /\ y in X ) & ( for x, y being set st x in X & y in X holds
x \/ y in X ) ) by A1, COHSP_1:def_7;
hence  ( InclPoset X is with_suprema & InclPoset X is with_infima & InclPoset X is distributive ) by A2, YELLOW_1:11, YELLOW_1:12; ::_thesis: verum
end;
end;

theorem Th15: :: LATTICE7:15
for L being finite LATTICE holds LOWER (subrelstr (Join-IRR L)) is Ring_of_sets
proof
let L be finite LATTICE; ::_thesis: LOWER (subrelstr (Join-IRR L)) is Ring_of_sets
set X = LOWER (subrelstr (Join-IRR L));
 LOWER (subrelstr (Join-IRR L)) includes_lattice_of LOWER (subrelstr (Join-IRR L))
proof
let a, b be set ; :: according to COHSP_1:def_7 ::_thesis: ( not a in LOWER (subrelstr (Join-IRR L)) or not b in LOWER (subrelstr (Join-IRR L)) or ( a /\ b in LOWER (subrelstr (Join-IRR L)) & a \/ b in LOWER (subrelstr (Join-IRR L)) ) )
assume that
A1: a in LOWER (subrelstr (Join-IRR L)) and
A2: b in LOWER (subrelstr (Join-IRR L)) ; ::_thesis: ( a /\ b in LOWER (subrelstr (Join-IRR L)) & a \/ b in LOWER (subrelstr (Join-IRR L)) )
A3: a \/ b in LOWER (subrelstr (Join-IRR L))
proof
consider Z1 being Subset of (subrelstr (Join-IRR L)) such that
A4: b = Z1 and
A5: Z1 is lower by A2;
consider Z being Subset of (subrelstr (Join-IRR L)) such that
A6: a = Z and
A7: Z is lower by A1;
 Z \/ Z1 is lower by A7, A5, WAYBEL_0:27;
hence  a \/ b in LOWER (subrelstr (Join-IRR L)) by A6, A4; ::_thesis: verum
end;
 a /\ b in LOWER (subrelstr (Join-IRR L))
proof
consider Z1 being Subset of (subrelstr (Join-IRR L)) such that
A8: b = Z1 and
A9: Z1 is lower by A2;
consider Z being Subset of (subrelstr (Join-IRR L)) such that
A10: a = Z and
A11: Z is lower by A1;
 Z /\ Z1 is lower by A11, A9, WAYBEL_0:27;
hence  a /\ b in LOWER (subrelstr (Join-IRR L)) by A10, A8; ::_thesis: verum
end;
hence  ( a /\ b in LOWER (subrelstr (Join-IRR L)) & a \/ b in LOWER (subrelstr (Join-IRR L)) ) by A3; ::_thesis: verum
end;
hence  LOWER (subrelstr (Join-IRR L)) is Ring_of_sets by Def8; ::_thesis: verum
end;

theorem :: LATTICE7:16
for L being finite LATTICE holds
( L is distributive iff ex X being non empty Ring_of_sets st L, InclPoset X are_isomorphic )
proof
let L be finite LATTICE; ::_thesis: ( L is distributive iff ex X being non empty Ring_of_sets st L, InclPoset X are_isomorphic )
thus  ( L is distributive implies ex X being non empty Ring_of_sets st L, InclPoset X are_isomorphic ) ::_thesis: ( ex X being non empty Ring_of_sets st L, InclPoset X are_isomorphic implies L is distributive )
proof
consider X being set  such that
A1: X = LOWER (subrelstr (Join-IRR L)) ;
A2: X is Ring_of_sets by A1, Th15;
assume  L is distributive ; ::_thesis: ex X being non empty Ring_of_sets st L, InclPoset X are_isomorphic
then  L, InclPoset X are_isomorphic by A1, Th14;
hence  ex X being non empty Ring_of_sets st L, InclPoset X are_isomorphic by A1, A2; ::_thesis: verum
end;
given X being non empty Ring_of_sets  such that A3: L, InclPoset X are_isomorphic ; ::_thesis: L is distributive
consider f being Function of L,(InclPoset X) such that
A4: f is isomorphic by A3, WAYBEL_1:def_8;
A5: f is V13() by A4, WAYBEL_0:66;
 ( f is infs-preserving & f is join-preserving ) by A4, Lm3, WAYBEL13:20;
hence  L is distributive by A5, Lm2, WAYBEL_6:3; ::_thesis: verum
end;