:: LATTICES semantic presentation  Show TPTP formulae Show IDV graph for whole article:: Showing IDV graph ... (Click the Palm Trees again to close it)

definition
attr c1 is strict;
struct /\-SemiLattStr -> 1-sorted ;
aggr /\-SemiLattStr(# carrier, L_meet #) -> /\-SemiLattStr ;
sel L_meet c1 -> BinOp of the carrier of c1;
end;

definition
attr c1 is strict;
struct \/-SemiLattStr -> 1-sorted ;
aggr \/-SemiLattStr(# carrier, L_join #) -> \/-SemiLattStr ;
sel L_join c1 -> BinOp of the carrier of c1;
end;

definition
attr c1 is strict;
struct LattStr -> /\-SemiLattStr , \/-SemiLattStr ;
aggr LattStr(# carrier, L_join, L_meet #) -> LattStr ;
end;

registration
let D be non empty set ;
let u be BinOp of D;
cluster \/-SemiLattStr(# D,u #) -> non empty ;
coherence
not \/-SemiLattStr(# D,u #) is empty by STRUCT_0:def 1;
cluster /\-SemiLattStr(# D,u #) -> non empty ;
coherence
not /\-SemiLattStr(# D,u #) is empty by STRUCT_0:def 1;
end;

registration
let D be non empty set ;
let u, n be BinOp of D;
cluster LattStr(# D,u,n #) -> non empty ;
coherence
not LattStr(# D,u,n #) is empty by STRUCT_0:def 1;
end;

registration
cluster non empty strict \/-SemiLattStr ;
existence
ex b1 being \/-SemiLattStr st
( b1 is strict & not b1 is empty )
proof end;
cluster non empty strict /\-SemiLattStr ;
existence
ex b1 being /\-SemiLattStr st
( b1 is strict & not b1 is empty )
proof end;
cluster non empty strict LattStr ;
existence
ex b1 being LattStr st
( b1 is strict & not b1 is empty )
proof end;
end;

definition
let G be non empty \/-SemiLattStr ;
let p, q be Element of G;
func p "\/" q -> Element of G equals :: LATTICES:def 1
the L_join of G . p,q;
coherence
the L_join of G . p,q is Element of G ;
end;

:: deftheorem defines "\/" LATTICES:def 1 :
for G being non empty \/-SemiLattStr
for p, q being Element of G holds p "\/" q = the L_join of G . p,q;

definition
let G be non empty /\-SemiLattStr ;
let p, q be Element of G;
func p "/\" q -> Element of G equals :: LATTICES:def 2
the L_meet of G . p,q;
coherence
the L_meet of G . p,q is Element of G ;
end;

:: deftheorem defines "/\" LATTICES:def 2 :
for G being non empty /\-SemiLattStr
for p, q being Element of G holds p "/\" q = the L_meet of G . p,q;

definition
let G be non empty \/-SemiLattStr ;
let p, q be Element of G;
pred p [= q means :Def3: :: LATTICES:def 3
p "\/" q = q;
end;

:: deftheorem Def3 defines [= LATTICES:def 3 :
for G being non empty \/-SemiLattStr
for p, q being Element of G holds
( p [= q iff p "\/" q = q );

Lm1: for uu, nn being BinOp of bool {}
for x, y being Element of LattStr(# (bool {} ),uu,nn #) holds x = y
proof end;

Lm2: for n being BinOp of bool {}
for x, y being Element of \/-SemiLattStr(# (bool {} ),n #) holds x = y
proof end;

Lm3: for n being BinOp of bool {}
for x, y being Element of /\-SemiLattStr(# (bool {} ),n #) holds x = y
proof end;

definition
let IT be non empty \/-SemiLattStr ;
attr IT is join-commutative means :Def4: :: LATTICES:def 4
for a, b being Element of IT holds a "\/" b = b "\/" a;
attr IT is join-associative means :Def5: :: LATTICES:def 5
for a, b, c being Element of IT holds a "\/" (b "\/" c) = (a "\/" b) "\/" c;
end;

:: deftheorem Def4 defines join-commutative LATTICES:def 4 :
for IT being non empty \/-SemiLattStr holds
( IT is join-commutative iff for a, b being Element of IT holds a "\/" b = b "\/" a );

:: deftheorem Def5 defines join-associative LATTICES:def 5 :
for IT being non empty \/-SemiLattStr holds
( IT is join-associative iff for a, b, c being Element of IT holds a "\/" (b "\/" c) = (a "\/" b) "\/" c );

definition
let IT be non empty /\-SemiLattStr ;
attr IT is meet-commutative means :Def6: :: LATTICES:def 6
for a, b being Element of IT holds a "/\" b = b "/\" a;
attr IT is meet-associative means :Def7: :: LATTICES:def 7
for a, b, c being Element of IT holds a "/\" (b "/\" c) = (a "/\" b) "/\" c;
end;

:: deftheorem Def6 defines meet-commutative LATTICES:def 6 :
for IT being non empty /\-SemiLattStr holds
( IT is meet-commutative iff for a, b being Element of IT holds a "/\" b = b "/\" a );

:: deftheorem Def7 defines meet-associative LATTICES:def 7 :
for IT being non empty /\-SemiLattStr holds
( IT is meet-associative iff for a, b, c being Element of IT holds a "/\" (b "/\" c) = (a "/\" b) "/\" c );

definition
let IT be non empty LattStr ;
attr IT is meet-absorbing means :Def8: :: LATTICES:def 8
for a, b being Element of IT holds (a "/\" b) "\/" b = b;
attr IT is join-absorbing means :Def9: :: LATTICES:def 9
for a, b being Element of IT holds a "/\" (a "\/" b) = a;
end;

:: deftheorem Def8 defines meet-absorbing LATTICES:def 8 :
for IT being non empty LattStr holds
( IT is meet-absorbing iff for a, b being Element of IT holds (a "/\" b) "\/" b = b );

:: deftheorem Def9 defines join-absorbing LATTICES:def 9 :
for IT being non empty LattStr holds
( IT is join-absorbing iff for a, b being Element of IT holds a "/\" (a "\/" b) = a );

definition
let IT be non empty LattStr ;
attr IT is Lattice-like means :Def10: :: LATTICES:def 10
( IT is join-commutative & IT is join-associative & IT is meet-absorbing & IT is meet-commutative & IT is meet-associative & IT is join-absorbing );
end;

:: deftheorem Def10 defines Lattice-like LATTICES:def 10 :
for IT being non empty LattStr holds
( IT is Lattice-like iff ( IT is join-commutative & IT is join-associative & IT is meet-absorbing & IT is meet-commutative & IT is meet-associative & IT is join-absorbing ) );

registration
cluster non empty Lattice-like -> non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing LattStr ;
coherence
for b1 being non empty LattStr st b1 is Lattice-like holds
( b1 is join-commutative & b1 is join-associative & b1 is meet-absorbing & b1 is meet-commutative & b1 is meet-associative & b1 is join-absorbing ) by Def10;
cluster non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing -> non empty Lattice-like LattStr ;
coherence
for b1 being non empty LattStr st b1 is join-commutative & b1 is join-associative & b1 is meet-absorbing & b1 is meet-commutative & b1 is meet-associative & b1 is join-absorbing holds
b1 is Lattice-like by Def10;
end;

registration
cluster non empty strict join-commutative join-associative \/-SemiLattStr ;
existence
ex b1 being non empty \/-SemiLattStr st
( b1 is strict & b1 is join-commutative & b1 is join-associative )
proof end;
cluster non empty strict meet-commutative meet-associative /\-SemiLattStr ;
existence
ex b1 being non empty /\-SemiLattStr st
( b1 is strict & b1 is meet-commutative & b1 is meet-associative )
proof end;
cluster non empty strict join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like LattStr ;
existence
ex b1 being non empty LattStr st
( b1 is strict & b1 is Lattice-like )
proof end;
end;

definition
mode Lattice is non empty Lattice-like LattStr ;
end;

definition
let L be non empty join-commutative \/-SemiLattStr ;
let a, b be Element of L;
:: original: "\/"
redefine func a "\/" b -> Element of L;
commutativity
for a, b being Element of L holds a "\/" b = b "\/" a by Def4;
end;

definition
let L be non empty meet-commutative /\-SemiLattStr ;
let a, b be Element of L;
:: original: "/\"
redefine func a "/\" b -> Element of L;
commutativity
for a, b being Element of L holds a "/\" b = b "/\" a by Def6;
end;

definition
let IT be non empty LattStr ;
attr IT is distributive means :Def11: :: LATTICES:def 11
for a, b, c being Element of IT holds a "/\" (b "\/" c) = (a "/\" b) "\/" (a "/\" c);
end;

:: deftheorem Def11 defines distributive LATTICES:def 11 :
for IT being non empty LattStr holds
( IT is distributive iff for a, b, c being Element of IT holds a "/\" (b "\/" c) = (a "/\" b) "\/" (a "/\" c) );

definition
let IT be non empty LattStr ;
attr IT is modular means :Def12: :: LATTICES:def 12
for a, b, c being Element of IT st a [= c holds
a "\/" (b "/\" c) = (a "\/" b) "/\" c;
end;

:: deftheorem Def12 defines modular LATTICES:def 12 :
for IT being non empty LattStr holds
( IT is modular iff for a, b, c being Element of IT st a [= c holds
a "\/" (b "/\" c) = (a "\/" b) "/\" c );

definition
let IT be non empty /\-SemiLattStr ;
attr IT is lower-bounded means :Def13: :: LATTICES:def 13
 ex c being Element of IT st
for a being Element of IT holds
( c "/\" a = c & a "/\" c = c );
end;

:: deftheorem Def13 defines lower-bounded LATTICES:def 13 :
for IT being non empty /\-SemiLattStr holds
( IT is lower-bounded iff ex c being Element of IT st
for a being Element of IT holds
( c "/\" a = c & a "/\" c = c ) );

definition
let IT be non empty \/-SemiLattStr ;
attr IT is upper-bounded means :Def14: :: LATTICES:def 14
 ex c being Element of IT st
for a being Element of IT holds
( c "\/" a = c & a "\/" c = c );
end;

:: deftheorem Def14 defines upper-bounded LATTICES:def 14 :
for IT being non empty \/-SemiLattStr holds
( IT is upper-bounded iff ex c being Element of IT st
for a being Element of IT holds
( c "\/" a = c & a "\/" c = c ) );

Lm4: for n, u being BinOp of bool {} holds LattStr(# (bool {} ),n,u #) is Lattice
proof end;

registration
cluster strict distributive modular lower-bounded upper-bounded LattStr ;
existence
ex b1 being Lattice st
( b1 is strict & b1 is distributive & b1 is lower-bounded & b1 is upper-bounded & b1 is modular )
proof end;
end;

definition
mode D_Lattice is distributive Lattice;
mode M_Lattice is modular Lattice;
mode 0_Lattice is lower-bounded Lattice;
mode 1_Lattice is upper-bounded Lattice;
end;

Lm5: for n, u being BinOp of bool {} holds LattStr(# (bool {} ),n,u #) is 0_Lattice
proof end;

Lm6: for n, u being BinOp of bool {} holds LattStr(# (bool {} ),n,u #) is 1_Lattice
proof end;

definition
let IT be non empty LattStr ;
attr IT is bounded means :Def15: :: LATTICES:def 15
( IT is lower-bounded & IT is upper-bounded );
end;

:: deftheorem Def15 defines bounded LATTICES:def 15 :
for IT being non empty LattStr holds
( IT is bounded iff ( IT is lower-bounded & IT is upper-bounded ) );

registration
cluster non empty lower-bounded upper-bounded -> non empty bounded LattStr ;
coherence
for b1 being non empty LattStr st b1 is lower-bounded & b1 is upper-bounded holds
b1 is bounded by Def15;
cluster non empty bounded -> non empty lower-bounded upper-bounded LattStr ;
coherence
for b1 being non empty LattStr st b1 is bounded holds
( b1 is lower-bounded & b1 is upper-bounded ) by Def15;
end;

registration
cluster strict lower-bounded upper-bounded bounded LattStr ;
existence
ex b1 being Lattice st
( b1 is bounded & b1 is strict )
proof end;
end;

definition
mode 01_Lattice is bounded Lattice;
end;

definition
let L be non empty /\-SemiLattStr ;
assume A1: L is lower-bounded ;
func Bottom L -> Element of L means :Def16: :: LATTICES:def 16
for a being Element of L holds
( it "/\" a = it & a "/\" it = it );
existence
ex b1 being Element of L st
for a being Element of L holds
( b1 "/\" a = b1 & a "/\" b1 = b1 ) by A1, Def13;
uniqueness
for b1, b2 being Element of L st ( for a being Element of L holds
( b1 "/\" a = b1 & a "/\" b1 = b1 ) ) & ( for a being Element of L holds
( b2 "/\" a = b2 & a "/\" b2 = b2 ) ) holds
b1 = b2
proof end;
end;

:: deftheorem Def16 defines Bottom LATTICES:def 16 :
for L being non empty /\-SemiLattStr st L is lower-bounded holds
for b2 being Element of L holds
( b2 = Bottom L iff for a being Element of L holds
( b2 "/\" a = b2 & a "/\" b2 = b2 ) );

definition
let L be non empty \/-SemiLattStr ;
assume A1: L is upper-bounded ;
func Top L -> Element of L means :Def17: :: LATTICES:def 17
for a being Element of L holds
( it "\/" a = it & a "\/" it = it );
existence
ex b1 being Element of L st
for a being Element of L holds
( b1 "\/" a = b1 & a "\/" b1 = b1 ) by A1, Def14;
uniqueness
for b1, b2 being Element of L st ( for a being Element of L holds
( b1 "\/" a = b1 & a "\/" b1 = b1 ) ) & ( for a being Element of L holds
( b2 "\/" a = b2 & a "\/" b2 = b2 ) ) holds
b1 = b2
proof end;
end;

:: deftheorem Def17 defines Top LATTICES:def 17 :
for L being non empty \/-SemiLattStr st L is upper-bounded holds
for b2 being Element of L holds
( b2 = Top L iff for a being Element of L holds
( b2 "\/" a = b2 & a "\/" b2 = b2 ) );

definition
let L be non empty LattStr ;
let a, b be Element of L;
pred a is_a_complement_of b means :Def18: :: LATTICES:def 18
( a "\/" b = Top L & b "\/" a = Top L & a "/\" b = Bottom L & b "/\" a = Bottom L );
end;

:: deftheorem Def18 defines is_a_complement_of LATTICES:def 18 :
for L being non empty LattStr
for a, b being Element of L holds
( a is_a_complement_of b iff ( a "\/" b = Top L & b "\/" a = Top L & a "/\" b = Bottom L & b "/\" a = Bottom L ) );

definition
let IT be non empty LattStr ;
attr IT is complemented means :Def19: :: LATTICES:def 19
for b being Element of IT ex a being Element of IT st a is_a_complement_of b;
end;

:: deftheorem Def19 defines complemented LATTICES:def 19 :
for IT being non empty LattStr holds
( IT is complemented iff for b being Element of IT ex a being Element of IT st a is_a_complement_of b );

registration
cluster strict lower-bounded upper-bounded bounded complemented LattStr ;
existence
ex b1 being Lattice st
( b1 is bounded & b1 is complemented & b1 is strict )
proof end;
end;

definition
mode C_Lattice is complemented 01_Lattice;
end;

definition
let IT be non empty LattStr ;
attr IT is Boolean means :Def20: :: LATTICES:def 20
( IT is bounded & IT is complemented & IT is distributive );
end;

:: deftheorem Def20 defines Boolean LATTICES:def 20 :
for IT being non empty LattStr holds
( IT is Boolean iff ( IT is bounded & IT is complemented & IT is distributive ) );

registration
cluster non empty Boolean -> non empty distributive lower-bounded upper-bounded bounded complemented LattStr ;
coherence
for b1 being non empty LattStr st b1 is Boolean holds
( b1 is bounded & b1 is complemented & b1 is distributive ) by Def20;
cluster non empty distributive bounded complemented -> non empty Boolean LattStr ;
coherence
for b1 being non empty LattStr st b1 is bounded & b1 is complemented & b1 is distributive holds
b1 is Boolean by Def20;
end;

registration
cluster strict distributive lower-bounded upper-bounded bounded complemented Boolean LattStr ;
existence
ex b1 being Lattice st
( b1 is Boolean & b1 is strict )
proof end;
end;

definition
mode B_Lattice is Boolean Lattice;
end;

theorem :: LATTICES:1  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
canceled;

theorem :: LATTICES:2  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
canceled;

theorem :: LATTICES:3  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
canceled;

theorem :: LATTICES:4  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
canceled;

theorem :: LATTICES:5  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
canceled;

theorem :: LATTICES:6  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
canceled;

theorem :: LATTICES:7  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
canceled;

theorem :: LATTICES:8  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
canceled;

theorem :: LATTICES:9  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
canceled;

theorem :: LATTICES:10  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
canceled;

theorem :: LATTICES:11  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
canceled;

theorem :: LATTICES:12  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
canceled;

theorem :: LATTICES:13  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
canceled;

theorem :: LATTICES:14  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
canceled;

theorem :: LATTICES:15  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
canceled;

theorem :: LATTICES:16  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
canceled;

theorem Th17: :: LATTICES:17  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for L being non empty meet-commutative meet-absorbing join-absorbing LattStr
for a being Element of L holds a "\/" a = a
proof end;

theorem :: LATTICES:18  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for L being non empty meet-commutative meet-absorbing join-absorbing LattStr
for a being Element of L holds a "/\" a = a
proof end;

theorem Th19: :: LATTICES:19  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for L being Lattice holds
( ( for a, b, c being Element of L holds a "/\" (b "\/" c) = (a "/\" b) "\/" (a "/\" c) ) iff for a, b, c being Element of L holds a "\/" (b "/\" c) = (a "\/" b) "/\" (a "\/" c) )
proof end;

theorem :: LATTICES:20  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
canceled;

theorem Th21: :: LATTICES:21  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for L being non empty meet-absorbing join-absorbing LattStr
for a, b being Element of L holds
( a [= b iff a "/\" b = a )
proof end;

theorem Th22: :: LATTICES:22  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for L being non empty join-associative meet-commutative meet-absorbing join-absorbing LattStr
for a, b being Element of L holds a [= a "\/" b
proof end;

theorem Th23: :: LATTICES:23  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for L being non empty meet-commutative meet-absorbing LattStr
for a, b being Element of L holds a "/\" b [= a
proof end;

definition
let L be non empty meet-commutative meet-absorbing join-absorbing LattStr ;
let a, b be Element of L;
:: original: [=
redefine pred a [= b;
reflexivity
for a being Element of L holds a [= a
proof end;
end;

theorem :: LATTICES:24  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
canceled;

theorem :: LATTICES:25  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for L being non empty join-associative \/-SemiLattStr
for a, b, c being Element of L st a [= b & b [= c holds
a [= c
proof end;

theorem Th26: :: LATTICES:26  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for L being non empty join-commutative \/-SemiLattStr
for a, b being Element of L st a [= b & b [= a holds
a = b
proof end;

theorem Th27: :: LATTICES:27  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for L being non empty meet-associative meet-absorbing join-absorbing LattStr
for a, b, c being Element of L st a [= b holds
a "/\" c [= b "/\" c
proof end;

theorem :: LATTICES:28  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
canceled;

theorem :: LATTICES:29  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for L being Lattice st ( for a, b, c being Element of L holds ((a "/\" b) "\/" (b "/\" c)) "\/" (c "/\" a) = ((a "\/" b) "/\" (b "\/" c)) "/\" (c "\/" a) ) holds
L is distributive
proof end;

theorem :: LATTICES:30  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
canceled;

theorem Th31: :: LATTICES:31  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for L being D_Lattice
for a, b, c being Element of L holds a "\/" (b "/\" c) = (a "\/" b) "/\" (a "\/" c)
proof end;

theorem Th32: :: LATTICES:32  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for L being D_Lattice
for c, a, b being Element of L st c "/\" a = c "/\" b & c "\/" a = c "\/" b holds
a = b
proof end;

theorem :: LATTICES:33  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
canceled;

theorem :: LATTICES:34  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for L being D_Lattice
for a, b, c being Element of L holds ((a "\/" b) "/\" (b "\/" c)) "/\" (c "\/" a) = ((a "/\" b) "\/" (b "/\" c)) "\/" (c "/\" a)
proof end;

registration
cluster distributive -> join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing modular LattStr ;
coherence
for b1 being Lattice st b1 is distributive holds
b1 is modular
proof end;
end;

theorem :: LATTICES:35  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
canceled;

theorem :: LATTICES:36  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
canceled;

theorem :: LATTICES:37  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
canceled;

theorem :: LATTICES:38  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
canceled;

theorem Th39: :: LATTICES:39  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for L being 0_Lattice
for a being Element of L holds (Bottom L) "\/" a = a
proof end;

theorem :: LATTICES:40  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for L being 0_Lattice
for a being Element of L holds (Bottom L) "/\" a = Bottom L by Def16;

theorem Th41: :: LATTICES:41  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for L being 0_Lattice
for a being Element of L holds Bottom L [= a
proof end;

theorem :: LATTICES:42  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
canceled;

theorem Th43: :: LATTICES:43  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for L being 1_Lattice
for a being Element of L holds (Top L) "/\" a = a
proof end;

theorem :: LATTICES:44  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for L being 1_Lattice
for a being Element of L holds (Top L) "\/" a = Top L by Def17;

theorem :: LATTICES:45  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for L being 1_Lattice
for a being Element of L holds a [= Top L
proof end;

definition
let L be non empty LattStr ;
let x be Element of L;
assume A1: L is complemented D_Lattice ;
func x ` -> Element of L means :Def21: :: LATTICES:def 21
it is_a_complement_of x;
existence
ex b1 being Element of L st b1 is_a_complement_of x by A1, Def19;
uniqueness
for b1, b2 being Element of L st b1 is_a_complement_of x & b2 is_a_complement_of x holds
b1 = b2
proof end;
end;

:: deftheorem Def21 defines ` LATTICES:def 21 :
for L being non empty LattStr
for x being Element of L st L is complemented D_Lattice holds
for b3 being Element of L holds
( b3 = x ` iff b3 is_a_complement_of x );

theorem :: LATTICES:46  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
canceled;

theorem Th47: :: LATTICES:47  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for L being B_Lattice
for a being Element of L holds (a ` ) "/\" a = Bottom L
proof end;

theorem Th48: :: LATTICES:48  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for L being B_Lattice
for a being Element of L holds (a ` ) "\/" a = Top L
proof end;

theorem Th49: :: LATTICES:49  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for L being B_Lattice
for a being Element of L holds (a ` ) ` = a
proof end;

theorem Th50: :: LATTICES:50  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for L being B_Lattice
for a, b being Element of L holds (a "/\" b) ` = (a ` ) "\/" (b ` )
proof end;

theorem :: LATTICES:51  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for L being B_Lattice
for a, b being Element of L holds (a "\/" b) ` = (a ` ) "/\" (b ` )
proof end;

theorem Th52: :: LATTICES:52  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for L being B_Lattice
for b, a being Element of L holds
( b "/\" a = Bottom L iff b [= a ` )
proof end;

theorem :: LATTICES:53  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for L being B_Lattice
for a, b being Element of L st a [= b holds
b ` [= a `
proof end;