:: by Grzegorz Bancerek

::

:: Received May 13, 1992

:: Copyright (c) 1992-2016 Association of Mizar Users

deffunc H

deffunc H

deffunc H

definition

let X be set ;

ex b_{1} being strict LattStr st

( the carrier of b_{1} = bool X & ( for Y, Z being Subset of X holds

( the L_join of b_{1} . (Y,Z) = Y \/ Z & the L_meet of b_{1} . (Y,Z) = Y /\ Z ) ) )

for b_{1}, b_{2} being strict LattStr st the carrier of b_{1} = bool X & ( for Y, Z being Subset of X holds

( the L_join of b_{1} . (Y,Z) = Y \/ Z & the L_meet of b_{1} . (Y,Z) = Y /\ Z ) ) & the carrier of b_{2} = bool X & ( for Y, Z being Subset of X holds

( the L_join of b_{2} . (Y,Z) = Y \/ Z & the L_meet of b_{2} . (Y,Z) = Y /\ Z ) ) holds

b_{1} = b_{2}

end;
func BooleLatt X -> strict LattStr means :Def1: :: LATTICE3:def 1

( the carrier of it = bool X & ( for Y, Z being Subset of X holds

( the L_join of it . (Y,Z) = Y \/ Z & the L_meet of it . (Y,Z) = Y /\ Z ) ) );

existence ( the carrier of it = bool X & ( for Y, Z being Subset of X holds

( the L_join of it . (Y,Z) = Y \/ Z & the L_meet of it . (Y,Z) = Y /\ Z ) ) );

ex b

( the carrier of b

( the L_join of b

proof end;

uniqueness for b

( the L_join of b

( the L_join of b

b

proof end;

:: deftheorem Def1 defines BooleLatt LATTICE3:def 1 :

for X being set

for b_{2} being strict LattStr holds

( b_{2} = BooleLatt X iff ( the carrier of b_{2} = bool X & ( for Y, Z being Subset of X holds

( the L_join of b_{2} . (Y,Z) = Y \/ Z & the L_meet of b_{2} . (Y,Z) = Y /\ Z ) ) ) );

for X being set

for b

( b

( the L_join of b

registration

let X be set ;

let x, y be Element of (BooleLatt X);

let x9, y9 be set ;

compatibility

( x = x9 & y = y9 implies x "\/" y = x9 \/ y9 )

( x = x9 & y = y9 implies x "/\" y = x9 /\ y9 )

end;
let x, y be Element of (BooleLatt X);

let x9, y9 be set ;

compatibility

( x = x9 & y = y9 implies x "\/" y = x9 \/ y9 )

proof end;

compatibility ( x = x9 & y = y9 implies x "/\" y = x9 /\ y9 )

proof end;

theorem Th2: :: LATTICE3:2

for X being set

for x, y being Element of (BooleLatt X) holds

( x [= y iff x c= y ) by XBOOLE_1:7, XBOOLE_1:12;

for x, y being Element of (BooleLatt X) holds

( x [= y iff x c= y ) by XBOOLE_1:7, XBOOLE_1:12;

registration
end;

definition

let L be Lattice;

:: original: LattRel

redefine func LattRel L -> Order of the carrier of L;

coherence

LattRel L is Order of the carrier of L

end;
:: original: LattRel

redefine func LattRel L -> Order of the carrier of L;

coherence

LattRel L is Order of the carrier of L

proof end;

definition
end;

:: deftheorem defines LattPOSet LATTICE3:def 2 :

for L being Lattice holds LattPOSet L = RelStr(# the carrier of L,(LattRel L) #);

for L being Lattice holds LattPOSet L = RelStr(# the carrier of L,(LattRel L) #);

registration
end;

theorem Th6: :: LATTICE3:6

for L1, L2 being Lattice st LattPOSet L1 = LattPOSet L2 holds

LattStr(# the carrier of L1, the L_join of L1, the L_meet of L1 #) = LattStr(# the carrier of L2, the L_join of L2, the L_meet of L2 #)

LattStr(# the carrier of L1, the L_join of L1, the L_meet of L1 #) = LattStr(# the carrier of L2, the L_join of L2, the L_meet of L2 #)

proof end;

definition
end;

:: deftheorem defines % LATTICE3:def 3 :

for L being Lattice

for p being Element of L holds p % = p;

for L being Lattice

for p being Element of L holds p % = p;

definition
end;

:: deftheorem defines % LATTICE3:def 4 :

for L being Lattice

for p being Element of (LattPOSet L) holds % p = p;

for L being Lattice

for p being Element of (LattPOSet L) holds % p = p;

definition

let X be set ;

let O be Order of X;

:: original: ~

redefine func O ~ -> Order of X;

coherence

O ~ is Order of X

end;
let O be Order of X;

:: original: ~

redefine func O ~ -> Order of X;

coherence

O ~ is Order of X

proof end;

definition

let A be RelStr ;

coherence

RelStr(# the carrier of A,( the InternalRel of A ~) #) is strict RelStr ;

;

end;
func A ~ -> strict RelStr equals :: LATTICE3:def 5

RelStr(# the carrier of A,( the InternalRel of A ~) #);

correctness RelStr(# the carrier of A,( the InternalRel of A ~) #);

coherence

RelStr(# the carrier of A,( the InternalRel of A ~) #) is strict RelStr ;

;

:: deftheorem defines ~ LATTICE3:def 5 :

for A being RelStr holds A ~ = RelStr(# the carrier of A,( the InternalRel of A ~) #);

for A being RelStr holds A ~ = RelStr(# the carrier of A,( the InternalRel of A ~) #);

registration

let A be Poset;

coherence

( A ~ is reflexive & A ~ is transitive & A ~ is antisymmetric )

end;
coherence

( A ~ is reflexive & A ~ is transitive & A ~ is antisymmetric )

proof end;

registration
end;

theorem :: LATTICE3:8

definition
end;

definition
end;

:: deftheorem defines ~ LATTICE3:def 7 :

for A being RelStr

for a being Element of (A ~) holds ~ a = a;

for A being RelStr

for a being Element of (A ~) holds ~ a = a;

:: deftheorem defines is_<=_than LATTICE3:def 8 :

for A being RelStr

for X being set

for a being Element of A holds

( a is_<=_than X iff for b being Element of A st b in X holds

a <= b );

for A being RelStr

for X being set

for a being Element of A holds

( a is_<=_than X iff for b being Element of A st b in X holds

a <= b );

:: deftheorem defines is_<=_than LATTICE3:def 9 :

for A being RelStr

for X being set

for a being Element of A holds

( X is_<=_than a iff for b being Element of A st b in X holds

b <= a );

for A being RelStr

for X being set

for a being Element of A holds

( X is_<=_than a iff for b being Element of A st b in X holds

b <= a );

notation

let A be RelStr ;

let X be set ;

let a be Element of A;

synonym X is_>=_than a for a is_<=_than X;

synonym a is_>=_than X for X is_<=_than a;

end;
let X be set ;

let a be Element of A;

synonym X is_>=_than a for a is_<=_than X;

synonym a is_>=_than X for X is_<=_than a;

definition

let IT be RelStr ;

end;
:: deftheorem Def10 defines with_suprema LATTICE3:def 10 :

for IT being RelStr holds

( IT is with_suprema iff for x, y being Element of IT ex z being Element of IT st

( x <= z & y <= z & ( for z9 being Element of IT st x <= z9 & y <= z9 holds

z <= z9 ) ) );

for IT being RelStr holds

( IT is with_suprema iff for x, y being Element of IT ex z being Element of IT st

( x <= z & y <= z & ( for z9 being Element of IT st x <= z9 & y <= z9 holds

z <= z9 ) ) );

:: deftheorem Def11 defines with_infima LATTICE3:def 11 :

for IT being RelStr holds

( IT is with_infima iff for x, y being Element of IT ex z being Element of IT st

( z <= x & z <= y & ( for z9 being Element of IT st z9 <= x & z9 <= y holds

z9 <= z ) ) );

for IT being RelStr holds

( IT is with_infima iff for x, y being Element of IT ex z being Element of IT st

( z <= x & z <= y & ( for z9 being Element of IT st z9 <= x & z9 <= y holds

z9 <= z ) ) );

registration

coherence

for b_{1} being RelStr st b_{1} is with_suprema holds

not b_{1} is empty

for b_{1} being RelStr st b_{1} is with_infima holds

not b_{1} is empty

end;
for b

not b

proof end;

coherence for b

not b

proof end;

definition

let IT be RelStr ;

end;
attr IT is complete means :Def12: :: LATTICE3:def 12

for X being set ex a being Element of IT st

( X is_<=_than a & ( for b being Element of IT st X is_<=_than b holds

a <= b ) );

for X being set ex a being Element of IT st

( X is_<=_than a & ( for b being Element of IT st X is_<=_than b holds

a <= b ) );

:: deftheorem Def12 defines complete LATTICE3:def 12 :

for IT being RelStr holds

( IT is complete iff for X being set ex a being Element of IT st

( X is_<=_than a & ( for b being Element of IT st X is_<=_than b holds

a <= b ) ) );

for IT being RelStr holds

( IT is complete iff for X being set ex a being Element of IT st

( X is_<=_than a & ( for b being Element of IT st X is_<=_than b holds

a <= b ) ) );

registration

existence

ex b_{1} being Poset st

( b_{1} is strict & b_{1} is complete & not b_{1} is empty )

end;
ex b

( b

proof end;

registration

ex b_{1} being Poset st

( b_{1} is complete & b_{1} is with_suprema & b_{1} is with_infima & b_{1} is strict & not b_{1} is empty )
end;

cluster non empty strict V69() reflexive transitive antisymmetric with_suprema with_infima complete for RelStr ;

existence ex b

( b

proof end;

definition

let A be RelStr ;

assume A1: A is antisymmetric ;

let a, b be Element of A;

assume A2: ex x being Element of A st

( a <= x & b <= x & ( for c being Element of A st a <= c & b <= c holds

x <= c ) ) ;

ex b_{1} being Element of A st

( a <= b_{1} & b <= b_{1} & ( for c being Element of A st a <= c & b <= c holds

b_{1} <= c ) )
by A2;

uniqueness

for b_{1}, b_{2} being Element of A st a <= b_{1} & b <= b_{1} & ( for c being Element of A st a <= c & b <= c holds

b_{1} <= c ) & a <= b_{2} & b <= b_{2} & ( for c being Element of A st a <= c & b <= c holds

b_{2} <= c ) holds

b_{1} = b_{2}

end;
assume A1: A is antisymmetric ;

let a, b be Element of A;

assume A2: ex x being Element of A st

( a <= x & b <= x & ( for c being Element of A st a <= c & b <= c holds

x <= c ) ) ;

func a "\/" b -> Element of A means :Def13: :: LATTICE3:def 13

( a <= it & b <= it & ( for c being Element of A st a <= c & b <= c holds

it <= c ) );

existence ( a <= it & b <= it & ( for c being Element of A st a <= c & b <= c holds

it <= c ) );

ex b

( a <= b

b

uniqueness

for b

b

b

b

proof end;

:: deftheorem Def13 defines "\/" LATTICE3:def 13 :

for A being RelStr st A is antisymmetric holds

for a, b being Element of A st ex x being Element of A st

( a <= x & b <= x & ( for c being Element of A st a <= c & b <= c holds

x <= c ) ) holds

for b_{4} being Element of A holds

( b_{4} = a "\/" b iff ( a <= b_{4} & b <= b_{4} & ( for c being Element of A st a <= c & b <= c holds

b_{4} <= c ) ) );

for A being RelStr st A is antisymmetric holds

for a, b being Element of A st ex x being Element of A st

( a <= x & b <= x & ( for c being Element of A st a <= c & b <= c holds

x <= c ) ) holds

for b

( b

b

Lm1: now :: thesis: for A being non empty antisymmetric with_suprema RelStr

for a, b, c being Element of A holds

( c = a "\/" b iff ( a <= c & b <= c & ( for d being Element of A st a <= d & b <= d holds

c <= d ) ) )

for a, b, c being Element of A holds

( c = a "\/" b iff ( a <= c & b <= c & ( for d being Element of A st a <= d & b <= d holds

c <= d ) ) )

let A be non empty antisymmetric with_suprema RelStr ; :: thesis: for a, b, c being Element of A holds

( c = a "\/" b iff ( a <= c & b <= c & ( for d being Element of A st a <= d & b <= d holds

c <= d ) ) )

let a, b be Element of A; :: thesis: for c being Element of A holds

( c = a "\/" b iff ( a <= c & b <= c & ( for d being Element of A st a <= d & b <= d holds

c <= d ) ) )

ex x being Element of A st

( a <= x & b <= x & ( for c being Element of A st a <= c & b <= c holds

x <= c ) ) by Def10;

hence for c being Element of A holds

( c = a "\/" b iff ( a <= c & b <= c & ( for d being Element of A st a <= d & b <= d holds

c <= d ) ) ) by Def13; :: thesis: verum

end;
( c = a "\/" b iff ( a <= c & b <= c & ( for d being Element of A st a <= d & b <= d holds

c <= d ) ) )

let a, b be Element of A; :: thesis: for c being Element of A holds

( c = a "\/" b iff ( a <= c & b <= c & ( for d being Element of A st a <= d & b <= d holds

c <= d ) ) )

ex x being Element of A st

( a <= x & b <= x & ( for c being Element of A st a <= c & b <= c holds

x <= c ) ) by Def10;

hence for c being Element of A holds

( c = a "\/" b iff ( a <= c & b <= c & ( for d being Element of A st a <= d & b <= d holds

c <= d ) ) ) by Def13; :: thesis: verum

definition

let A be RelStr ;

assume A1: A is antisymmetric ;

let a, b be Element of A;

assume A2: ex x being Element of A st

( a >= x & b >= x & ( for c being Element of A st a >= c & b >= c holds

x >= c ) ) ;

ex b_{1} being Element of A st

( b_{1} <= a & b_{1} <= b & ( for c being Element of A st c <= a & c <= b holds

c <= b_{1} ) )
by A2;

uniqueness

for b_{1}, b_{2} being Element of A st b_{1} <= a & b_{1} <= b & ( for c being Element of A st c <= a & c <= b holds

c <= b_{1} ) & b_{2} <= a & b_{2} <= b & ( for c being Element of A st c <= a & c <= b holds

c <= b_{2} ) holds

b_{1} = b_{2}

end;
assume A1: A is antisymmetric ;

let a, b be Element of A;

assume A2: ex x being Element of A st

( a >= x & b >= x & ( for c being Element of A st a >= c & b >= c holds

x >= c ) ) ;

func a "/\" b -> Element of A means :Def14: :: LATTICE3:def 14

( it <= a & it <= b & ( for c being Element of A st c <= a & c <= b holds

c <= it ) );

existence ( it <= a & it <= b & ( for c being Element of A st c <= a & c <= b holds

c <= it ) );

ex b

( b

c <= b

uniqueness

for b

c <= b

c <= b

b

proof end;

:: deftheorem Def14 defines "/\" LATTICE3:def 14 :

for A being RelStr st A is antisymmetric holds

for a, b being Element of A st ex x being Element of A st

( a >= x & b >= x & ( for c being Element of A st a >= c & b >= c holds

x >= c ) ) holds

for b_{4} being Element of A holds

( b_{4} = a "/\" b iff ( b_{4} <= a & b_{4} <= b & ( for c being Element of A st c <= a & c <= b holds

c <= b_{4} ) ) );

for A being RelStr st A is antisymmetric holds

for a, b being Element of A st ex x being Element of A st

( a >= x & b >= x & ( for c being Element of A st a >= c & b >= c holds

x >= c ) ) holds

for b

( b

c <= b

Lm2: now :: thesis: for A being non empty antisymmetric with_infima RelStr

for a, b, c being Element of A holds

( c = a "/\" b iff ( a >= c & b >= c & ( for d being Element of A st a >= d & b >= d holds

c >= d ) ) )

for a, b, c being Element of A holds

( c = a "/\" b iff ( a >= c & b >= c & ( for d being Element of A st a >= d & b >= d holds

c >= d ) ) )

let A be non empty antisymmetric with_infima RelStr ; :: thesis: for a, b, c being Element of A holds

( c = a "/\" b iff ( a >= c & b >= c & ( for d being Element of A st a >= d & b >= d holds

c >= d ) ) )

let a, b be Element of A; :: thesis: for c being Element of A holds

( c = a "/\" b iff ( a >= c & b >= c & ( for d being Element of A st a >= d & b >= d holds

c >= d ) ) )

ex x being Element of A st

( a >= x & b >= x & ( for c being Element of A st a >= c & b >= c holds

x >= c ) ) by Def11;

hence for c being Element of A holds

( c = a "/\" b iff ( a >= c & b >= c & ( for d being Element of A st a >= d & b >= d holds

c >= d ) ) ) by Def14; :: thesis: verum

end;
( c = a "/\" b iff ( a >= c & b >= c & ( for d being Element of A st a >= d & b >= d holds

c >= d ) ) )

let a, b be Element of A; :: thesis: for c being Element of A holds

( c = a "/\" b iff ( a >= c & b >= c & ( for d being Element of A st a >= d & b >= d holds

c >= d ) ) )

ex x being Element of A st

( a >= x & b >= x & ( for c being Element of A st a >= c & b >= c holds

x >= c ) ) by Def11;

hence for c being Element of A holds

( c = a "/\" b iff ( a >= c & b >= c & ( for d being Element of A st a >= d & b >= d holds

c >= d ) ) ) by Def14; :: thesis: verum

theorem Th13: :: LATTICE3:13

for V being antisymmetric with_suprema RelStr

for u1, u2 being Element of V holds u1 "\/" u2 = u2 "\/" u1

for u1, u2 being Element of V holds u1 "\/" u2 = u2 "\/" u1

proof end;

theorem Th14: :: LATTICE3:14

for V being antisymmetric with_suprema RelStr

for u1, u2, u3 being Element of V st V is transitive holds

(u1 "\/" u2) "\/" u3 = u1 "\/" (u2 "\/" u3)

for u1, u2, u3 being Element of V st V is transitive holds

(u1 "\/" u2) "\/" u3 = u1 "\/" (u2 "\/" u3)

proof end;

theorem Th15: :: LATTICE3:15

for N being antisymmetric with_infima RelStr

for n1, n2 being Element of N holds n1 "/\" n2 = n2 "/\" n1

for n1, n2 being Element of N holds n1 "/\" n2 = n2 "/\" n1

proof end;

theorem Th16: :: LATTICE3:16

for N being antisymmetric with_infima RelStr

for n1, n2, n3 being Element of N st N is transitive holds

(n1 "/\" n2) "/\" n3 = n1 "/\" (n2 "/\" n3)

for n1, n2, n3 being Element of N st N is transitive holds

(n1 "/\" n2) "/\" n3 = n1 "/\" (n2 "/\" n3)

proof end;

definition

let L be antisymmetric with_infima RelStr ;

let x, y be Element of L;

:: original: "/\"

redefine func x "/\" y -> Element of L;

commutativity

for x, y being Element of L holds x "/\" y = y "/\" x by Th15;

end;
let x, y be Element of L;

:: original: "/\"

redefine func x "/\" y -> Element of L;

commutativity

for x, y being Element of L holds x "/\" y = y "/\" x by Th15;

definition

let L be antisymmetric with_suprema RelStr ;

let x, y be Element of L;

:: original: "\/"

redefine func x "\/" y -> Element of L;

commutativity

for x, y being Element of L holds x "\/" y = y "\/" x by Th13;

end;
let x, y be Element of L;

:: original: "\/"

redefine func x "\/" y -> Element of L;

commutativity

for x, y being Element of L holds x "\/" y = y "\/" x by Th13;

theorem Th17: :: LATTICE3:17

for K being reflexive antisymmetric with_suprema with_infima RelStr

for k1, k2 being Element of K holds (k1 "/\" k2) "\/" k2 = k2

for k1, k2 being Element of K holds (k1 "/\" k2) "\/" k2 = k2

proof end;

theorem Th18: :: LATTICE3:18

for K being reflexive antisymmetric with_suprema with_infima RelStr

for k1, k2 being Element of K holds k1 "/\" (k1 "\/" k2) = k1

for k1, k2 being Element of K holds k1 "/\" (k1 "\/" k2) = k1

proof end;

theorem Th19: :: LATTICE3:19

for A being with_suprema with_infima Poset ex L being strict Lattice st RelStr(# the carrier of A, the InternalRel of A #) = LattPOSet L

proof end;

definition

let A be RelStr ;

assume A1: A is with_suprema with_infima Poset ;

ex b_{1} being strict Lattice st RelStr(# the carrier of A, the InternalRel of A #) = LattPOSet b_{1}
by A1, Th19;

uniqueness

for b_{1}, b_{2} being strict Lattice st RelStr(# the carrier of A, the InternalRel of A #) = LattPOSet b_{1} & RelStr(# the carrier of A, the InternalRel of A #) = LattPOSet b_{2} holds

b_{1} = b_{2}
by Th6;

end;
assume A1: A is with_suprema with_infima Poset ;

func latt A -> strict Lattice means :Def15: :: LATTICE3:def 15

RelStr(# the carrier of A, the InternalRel of A #) = LattPOSet it;

existence RelStr(# the carrier of A, the InternalRel of A #) = LattPOSet it;

ex b

uniqueness

for b

b

:: deftheorem Def15 defines latt LATTICE3:def 15 :

for A being RelStr st A is with_suprema with_infima Poset holds

for b_{2} being strict Lattice holds

( b_{2} = latt A iff RelStr(# the carrier of A, the InternalRel of A #) = LattPOSet b_{2} );

for A being RelStr st A is with_suprema with_infima Poset holds

for b

( b

:: deftheorem defines is_less_than LATTICE3:def 16 :

for L being non empty LattStr

for p being Element of L

for X being set holds

( p is_less_than X iff for q being Element of L st q in X holds

p [= q );

for L being non empty LattStr

for p being Element of L

for X being set holds

( p is_less_than X iff for q being Element of L st q in X holds

p [= q );

:: deftheorem defines is_less_than LATTICE3:def 17 :

for L being non empty LattStr

for p being Element of L

for X being set holds

( X is_less_than p iff for q being Element of L st q in X holds

q [= p );

for L being non empty LattStr

for p being Element of L

for X being set holds

( X is_less_than p iff for q being Element of L st q in X holds

q [= p );

notation

let L be non empty LattStr ;

let p be Element of L;

let X be set ;

synonym X is_greater_than p for p is_less_than X;

synonym p is_greater_than X for X is_less_than p;

end;
let p be Element of L;

let X be set ;

synonym X is_greater_than p for p is_less_than X;

synonym p is_greater_than X for X is_less_than p;

theorem :: LATTICE3:22

for L being Lattice

for p, q, r being Element of L holds

( p is_greater_than {q,r} iff q "\/" r [= p )

for p, q, r being Element of L holds

( p is_greater_than {q,r} iff q "\/" r [= p )

proof end;

definition

let IT be non empty LattStr ;

end;
attr IT is complete means :Def18: :: LATTICE3:def 18

for X being set ex p being Element of IT st

( X is_less_than p & ( for r being Element of IT st X is_less_than r holds

p [= r ) );

for X being set ex p being Element of IT st

( X is_less_than p & ( for r being Element of IT st X is_less_than r holds

p [= r ) );

attr IT is \/-distributive means :: LATTICE3:def 19

for X being set

for a, b, c being Element of IT st X is_less_than a & ( for d being Element of IT st X is_less_than d holds

a [= d ) & { (b "/\" a9) where a9 is Element of IT : a9 in X } is_less_than c & ( for d being Element of IT st { (b "/\" a9) where a9 is Element of IT : a9 in X } is_less_than d holds

c [= d ) holds

b "/\" a [= c;

for X being set

for a, b, c being Element of IT st X is_less_than a & ( for d being Element of IT st X is_less_than d holds

a [= d ) & { (b "/\" a9) where a9 is Element of IT : a9 in X } is_less_than c & ( for d being Element of IT st { (b "/\" a9) where a9 is Element of IT : a9 in X } is_less_than d holds

c [= d ) holds

b "/\" a [= c;

attr IT is /\-distributive means :: LATTICE3:def 20

for X being set

for a, b, c being Element of IT st X is_greater_than a & ( for d being Element of IT st X is_greater_than d holds

d [= a ) & { (b "\/" a9) where a9 is Element of IT : a9 in X } is_greater_than c & ( for d being Element of IT st { (b "\/" a9) where a9 is Element of IT : a9 in X } is_greater_than d holds

d [= c ) holds

c [= b "\/" a;

for X being set

for a, b, c being Element of IT st X is_greater_than a & ( for d being Element of IT st X is_greater_than d holds

d [= a ) & { (b "\/" a9) where a9 is Element of IT : a9 in X } is_greater_than c & ( for d being Element of IT st { (b "\/" a9) where a9 is Element of IT : a9 in X } is_greater_than d holds

d [= c ) holds

c [= b "\/" a;

:: deftheorem Def18 defines complete LATTICE3:def 18 :

for IT being non empty LattStr holds

( IT is complete iff for X being set ex p being Element of IT st

( X is_less_than p & ( for r being Element of IT st X is_less_than r holds

p [= r ) ) );

for IT being non empty LattStr holds

( IT is complete iff for X being set ex p being Element of IT st

( X is_less_than p & ( for r being Element of IT st X is_less_than r holds

p [= r ) ) );

:: deftheorem defines \/-distributive LATTICE3:def 19 :

for IT being non empty LattStr holds

( IT is \/-distributive iff for X being set

for a, b, c being Element of IT st X is_less_than a & ( for d being Element of IT st X is_less_than d holds

a [= d ) & { (b "/\" a9) where a9 is Element of IT : a9 in X } is_less_than c & ( for d being Element of IT st { (b "/\" a9) where a9 is Element of IT : a9 in X } is_less_than d holds

c [= d ) holds

b "/\" a [= c );

for IT being non empty LattStr holds

( IT is \/-distributive iff for X being set

for a, b, c being Element of IT st X is_less_than a & ( for d being Element of IT st X is_less_than d holds

a [= d ) & { (b "/\" a9) where a9 is Element of IT : a9 in X } is_less_than c & ( for d being Element of IT st { (b "/\" a9) where a9 is Element of IT : a9 in X } is_less_than d holds

c [= d ) holds

b "/\" a [= c );

:: deftheorem defines /\-distributive LATTICE3:def 20 :

for IT being non empty LattStr holds

( IT is /\-distributive iff for X being set

for a, b, c being Element of IT st X is_greater_than a & ( for d being Element of IT st X is_greater_than d holds

d [= a ) & { (b "\/" a9) where a9 is Element of IT : a9 in X } is_greater_than c & ( for d being Element of IT st { (b "\/" a9) where a9 is Element of IT : a9 in X } is_greater_than d holds

d [= c ) holds

c [= b "\/" a );

for IT being non empty LattStr holds

( IT is /\-distributive iff for X being set

for a, b, c being Element of IT st X is_greater_than a & ( for d being Element of IT st X is_greater_than d holds

d [= a ) & { (b "\/" a9) where a9 is Element of IT : a9 in X } is_greater_than c & ( for d being Element of IT st { (b "\/" a9) where a9 is Element of IT : a9 in X } is_greater_than d holds

d [= c ) holds

c [= b "\/" a );

theorem :: LATTICE3:23

for X being set

for B being B_Lattice

for a being Element of B holds

( X is_less_than a iff { (b `) where b is Element of B : b in X } is_greater_than a ` )

for B being B_Lattice

for a being Element of B holds

( X is_less_than a iff { (b `) where b is Element of B : b in X } is_greater_than a ` )

proof end;

theorem Th24: :: LATTICE3:24

for X being set

for B being B_Lattice

for a being Element of B holds

( X is_greater_than a iff { (b `) where b is Element of B : b in X } is_less_than a ` )

for B being B_Lattice

for a being Element of B holds

( X is_greater_than a iff { (b `) where b is Element of B : b in X } is_less_than a ` )

proof end;

registration
end;

registration

ex b_{1} being Lattice st

( b_{1} is complete & b_{1} is \/-distributive & b_{1} is /\-distributive & b_{1} is strict )
end;

cluster non empty strict join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like complete \/-distributive /\-distributive for LattStr ;

existence ex b

( b

proof end;

theorem Th28: :: LATTICE3:28

for X being set

for L being Lattice

for p being Element of L holds

( p is_less_than X iff p % is_<=_than X )

for L being Lattice

for p being Element of L holds

( p is_less_than X iff p % is_<=_than X )

proof end;

theorem :: LATTICE3:29

for X being set

for L being Lattice

for p9 being Element of (LattPOSet L) holds

( p9 is_<=_than X iff % p9 is_less_than X )

for L being Lattice

for p9 being Element of (LattPOSet L) holds

( p9 is_<=_than X iff % p9 is_less_than X )

proof end;

theorem Th30: :: LATTICE3:30

for X being set

for L being Lattice

for p being Element of L holds

( X is_less_than p iff X is_<=_than p % )

for L being Lattice

for p being Element of L holds

( X is_less_than p iff X is_<=_than p % )

proof end;

theorem Th31: :: LATTICE3:31

for X being set

for L being Lattice

for p9 being Element of (LattPOSet L) holds

( X is_<=_than p9 iff X is_less_than % p9 )

for L being Lattice

for p9 being Element of (LattPOSet L) holds

( X is_<=_than p9 iff X is_less_than % p9 )

proof end;

definition

let L be non empty LattStr ;

assume A1: L is complete Lattice ;

let X be set ;

ex b_{1} being Element of L st

( X is_less_than b_{1} & ( for r being Element of L st X is_less_than r holds

b_{1} [= r ) )
by A1, Def18;

uniqueness

for b_{1}, b_{2} being Element of L st X is_less_than b_{1} & ( for r being Element of L st X is_less_than r holds

b_{1} [= r ) & X is_less_than b_{2} & ( for r being Element of L st X is_less_than r holds

b_{2} [= r ) holds

b_{1} = b_{2}

end;
assume A1: L is complete Lattice ;

let X be set ;

func "\/" (X,L) -> Element of L means :Def21: :: LATTICE3:def 21

( X is_less_than it & ( for r being Element of L st X is_less_than r holds

it [= r ) );

existence ( X is_less_than it & ( for r being Element of L st X is_less_than r holds

it [= r ) );

ex b

( X is_less_than b

b

uniqueness

for b

b

b

b

proof end;

:: deftheorem Def21 defines "\/" LATTICE3:def 21 :

for L being non empty LattStr st L is complete Lattice holds

for X being set

for b_{3} being Element of L holds

( b_{3} = "\/" (X,L) iff ( X is_less_than b_{3} & ( for r being Element of L st X is_less_than r holds

b_{3} [= r ) ) );

for L being non empty LattStr st L is complete Lattice holds

for X being set

for b

( b

b

definition

let L be non empty LattStr ;

let X be set ;

coherence

"\/" ( { p where p is Element of L : p is_less_than X } ,L) is Element of L;

;

end;
let X be set ;

func "/\" (X,L) -> Element of L equals :: LATTICE3:def 22

"\/" ( { p where p is Element of L : p is_less_than X } ,L);

correctness "\/" ( { p where p is Element of L : p is_less_than X } ,L);

coherence

"\/" ( { p where p is Element of L : p is_less_than X } ,L) is Element of L;

;

:: deftheorem defines "/\" LATTICE3:def 22 :

for L being non empty LattStr

for X being set holds "/\" (X,L) = "\/" ( { p where p is Element of L : p is_less_than X } ,L);

for L being non empty LattStr

for X being set holds "/\" (X,L) = "\/" ( { p where p is Element of L : p is_less_than X } ,L);

notation

let L be non empty LattStr ;

let X be Subset of L;

synonym "\/" X for "\/" (X,L);

synonym "/\" X for "/\" (X,L);

end;
let X be Subset of L;

synonym "\/" X for "\/" (X,L);

synonym "/\" X for "/\" (X,L);

theorem Th32: :: LATTICE3:32

for C being complete Lattice

for a being Element of C

for X being set holds "\/" ( { (a "/\" b) where b is Element of C : b in X } ,C) [= a "/\" ("\/" (X,C))

for a being Element of C

for X being set holds "\/" ( { (a "/\" b) where b is Element of C : b in X } ,C) [= a "/\" ("\/" (X,C))

proof end;

theorem Th33: :: LATTICE3:33

for C being complete Lattice holds

( C is \/-distributive iff for X being set

for a being Element of C holds a "/\" ("\/" (X,C)) [= "\/" ( { (a "/\" b) where b is Element of C : b in X } ,C) )

( C is \/-distributive iff for X being set

for a being Element of C holds a "/\" ("\/" (X,C)) [= "\/" ( { (a "/\" b) where b is Element of C : b in X } ,C) )

proof end;

theorem Th34: :: LATTICE3:34

for C being complete Lattice

for a being Element of C

for X being set holds

( a = "/\" (X,C) iff ( a is_less_than X & ( for b being Element of C st b is_less_than X holds

b [= a ) ) )

for a being Element of C

for X being set holds

( a = "/\" (X,C) iff ( a is_less_than X & ( for b being Element of C st b is_less_than X holds

b [= a ) ) )

proof end;

theorem Th35: :: LATTICE3:35

for C being complete Lattice

for a being Element of C

for X being set holds a "\/" ("/\" (X,C)) [= "/\" ( { (a "\/" b) where b is Element of C : b in X } ,C)

for a being Element of C

for X being set holds a "\/" ("/\" (X,C)) [= "/\" ( { (a "\/" b) where b is Element of C : b in X } ,C)

proof end;

theorem Th36: :: LATTICE3:36

for C being complete Lattice holds

( C is /\-distributive iff for X being set

for a being Element of C holds "/\" ( { (a "\/" b) where b is Element of C : b in X } ,C) [= a "\/" ("/\" (X,C)) )

( C is /\-distributive iff for X being set

for a being Element of C holds "/\" ( { (a "\/" b) where b is Element of C : b in X } ,C) [= a "\/" ("/\" (X,C)) )

proof end;

theorem :: LATTICE3:37

for C being complete Lattice

for X being set holds "\/" (X,C) = "/\" ( { a where a is Element of C : a is_greater_than X } ,C)

for X being set holds "\/" (X,C) = "/\" ( { a where a is Element of C : a is_greater_than X } ,C)

proof end;

theorem Th38: :: LATTICE3:38

for C being complete Lattice

for a being Element of C

for X being set st a in X holds

( a [= "\/" (X,C) & "/\" (X,C) [= a )

for a being Element of C

for X being set st a in X holds

( a [= "\/" (X,C) & "/\" (X,C) [= a )

proof end;

theorem Th39: :: LATTICE3:39

for C being complete Lattice

for a being Element of C

for X being set st a is_less_than X holds

a [= "/\" (X,C)

for a being Element of C

for X being set st a is_less_than X holds

a [= "/\" (X,C)

proof end;

theorem Th40: :: LATTICE3:40

for C being complete Lattice

for a being Element of C

for X being set st a in X & X is_less_than a holds

"\/" (X,C) = a

for a being Element of C

for X being set st a in X & X is_less_than a holds

"\/" (X,C) = a

proof end;

theorem Th41: :: LATTICE3:41

for C being complete Lattice

for a being Element of C

for X being set st a in X & a is_less_than X holds

"/\" (X,C) = a

for a being Element of C

for X being set st a in X & a is_less_than X holds

"/\" (X,C) = a

proof end;

theorem :: LATTICE3:43

for C being complete Lattice

for a, b being Element of C holds

( a "\/" b = "\/" {a,b} & a "/\" b = "/\" {a,b} )

for a, b being Element of C holds

( a "\/" b = "\/" {a,b} & a "/\" b = "/\" {a,b} )

proof end;

theorem :: LATTICE3:44

for C being complete Lattice

for a being Element of C holds

( a = "\/" ( { b where b is Element of C : b [= a } ,C) & a = "/\" ( { c where c is Element of C : a [= c } ,C) )

for a being Element of C holds

( a = "\/" ( { b where b is Element of C : b [= a } ,C) & a = "/\" ( { c where c is Element of C : a [= c } ,C) )

proof end;

theorem Th45: :: LATTICE3:45

for C being complete Lattice

for X, Y being set st X c= Y holds

( "\/" (X,C) [= "\/" (Y,C) & "/\" (Y,C) [= "/\" (X,C) )

for X, Y being set st X c= Y holds

( "\/" (X,C) [= "\/" (Y,C) & "/\" (Y,C) [= "/\" (X,C) )

proof end;

theorem Th46: :: LATTICE3:46

for C being complete Lattice

for X being set holds

( "\/" (X,C) = "\/" ( { a where a is Element of C : ex b being Element of C st

( a [= b & b in X ) } ,C) & "/\" (X,C) = "/\" ( { b where b is Element of C : ex a being Element of C st

( a [= b & a in X ) } ,C) )

for X being set holds

( "\/" (X,C) = "\/" ( { a where a is Element of C : ex b being Element of C st

( a [= b & b in X ) } ,C) & "/\" (X,C) = "/\" ( { b where b is Element of C : ex a being Element of C st

( a [= b & a in X ) } ,C) )

proof end;

theorem :: LATTICE3:47

for C being complete Lattice

for X, Y being set st ( for a being Element of C st a in X holds

ex b being Element of C st

( a [= b & b in Y ) ) holds

"\/" (X,C) [= "\/" (Y,C)

for X, Y being set st ( for a being Element of C st a in X holds

ex b being Element of C st

( a [= b & b in Y ) ) holds

"\/" (X,C) [= "\/" (Y,C)

proof end;

theorem :: LATTICE3:48

for C being complete Lattice

for X being set st X c= bool the carrier of C holds

"\/" ((union X),C) = "\/" ( { ("\/" Y) where Y is Subset of C : Y in X } ,C)

for X being set st X c= bool the carrier of C holds

"\/" ((union X),C) = "\/" ( { ("\/" Y) where Y is Subset of C : Y in X } ,C)

proof end;

theorem Th51: :: LATTICE3:51

for C being complete Lattice

for a, b being Element of C st C is I_Lattice holds

a => b = "\/" ( { c where c is Element of C : a "/\" c [= b } ,C)

for a, b being Element of C st C is I_Lattice holds

a => b = "\/" ( { c where c is Element of C : a "/\" c [= b } ,C)

proof end;

theorem :: LATTICE3:53

for X being set

for D being complete \/-distributive Lattice

for a being Element of D holds

( a "/\" ("\/" (X,D)) = "\/" ( { (a "/\" b1) where b1 is Element of D : b1 in X } ,D) & ("\/" (X,D)) "/\" a = "\/" ( { (b2 "/\" a) where b2 is Element of D : b2 in X } ,D) )

for D being complete \/-distributive Lattice

for a being Element of D holds

( a "/\" ("\/" (X,D)) = "\/" ( { (a "/\" b1) where b1 is Element of D : b1 in X } ,D) & ("\/" (X,D)) "/\" a = "\/" ( { (b2 "/\" a) where b2 is Element of D : b2 in X } ,D) )

proof end;

theorem :: LATTICE3:54

for X being set

for D being complete /\-distributive Lattice

for a being Element of D holds

( a "\/" ("/\" (X,D)) = "/\" ( { (a "\/" b1) where b1 is Element of D : b1 in X } ,D) & ("/\" (X,D)) "\/" a = "/\" ( { (b2 "\/" a) where b2 is Element of D : b2 in X } ,D) )

for D being complete /\-distributive Lattice

for a being Element of D holds

( a "\/" ("/\" (X,D)) = "/\" ( { (a "\/" b1) where b1 is Element of D : b1 in X } ,D) & ("/\" (X,D)) "\/" a = "/\" ( { (b2 "\/" a) where b2 is Element of D : b2 in X } ,D) )

proof end;

scheme :: LATTICE3:sch 2

FuncFraenkel{ F_{1}() -> non empty set , F_{2}() -> non empty set , F_{3}( set ) -> Element of F_{2}(), F_{4}() -> Function, P_{1}[ set ] } :

FuncFraenkel{ F

F_{4}() .: { F_{3}(x) where x is Element of F_{1}() : P_{1}[x] } = { (F_{4}() . F_{3}(x)) where x is Element of F_{1}() : P_{1}[x] }

provided
proof end;

Lm3: now :: thesis: for D being non empty set

for f being Function of (bool D),D st ( for a being Element of D holds f . {a} = a ) & ( for X being Subset-Family of D holds f . (f .: X) = f . (union X) ) holds

ex L being strict Lattice st

( H_{1}(L) = D & ( for X being Subset of L holds "\/" X = f . X ) )

for f being Function of (bool D),D st ( for a being Element of D holds f . {a} = a ) & ( for X being Subset-Family of D holds f . (f .: X) = f . (union X) ) holds

ex L being strict Lattice st

( H

let D be non empty set ; :: thesis: for f being Function of (bool D),D st ( for a being Element of D holds f . {a} = a ) & ( for X being Subset-Family of D holds f . (f .: X) = f . (union X) ) holds

ex L being strict Lattice st

( H_{1}(L) = D & ( for X being Subset of L holds "\/" X = f . X ) )

let f be Function of (bool D),D; :: thesis: ( ( for a being Element of D holds f . {a} = a ) & ( for X being Subset-Family of D holds f . (f .: X) = f . (union X) ) implies ex L being strict Lattice st

( H_{1}(L) = D & ( for X being Subset of L holds "\/" X = f . X ) ) )

assume that

A1: for a being Element of D holds f . {a} = a and

A2: for X being Subset-Family of D holds f . (f .: X) = f . (union X) ; :: thesis: ex L being strict Lattice st

( H_{1}(L) = D & ( for X being Subset of L holds "\/" X = f . X ) )

defpred S_{1}[ object , object ] means f . {$1,$2} = $2;

consider R being Relation of D such that

A3: for x, y being object holds

( [x,y] in R iff ( x in D & y in D & S_{1}[x,y] ) )
from RELSET_1:sch 1();

A4: dom f = bool D by FUNCT_2:def 1;

for X being Subset of D st y in X holds

f . (X \/ {x}) = f . { (f . {t,x}) where t is Element of D : t in X }

field R = D by A14, ORDERS_1:13;

then reconsider R = R as Order of D by A14, A16, A19, A27, PARTFUN1:def 2, RELAT_2:def 9, RELAT_2:def 12, RELAT_2:def 16;

set A = RelStr(# D,R #);

RelStr(# D,R #) is complete

take L = latt A; :: thesis: ( H_{1}(L) = D & ( for X being Subset of L holds "\/" X = f . X ) )

A34: ( A is with_suprema & A is with_infima ) by Th12;

then A35: A = LattPOSet L by Def15;

hence H_{1}(L) = D
; :: thesis: for X being Subset of L holds "\/" X = f . X

let X be Subset of L; :: thesis: "\/" X = f . X

reconsider Y = X as Subset of D by A35;

reconsider a = f . Y as Element of (LattPOSet L) by A34, Def15;

set p = % a;

X is_<=_than a

end;
ex L being strict Lattice st

( H

let f be Function of (bool D),D; :: thesis: ( ( for a being Element of D holds f . {a} = a ) & ( for X being Subset-Family of D holds f . (f .: X) = f . (union X) ) implies ex L being strict Lattice st

( H

assume that

A1: for a being Element of D holds f . {a} = a and

A2: for X being Subset-Family of D holds f . (f .: X) = f . (union X) ; :: thesis: ex L being strict Lattice st

( H

defpred S

consider R being Relation of D such that

A3: for x, y being object holds

( [x,y] in R iff ( x in D & y in D & S

A4: dom f = bool D by FUNCT_2:def 1;

A5: now :: thesis: for x, y being Subset of D holds f . {(f . x),(f . y)} = f . (x \/ y)

A6:
for x, y being Element of D
let x, y be Subset of D; :: thesis: f . {(f . x),(f . y)} = f . (x \/ y)

thus f . {(f . x),(f . y)} = f . (f .: {x,y}) by A4, FUNCT_1:60

.= f . (union {x,y}) by A2

.= f . (x \/ y) by ZFMISC_1:75 ; :: thesis: verum

end;
thus f . {(f . x),(f . y)} = f . (f .: {x,y}) by A4, FUNCT_1:60

.= f . (union {x,y}) by A2

.= f . (x \/ y) by ZFMISC_1:75 ; :: thesis: verum

for X being Subset of D st y in X holds

f . (X \/ {x}) = f . { (f . {t,x}) where t is Element of D : t in X }

proof

A14:
R is_reflexive_in D
let x, y be Element of D; :: thesis: for X being Subset of D st y in X holds

f . (X \/ {x}) = f . { (f . {t,x}) where t is Element of D : t in X }

let X be Subset of D; :: thesis: ( y in X implies f . (X \/ {x}) = f . { (f . {t,x}) where t is Element of D : t in X } )

assume A7: y in X ; :: thesis: f . (X \/ {x}) = f . { (f . {t,x}) where t is Element of D : t in X }

set Y = { {t,x} where t is Element of D : t in X } ;

A8: X \/ {x} = union { {t,x} where t is Element of D : t in X }

defpred S_{2}[ set ] means $1 in X;

deffunc H_{4}( Element of D) -> Element of bool D = {$1,x};

A13: bool D c= dom f by FUNCT_2:def 1;

f .: { H_{4}(t) where t is Element of D : S_{2}[t] } = { (f . H_{4}(t)) where t is Element of D : S_{2}[t] }
from LATTICE3:sch 2(A13);

then f . (union Y) = f . { (f . {t,x}) where t is Element of D : t in X } by A2;

hence f . (X \/ {x}) = f . { (f . {t,x}) where t is Element of D : t in X } by A8; :: thesis: verum

end;
f . (X \/ {x}) = f . { (f . {t,x}) where t is Element of D : t in X }

let X be Subset of D; :: thesis: ( y in X implies f . (X \/ {x}) = f . { (f . {t,x}) where t is Element of D : t in X } )

assume A7: y in X ; :: thesis: f . (X \/ {x}) = f . { (f . {t,x}) where t is Element of D : t in X }

set Y = { {t,x} where t is Element of D : t in X } ;

A8: X \/ {x} = union { {t,x} where t is Element of D : t in X }

proof

{ {t,x} where t is Element of D : t in X } c= bool D
thus
X \/ {x} c= union { {t,x} where t is Element of D : t in X }
:: according to XBOOLE_0:def 10 :: thesis: union { {t,x} where t is Element of D : t in X } c= X \/ {x}

assume s in union { {t,x} where t is Element of D : t in X } ; :: thesis: s in X \/ {x}

then consider Z being set such that

A9: s in Z and

A10: Z in { {t,x} where t is Element of D : t in X } by TARSKI:def 4;

consider t being Element of D such that

A11: Z = {t,x} and

A12: t in X by A10;

( s = t or ( s = x & x in {x} ) ) by A9, A11, TARSKI:def 1, TARSKI:def 2;

hence s in X \/ {x} by A12, XBOOLE_0:def 3; :: thesis: verum

end;
proof

let s be object ; :: according to TARSKI:def 3 :: thesis: ( not s in union { {t,x} where t is Element of D : t in X } or s in X \/ {x} )
let s be object ; :: according to TARSKI:def 3 :: thesis: ( not s in X \/ {x} or s in union { {t,x} where t is Element of D : t in X } )

assume s in X \/ {x} ; :: thesis: s in union { {t,x} where t is Element of D : t in X }

then ( ( s in X & X c= D ) or s in {x} ) by XBOOLE_0:def 3;

then ( ( s in X & s is Element of D ) or s = x ) by TARSKI:def 1;

then ( ( s in {s,x} & {s,x} in { {t,x} where t is Element of D : t in X } ) or ( s in {y,x} & {y,x} in { {t,x} where t is Element of D : t in X } ) ) by A7, TARSKI:def 2;

hence s in union { {t,x} where t is Element of D : t in X } by TARSKI:def 4; :: thesis: verum

end;
assume s in X \/ {x} ; :: thesis: s in union { {t,x} where t is Element of D : t in X }

then ( ( s in X & X c= D ) or s in {x} ) by XBOOLE_0:def 3;

then ( ( s in X & s is Element of D ) or s = x ) by TARSKI:def 1;

then ( ( s in {s,x} & {s,x} in { {t,x} where t is Element of D : t in X } ) or ( s in {y,x} & {y,x} in { {t,x} where t is Element of D : t in X } ) ) by A7, TARSKI:def 2;

hence s in union { {t,x} where t is Element of D : t in X } by TARSKI:def 4; :: thesis: verum

assume s in union { {t,x} where t is Element of D : t in X } ; :: thesis: s in X \/ {x}

then consider Z being set such that

A9: s in Z and

A10: Z in { {t,x} where t is Element of D : t in X } by TARSKI:def 4;

consider t being Element of D such that

A11: Z = {t,x} and

A12: t in X by A10;

( s = t or ( s = x & x in {x} ) ) by A9, A11, TARSKI:def 1, TARSKI:def 2;

hence s in X \/ {x} by A12, XBOOLE_0:def 3; :: thesis: verum

proof

then reconsider Y = { {t,x} where t is Element of D : t in X } as Subset-Family of D ;
let s be object ; :: according to TARSKI:def 3 :: thesis: ( not s in { {t,x} where t is Element of D : t in X } or s in bool D )

reconsider ss = s as set by TARSKI:1;

assume s in { {t,x} where t is Element of D : t in X } ; :: thesis: s in bool D

then ss c= X \/ {x} by A8, ZFMISC_1:74;

then ss c= D by XBOOLE_1:1;

hence s in bool D ; :: thesis: verum

end;
reconsider ss = s as set by TARSKI:1;

assume s in { {t,x} where t is Element of D : t in X } ; :: thesis: s in bool D

then ss c= X \/ {x} by A8, ZFMISC_1:74;

then ss c= D by XBOOLE_1:1;

hence s in bool D ; :: thesis: verum

defpred S

deffunc H

A13: bool D c= dom f by FUNCT_2:def 1;

f .: { H

then f . (union Y) = f . { (f . {t,x}) where t is Element of D : t in X } by A2;

hence f . (X \/ {x}) = f . { (f . {t,x}) where t is Element of D : t in X } by A8; :: thesis: verum

proof

A16:
R is_antisymmetric_in D
let x be object ; :: according to RELAT_2:def 1 :: thesis: ( not x in D or [x,x] in R )

assume A15: x in D ; :: thesis: [x,x] in R

then x = f . {x} by A1

.= f . {x,x} by ENUMSET1:29 ;

hence [x,x] in R by A3, A15; :: thesis: verum

end;
assume A15: x in D ; :: thesis: [x,x] in R

then x = f . {x} by A1

.= f . {x,x} by ENUMSET1:29 ;

hence [x,x] in R by A3, A15; :: thesis: verum

proof

A19:
R is_transitive_in D
let x, y be object ; :: according to RELAT_2:def 4 :: thesis: ( not x in D or not y in D or not [x,y] in R or not [y,x] in R or x = y )

assume that

x in D and

y in D and

A17: [x,y] in R and

A18: [y,x] in R ; :: thesis: x = y

f . {x,y} = y by A3, A17;

hence x = y by A3, A18; :: thesis: verum

end;
assume that

x in D and

y in D and

A17: [x,y] in R and

A18: [y,x] in R ; :: thesis: x = y

f . {x,y} = y by A3, A17;

hence x = y by A3, A18; :: thesis: verum

proof

A27:
dom R = D
by A14, ORDERS_1:13;
let x, y, z be object ; :: according to RELAT_2:def 8 :: thesis: ( not x in D or not y in D or not z in D or not [x,y] in R or not [y,z] in R or [x,z] in R )

assume that

A20: x in D and

A21: y in D and

A22: z in D and

A23: [x,y] in R and

A24: [y,z] in R ; :: thesis: [x,z] in R

reconsider a = x, b = y, c = z as Element of D by A20, A21, A22;

A25: f . {x,y} = y by A3, A23;

A26: f . {y,z} = z by A3, A24;

then f . {a,c} = f . {(f . {a}),(f . {b,c})} by A1

.= f . ({a} \/ {b,c}) by A5

.= f . {a,b,c} by ENUMSET1:2

.= f . ({a,b} \/ {c}) by ENUMSET1:3

.= f . {(f . {a,b}),(f . {c})} by A5

.= c by A1, A25, A26 ;

hence [x,z] in R by A3; :: thesis: verum

end;
assume that

A20: x in D and

A21: y in D and

A22: z in D and

A23: [x,y] in R and

A24: [y,z] in R ; :: thesis: [x,z] in R

reconsider a = x, b = y, c = z as Element of D by A20, A21, A22;

A25: f . {x,y} = y by A3, A23;

A26: f . {y,z} = z by A3, A24;

then f . {a,c} = f . {(f . {a}),(f . {b,c})} by A1

.= f . ({a} \/ {b,c}) by A5

.= f . {a,b,c} by ENUMSET1:2

.= f . ({a,b} \/ {c}) by ENUMSET1:3

.= f . {(f . {a,b}),(f . {c})} by A5

.= c by A1, A25, A26 ;

hence [x,z] in R by A3; :: thesis: verum

field R = D by A14, ORDERS_1:13;

then reconsider R = R as Order of D by A14, A16, A19, A27, PARTFUN1:def 2, RELAT_2:def 9, RELAT_2:def 12, RELAT_2:def 16;

set A = RelStr(# D,R #);

RelStr(# D,R #) is complete

proof

then reconsider A = RelStr(# D,R #) as non empty strict complete Poset ;
let X be set ; :: according to LATTICE3:def 12 :: thesis: ex a being Element of RelStr(# D,R #) st

( X is_<=_than a & ( for b being Element of RelStr(# D,R #) st X is_<=_than b holds

a <= b ) )

reconsider Y = X /\ D as Subset of D by XBOOLE_1:17;

reconsider a = f . Y as Element of RelStr(# D,R #) ;

take a ; :: thesis: ( X is_<=_than a & ( for b being Element of RelStr(# D,R #) st X is_<=_than b holds

a <= b ) )

thus X is_<=_than a :: thesis: for b being Element of RelStr(# D,R #) st X is_<=_than b holds

a <= b

assume A28: X is_<=_than b ; :: thesis: a <= b

A29: f . {a,b} = f . {a,(f . {b})} by A1

.= f . (Y \/ {b}) by A5 ;

end;
( X is_<=_than a & ( for b being Element of RelStr(# D,R #) st X is_<=_than b holds

a <= b ) )

reconsider Y = X /\ D as Subset of D by XBOOLE_1:17;

reconsider a = f . Y as Element of RelStr(# D,R #) ;

take a ; :: thesis: ( X is_<=_than a & ( for b being Element of RelStr(# D,R #) st X is_<=_than b holds

a <= b ) )

thus X is_<=_than a :: thesis: for b being Element of RelStr(# D,R #) st X is_<=_than b holds

a <= b

proof

let b be Element of RelStr(# D,R #); :: thesis: ( X is_<=_than b implies a <= b )
let b be Element of RelStr(# D,R #); :: according to LATTICE3:def 9 :: thesis: ( b in X implies b <= a )

assume b in X ; :: thesis: b <= a

then b in Y by XBOOLE_0:def 4;

then {b} \/ Y = Y by ZFMISC_1:40;

then a = f . {(f . {b}),a} by A5

.= f . {b,a} by A1 ;

hence [b,a] in the InternalRel of RelStr(# D,R #) by A3; :: according to ORDERS_2:def 5 :: thesis: verum

end;
assume b in X ; :: thesis: b <= a

then b in Y by XBOOLE_0:def 4;

then {b} \/ Y = Y by ZFMISC_1:40;

then a = f . {(f . {b}),a} by A5

.= f . {b,a} by A1 ;

hence [b,a] in the InternalRel of RelStr(# D,R #) by A3; :: according to ORDERS_2:def 5 :: thesis: verum

assume A28: X is_<=_than b ; :: thesis: a <= b

A29: f . {a,b} = f . {a,(f . {b})} by A1

.= f . (Y \/ {b}) by A5 ;

now :: thesis: f . {a,b} = b
end;

hence
[a,b] in the InternalRel of RelStr(# D,R #)
by A3; :: according to ORDERS_2:def 5 :: thesis: verum
per cases
( Y <> {} or Y = {} )
;

end;

suppose A30:
Y <> {}
; :: thesis: f . {a,b} = b

set s = the Element of Y;

reconsider s = the Element of Y as Element of D by A30, TARSKI:def 3;

deffunc H_{4}( Element of D) -> set = f . {$1,b};

deffunc H_{5}( Element of D) -> Element of RelStr(# D,R #) = b;

defpred S_{2}[ set ] means $1 in Y;

A31: for t being Element of D st S_{2}[t] holds

H_{4}(t) = H_{5}(t)

then A33: ex t being Element of D st S_{2}[t]
;

{ H_{4}(t) where t is Element of D : S_{2}[t] } =
{ H_{5}(t) where t is Element of D : S_{2}[t] }
from FRAENKEL:sch 6(A31)

.= { b where t is Element of D : S_{2}[t] }

.= {b} from LATTICE3:sch 1(A33) ;

hence f . {a,b} = f . {b} by A6, A29, A32

.= b by A1 ;

:: thesis: verum

end;
reconsider s = the Element of Y as Element of D by A30, TARSKI:def 3;

deffunc H

deffunc H

defpred S

A31: for t being Element of D st S

H

proof

A32:
s in Y
by A30;
let t be Element of D; :: thesis: ( S_{2}[t] implies H_{4}(t) = H_{5}(t) )

reconsider s = t as Element of RelStr(# D,R #) ;

reconsider y = b as Element of D ;

assume t in Y ; :: thesis: H_{4}(t) = H_{5}(t)

then t in X by XBOOLE_0:def 4;

then s <= b by A28;

then [t,y] in R ;

hence H_{4}(t) = H_{5}(t)
by A3; :: thesis: verum

end;
reconsider s = t as Element of RelStr(# D,R #) ;

reconsider y = b as Element of D ;

assume t in Y ; :: thesis: H

then t in X by XBOOLE_0:def 4;

then s <= b by A28;

then [t,y] in R ;

hence H

then A33: ex t being Element of D st S

{ H

.= { b where t is Element of D : S

.= {b} from LATTICE3:sch 1(A33) ;

hence f . {a,b} = f . {b} by A6, A29, A32

.= b by A1 ;

:: thesis: verum

take L = latt A; :: thesis: ( H

A34: ( A is with_suprema & A is with_infima ) by Th12;

then A35: A = LattPOSet L by Def15;

hence H

let X be Subset of L; :: thesis: "\/" X = f . X

reconsider Y = X as Subset of D by A35;

reconsider a = f . Y as Element of (LattPOSet L) by A34, Def15;

set p = % a;

X is_<=_than a

proof

then A37:
X is_less_than % a
by Th31;
let b be Element of (LattPOSet L); :: according to LATTICE3:def 9 :: thesis: ( b in X implies b <= a )

reconsider y = b as Element of D by A34, Def15;

assume b in X ; :: thesis: b <= a

then A36: X = {b} \/ X by ZFMISC_1:40;

f . {y,(f . Y)} = f . {(f . {y}),(f . Y)} by A1

.= a by A5, A36 ;

hence [b,a] in the InternalRel of (LattPOSet L) by A3, A35; :: according to ORDERS_2:def 5 :: thesis: verum

end;
reconsider y = b as Element of D by A34, Def15;

assume b in X ; :: thesis: b <= a

then A36: X = {b} \/ X by ZFMISC_1:40;

f . {y,(f . Y)} = f . {(f . {y}),(f . Y)} by A1

.= a by A5, A36 ;

hence [b,a] in the InternalRel of (LattPOSet L) by A3, A35; :: according to ORDERS_2:def 5 :: thesis: verum

now :: thesis: for q being Element of L st X is_less_than q holds

% a [= q

hence
"\/" X = f . X
by A37, Def21; :: thesis: verum% a [= q

let q be Element of L; :: thesis: ( X is_less_than q implies % a [= q )

reconsider y = q as Element of D by A35;

reconsider b = y as Element of (LattPOSet L) ;

assume X is_less_than q ; :: thesis: % a [= q

then A38: X is_<=_than q % by Th30;

A39: f . {(f . Y),b} = f . {(f . Y),(f . {y})} by A1

.= f . (Y \/ {b}) by A5 ;

then A44: a <= b ;

A45: (% a) % = % a ;

q % = b ;

hence % a [= q by A44, A45, Th7; :: thesis: verum

end;
reconsider y = q as Element of D by A35;

reconsider b = y as Element of (LattPOSet L) ;

assume X is_less_than q ; :: thesis: % a [= q

then A38: X is_<=_than q % by Th30;

A39: f . {(f . Y),b} = f . {(f . Y),(f . {y})} by A1

.= f . (Y \/ {b}) by A5 ;

now :: thesis: f . {a,b} = b
end;

then
[a,b] in the InternalRel of (LattPOSet L)
by A3, A35;
per cases
( Y <> {} or Y = {} )
;

end;

suppose A40:
Y <> {}
; :: thesis: f . {a,b} = b

set s = the Element of Y;

reconsider s = the Element of Y as Element of D by A40, TARSKI:def 3;

deffunc H_{4}( Element of D) -> set = f . {$1,b};

deffunc H_{5}( Element of D) -> Element of (LattPOSet L) = b;

defpred S_{2}[ set ] means $1 in Y;

A41: for t being Element of D st S_{2}[t] holds

H_{4}(t) = H_{5}(t)

then A43: ex t being Element of D st S_{2}[t]
;

{ H_{4}(t) where t is Element of D : S_{2}[t] } =
{ H_{5}(t) where t is Element of D : S_{2}[t] }
from FRAENKEL:sch 6(A41)

.= { b where t is Element of D : S_{2}[t] }

.= {b} from LATTICE3:sch 1(A43) ;

hence f . {a,b} = f . {b} by A6, A39, A42

.= b by A1 ;

:: thesis: verum

end;
reconsider s = the Element of Y as Element of D by A40, TARSKI:def 3;

deffunc H

deffunc H

defpred S

A41: for t being Element of D st S

H

proof

A42:
s in Y
by A40;
let t be Element of D; :: thesis: ( S_{2}[t] implies H_{4}(t) = H_{5}(t) )

reconsider s = t as Element of (LattPOSet L) by A34, Def15;

assume t in Y ; :: thesis: H_{4}(t) = H_{5}(t)

then s <= b by A38;

then [t,y] in R by A35;

hence H_{4}(t) = H_{5}(t)
by A3; :: thesis: verum

end;
reconsider s = t as Element of (LattPOSet L) by A34, Def15;

assume t in Y ; :: thesis: H

then s <= b by A38;

then [t,y] in R by A35;

hence H

then A43: ex t being Element of D st S

{ H

.= { b where t is Element of D : S

.= {b} from LATTICE3:sch 1(A43) ;

hence f . {a,b} = f . {b} by A6, A39, A42

.= b by A1 ;

:: thesis: verum

then A44: a <= b ;

A45: (% a) % = % a ;

q % = b ;

hence % a [= q by A44, A45, Th7; :: thesis: verum

theorem :: LATTICE3:55

for D being non empty set

for f being Function of (bool D),D st ( for a being Element of D holds f . {a} = a ) & ( for X being Subset-Family of D holds f . (f .: X) = f . (union X) ) holds

ex L being strict complete Lattice st

( the carrier of L = D & ( for X being Subset of L holds "\/" X = f . X ) ) by Lm3;

for f being Function of (bool D),D st ( for a being Element of D holds f . {a} = a ) & ( for X being Subset-Family of D holds f . (f .: X) = f . (union X) ) holds

ex L being strict complete Lattice st

( the carrier of L = D & ( for X being Subset of L holds "\/" X = f . X ) ) by Lm3;