:: Formalization of Quasilattices
:: by Dominik Kulesza and Adam Grabowski
::
:: Received May 31, 2020
:: Copyright (c) 2020-2021 Association of Mizar Users


definition
let L be non empty LattStr ;
attr L is satisfying_QLT1 means :: LATQUASI:def 1
for v0, v2, v1 being Element of L holds (v0 "/\" (v1 "\/" v2)) "\/" (v0 "/\" v1) = v0 "/\" (v1 "\/" v2);
attr L is satisfying_QLT2 means :: LATQUASI:def 2
for v0, v2, v1 being Element of L holds (v0 "\/" (v1 "/\" v2)) "/\" (v0 "\/" v1) = v0 "\/" (v1 "/\" v2);
attr L is QLT-distributive means :: LATQUASI:def 3
for v1, v2, v0 being Element of L holds v0 "/\" (v1 "\/" (v0 "/\" v2)) = v0 "/\" (v1 "\/" v2);
end;

:: deftheorem defines satisfying_QLT1 LATQUASI:def 1 :
for L being non empty LattStr holds
( L is satisfying_QLT1 iff for v0, v2, v1 being Element of L holds (v0 "/\" (v1 "\/" v2)) "\/" (v0 "/\" v1) = v0 "/\" (v1 "\/" v2) );

:: deftheorem defines satisfying_QLT2 LATQUASI:def 2 :
for L being non empty LattStr holds
( L is satisfying_QLT2 iff for v0, v2, v1 being Element of L holds (v0 "\/" (v1 "/\" v2)) "/\" (v0 "\/" v1) = v0 "\/" (v1 "/\" v2) );

:: deftheorem defines QLT-distributive LATQUASI:def 3 :
for L being non empty LattStr holds
( L is QLT-distributive iff for v1, v2, v0 being Element of L holds v0 "/\" (v1 "\/" (v0 "/\" v2)) = v0 "/\" (v1 "\/" v2) );

registration
cluster non empty trivial -> non empty satisfying_QLT1 satisfying_QLT2 QLT-distributive for LattStr ;
coherence
for b1 being non empty LattStr st b1 is trivial holds
( b1 is satisfying_QLT1 & b1 is satisfying_QLT2 & b1 is QLT-distributive )
by STRUCT_0:def 10;
end;

registration
cluster non empty trivial -> non empty join-idempotent meet-idempotent for LattStr ;
coherence
for b1 being non empty LattStr st b1 is trivial holds
( b1 is join-idempotent & b1 is meet-idempotent )
proof end;
end;

registration
cluster non empty join-commutative join-associative meet-commutative meet-associative join-idempotent meet-idempotent satisfying_QLT1 satisfying_QLT2 for LattStr ;
existence
ex b1 being non empty LattStr st
( b1 is join-commutative & b1 is join-associative & b1 is join-idempotent & b1 is meet-commutative & b1 is meet-associative & b1 is meet-idempotent & b1 is satisfying_QLT1 & b1 is satisfying_QLT2 )
proof end;
end;

definition
let L be non empty join-commutative LattStr ;
redefine attr L is satisfying_QLT1 means :: LATQUASI:def 4
for v0, v1, v2 being Element of L holds v0 "/\" v1 [= v0 "/\" (v1 "\/" v2);
compatibility
( L is satisfying_QLT1 iff for v0, v1, v2 being Element of L holds v0 "/\" v1 [= v0 "/\" (v1 "\/" v2) )
proof end;
end;

:: deftheorem defines satisfying_QLT1 LATQUASI:def 4 :
for L being non empty join-commutative LattStr holds
( L is satisfying_QLT1 iff for v0, v1, v2 being Element of L holds v0 "/\" v1 [= v0 "/\" (v1 "\/" v2) );

registration
cluster {0,1,2} -> real-membered ;
coherence
{0,1,2} is real-membered
;
end;

registration
cluster -> real for Element of {0,1,2};
coherence
for b1 being Element of {0,1,2} holds b1 is real
;
end;

T2: for x, y being Element of {0,1,2} holds min (x,y) in {0,1,2}
proof end;

definition
let x, y be Element of {0,1,2};
func OpEx2 (x,y) -> Element of {0,1,2} equals :OpEx2Def: :: LATQUASI:def 5
1 if ( x = 1 or y = 1 )
min (x,y) if ( x <> 1 & y <> 1 )
;
coherence
( ( ( x = 1 or y = 1 ) implies 1 is Element of {0,1,2} ) & ( x <> 1 & y <> 1 implies min (x,y) is Element of {0,1,2} ) )
by T2;
consistency
for b1 being Element of {0,1,2} st ( x = 1 or y = 1 ) & x <> 1 & y <> 1 holds
( b1 = 1 iff b1 = min (x,y) )
;
end;

:: deftheorem OpEx2Def defines OpEx2 LATQUASI:def 5 :
for x, y being Element of {0,1,2} holds
( ( ( x = 1 or y = 1 ) implies OpEx2 (x,y) = 1 ) & ( x <> 1 & y <> 1 implies OpEx2 (x,y) = min (x,y) ) );

definition
func QLT_Ex1 -> BinOp of {0,1,2} means :QLTEx1Def: :: LATQUASI:def 6
for x, y being Element of {0,1,2} holds
( ( x = y implies it . (x,y) = x ) & ( x <> y implies it . (x,y) = 0 ) );
existence
ex b1 being BinOp of {0,1,2} st
for x, y being Element of {0,1,2} holds
( ( x = y implies b1 . (x,y) = x ) & ( x <> y implies b1 . (x,y) = 0 ) )
proof end;
uniqueness
for b1, b2 being BinOp of {0,1,2} st ( for x, y being Element of {0,1,2} holds
( ( x = y implies b1 . (x,y) = x ) & ( x <> y implies b1 . (x,y) = 0 ) ) ) & ( for x, y being Element of {0,1,2} holds
( ( x = y implies b2 . (x,y) = x ) & ( x <> y implies b2 . (x,y) = 0 ) ) ) holds
b1 = b2
proof end;
func QLT_Ex2 -> BinOp of {0,1,2} means :QLTEx2Def: :: LATQUASI:def 7
for x, y being Element of {0,1,2} holds
( ( ( x = 1 or y = 1 ) implies it . (x,y) = 1 ) & ( x <> 1 & y <> 1 implies it . (x,y) = min (x,y) ) );
existence
ex b1 being BinOp of {0,1,2} st
for x, y being Element of {0,1,2} holds
( ( ( x = 1 or y = 1 ) implies b1 . (x,y) = 1 ) & ( x <> 1 & y <> 1 implies b1 . (x,y) = min (x,y) ) )
proof end;
uniqueness
for b1, b2 being BinOp of {0,1,2} st ( for x, y being Element of {0,1,2} holds
( ( ( x = 1 or y = 1 ) implies b1 . (x,y) = 1 ) & ( x <> 1 & y <> 1 implies b1 . (x,y) = min (x,y) ) ) ) & ( for x, y being Element of {0,1,2} holds
( ( ( x = 1 or y = 1 ) implies b2 . (x,y) = 1 ) & ( x <> 1 & y <> 1 implies b2 . (x,y) = min (x,y) ) ) ) holds
b1 = b2
proof end;
end;

:: deftheorem QLTEx1Def defines QLT_Ex1 LATQUASI:def 6 :
for b1 being BinOp of {0,1,2} holds
( b1 = QLT_Ex1 iff for x, y being Element of {0,1,2} holds
( ( x = y implies b1 . (x,y) = x ) & ( x <> y implies b1 . (x,y) = 0 ) ) );

:: deftheorem QLTEx2Def defines QLT_Ex2 LATQUASI:def 7 :
for b1 being BinOp of {0,1,2} holds
( b1 = QLT_Ex2 iff for x, y being Element of {0,1,2} holds
( ( ( x = 1 or y = 1 ) implies b1 . (x,y) = 1 ) & ( x <> 1 & y <> 1 implies b1 . (x,y) = min (x,y) ) ) );

theorem WazneQLT7: :: LATQUASI:1
QLT_Ex1 <> QLT_Ex2
proof end;

::: Construction of quasi-lattices needed to prove QLT-7
:: x <= y iff x "\/" y = y
::: if absorption is true, then x <= y iff x "/\" y = x
definition
func QLTLattice1 -> non empty strict LattStr equals :: LATQUASI:def 8
LattStr(# {0,1,2},QLT_Ex1,QLT_Ex1 #);
coherence
LattStr(# {0,1,2},QLT_Ex1,QLT_Ex1 #) is non empty strict LattStr
;
func QLTLattice2 -> non empty strict LattStr equals :: LATQUASI:def 9
LattStr(# {0,1,2},QLT_Ex1,QLT_Ex2 #);
coherence
LattStr(# {0,1,2},QLT_Ex1,QLT_Ex2 #) is non empty strict LattStr
;
end;

:: deftheorem defines QLTLattice1 LATQUASI:def 8 :
QLTLattice1 = LattStr(# {0,1,2},QLT_Ex1,QLT_Ex1 #);

:: deftheorem defines QLTLattice2 LATQUASI:def 9 :
QLTLattice2 = LattStr(# {0,1,2},QLT_Ex1,QLT_Ex2 #);

registration
cluster QLT_Ex1 -> commutative associative idempotent ;
coherence
( QLT_Ex1 is commutative & QLT_Ex1 is associative & QLT_Ex1 is idempotent )
proof end;
end;

registration
cluster QLT_Ex2 -> commutative associative idempotent ;
coherence
( QLT_Ex2 is commutative & QLT_Ex2 is associative & QLT_Ex2 is idempotent )
proof end;
end;

registration
cluster QLTLattice1 -> non empty strict join-commutative join-associative join-idempotent ;
coherence
( QLTLattice1 is join-commutative & QLTLattice1 is join-associative & QLTLattice1 is join-idempotent )
proof end;
end;

registration
cluster QLTLattice1 -> non empty strict meet-commutative meet-associative meet-idempotent ;
coherence
( QLTLattice1 is meet-commutative & QLTLattice1 is meet-associative & QLTLattice1 is meet-idempotent )
proof end;
end;

theorem Lemacik00: :: LATQUASI:2
for v0, v1 being Element of QLTLattice1 st v1 = 0 holds
v0 "/\" v1 = v1
proof end;

theorem Lemacik001: :: LATQUASI:3
for v0, v1 being Element of QLTLattice1 st v1 = 0 holds
v0 "\/" v1 = v1
proof end;

registration
cluster QLTLattice1 -> non empty strict satisfying_QLT1 ;
coherence
QLTLattice1 is satisfying_QLT1
proof end;
end;

registration
cluster QLTLattice1 -> non empty strict satisfying_QLT2 ;
coherence
QLTLattice1 is satisfying_QLT2
proof end;
end;

:: Every QLTLattice is QuasiLattice
registration
cluster -> real for Element of the carrier of QLTLattice2;
coherence
for b1 being Element of QLTLattice2 holds b1 is real
;
end;

registration
cluster QLTLattice2 -> non empty strict join-commutative join-associative join-idempotent ;
coherence
( QLTLattice2 is join-commutative & QLTLattice2 is join-associative & QLTLattice2 is join-idempotent )
proof end;
end;

registration
cluster QLTLattice2 -> non empty strict meet-commutative meet-associative meet-idempotent ;
coherence
( QLTLattice2 is meet-commutative & QLTLattice2 is meet-associative & QLTLattice2 is meet-idempotent )
proof end;
end;

registration
cluster QLTLattice2 -> non empty strict satisfying_QLT1 ;
coherence
QLTLattice2 is satisfying_QLT1
proof end;
end;

registration
cluster QLTLattice2 -> non empty strict satisfying_QLT2 ;
coherence
QLTLattice2 is satisfying_QLT2
proof end;
end;

registration
cluster QLTLattice2 -> non empty strict non join-absorbing ;
coherence
not QLTLattice2 is join-absorbing
proof end;
cluster QLTLattice2 -> non empty strict non meet-absorbing ;
coherence
not QLTLattice2 is meet-absorbing
proof end;
end;

registration
cluster QLTLattice1 -> non empty strict non join-absorbing ;
coherence
not QLTLattice1 is join-absorbing
proof end;
cluster QLTLattice1 -> non empty strict non meet-absorbing ;
coherence
not QLTLattice1 is meet-absorbing
proof end;
end;

definition
mode QuasiLattice is non empty join-commutative join-associative meet-commutative meet-associative join-idempotent meet-idempotent satisfying_QLT1 satisfying_QLT2 LattStr ;
end;

:: In QLT-1 we don't need two QLT axioms:
:: for v0 holds v0"/\"v0 = v0 & :: /\-idempotent
:: (for v2,v1,v0 holds
:: (v0"/\"v1)"/\"v2 = v0"/\"(v1"/\"v2)) & :: /\-associative
theorem Lemma1: :: LATQUASI:4
for L being non empty LattStr st ( for v1, v0 being Element of L holds v0 "/\" v1 = v1 "/\" v0 ) & ( for v0, v2, v1 being Element of L holds (v0 "/\" (v1 "\/" v2)) "\/" (v0 "/\" v1) = v0 "/\" (v1 "\/" v2) ) & ( for v0 being Element of L holds v0 "\/" v0 = v0 ) & ( for v2, v1, v0 being Element of L holds (v0 "\/" v1) "\/" v2 = v0 "\/" (v1 "\/" v2) ) & ( for v1, v0 being Element of L holds v0 "\/" v1 = v1 "\/" v0 ) & ( for v0, v2, v1 being Element of L holds (v0 "\/" (v1 "/\" v2)) "/\" (v0 "\/" v1) = v0 "\/" (v1 "/\" v2) ) & ( for v1, v2, v0 being Element of L holds v0 "/\" (v1 "\/" (v0 "/\" v2)) = v0 "/\" (v1 "\/" v2) ) holds
for v1, v2, v3 being Element of L holds (v1 "/\" v2) "\/" (v1 "/\" v3) = v1 "/\" (v2 "\/" v3)
proof end;

theorem Cluster1: :: LATQUASI:5
for L being non empty LattStr st L is meet-commutative & L is satisfying_QLT1 & L is join-idempotent & L is join-associative & L is join-commutative & L is satisfying_QLT2 & L is QLT-distributive holds
L is distributive
proof end;

registration
cluster non empty join-commutative join-associative meet-commutative join-idempotent satisfying_QLT1 satisfying_QLT2 QLT-distributive -> non empty distributive for LattStr ;
coherence
for b1 being non empty LattStr st b1 is meet-commutative & b1 is satisfying_QLT1 & b1 is join-idempotent & b1 is join-associative & b1 is join-commutative & b1 is satisfying_QLT2 & b1 is QLT-distributive holds
b1 is distributive
by Cluster1;
end;

theorem ThQLT2: :: LATQUASI:6
for L being non empty LattStr st ( for v0 being Element of L holds v0 "/\" v0 = v0 ) & ( for v2, v1, v0 being Element of L holds (v0 "/\" v1) "/\" v2 = v0 "/\" (v1 "/\" v2) ) & ( for v1, v0 being Element of L holds v0 "/\" v1 = v1 "/\" v0 ) & ( for v0 being Element of L holds v0 "\/" v0 = v0 ) & ( for v2, v1, v0 being Element of L holds (v0 "\/" v1) "\/" v2 = v0 "\/" (v1 "\/" v2) ) & ( for v0, v2, v1 being Element of L holds (v0 "\/" (v1 "/\" v2)) "/\" (v0 "\/" v1) = v0 "\/" (v1 "/\" v2) ) & ( for v0, v2, v1 being Element of L holds v0 "/\" (v1 "\/" v2) = (v0 "/\" v1) "\/" (v0 "/\" v2) ) holds
for v1, v2, v3 being Element of L holds v1 "\/" (v2 "/\" v3) = (v1 "\/" v2) "/\" (v1 "\/" v3)
proof end;

theorem Cluster2: :: LATQUASI:7
for L being non empty LattStr st L is meet-idempotent & L is meet-associative & L is meet-commutative & L is join-idempotent & L is join-associative & L is satisfying_QLT2 & L is distributive holds
L is distributive'
proof end;

registration
cluster non empty join-associative meet-commutative meet-associative distributive join-idempotent meet-idempotent satisfying_QLT2 -> non empty distributive' for LattStr ;
coherence
for b1 being non empty LattStr st b1 is meet-idempotent & b1 is meet-associative & b1 is meet-commutative & b1 is join-idempotent & b1 is join-associative & b1 is satisfying_QLT2 & b1 is distributive holds
b1 is distributive'
by Cluster2;
end;

definition
let L be non empty LattStr ;
attr L is QLT-selfdistributive means :: LATQUASI:def 10
for v2, v1, v0 being Element of L holds (((v0 "/\" v1) "\/" v2) "/\" v1) "\/" (v2 "/\" v0) = (((v0 "\/" v1) "/\" v2) "\/" v1) "/\" (v2 "\/" v0);
end;

:: deftheorem defines QLT-selfdistributive LATQUASI:def 10 :
for L being non empty LattStr holds
( L is QLT-selfdistributive iff for v2, v1, v0 being Element of L holds (((v0 "/\" v1) "\/" v2) "/\" v1) "\/" (v2 "/\" v0) = (((v0 "\/" v1) "/\" v2) "\/" v1) "/\" (v2 "\/" v0) );

theorem ThQLT3: :: LATQUASI:8
for L being non empty LattStr st ( for v0 being Element of L holds v0 "/\" v0 = v0 ) & ( for v2, v1, v0 being Element of L holds (v0 "/\" v1) "/\" v2 = v0 "/\" (v1 "/\" v2) ) & ( for v1, v0 being Element of L holds v0 "/\" v1 = v1 "/\" v0 ) & ( for v0, v2, v1 being Element of L holds (v0 "/\" (v1 "\/" v2)) "\/" (v0 "/\" v1) = v0 "/\" (v1 "\/" v2) ) & ( for v0 being Element of L holds v0 "\/" v0 = v0 ) & ( for v2, v1, v0 being Element of L holds (v0 "\/" v1) "\/" v2 = v0 "\/" (v1 "\/" v2) ) & ( for v1, v0 being Element of L holds v0 "\/" v1 = v1 "\/" v0 ) & ( for v0, v2, v1 being Element of L holds (v0 "\/" (v1 "/\" v2)) "/\" (v0 "\/" v1) = v0 "\/" (v1 "/\" v2) ) & ( for v2, v1, v0 being Element of L holds (((v0 "/\" v1) "\/" v2) "/\" v1) "\/" (v2 "/\" v0) = (((v0 "\/" v1) "/\" v2) "\/" v1) "/\" (v2 "\/" v0) ) holds
for v1, v2, v3 being Element of L holds v1 "\/" (v2 "/\" v3) = (v1 "\/" v2) "/\" (v1 "\/" v3)
proof end;

Cluster3: for L being non empty LattStr st L is meet-idempotent & L is meet-associative & L is meet-commutative & L is satisfying_QLT1 & L is join-idempotent & L is join-associative & L is join-commutative & L is satisfying_QLT2 & L is QLT-selfdistributive holds
L is distributive'

proof end;

registration
cluster non empty join-commutative join-associative meet-commutative meet-associative join-idempotent meet-idempotent satisfying_QLT1 satisfying_QLT2 QLT-selfdistributive -> non empty distributive' for LattStr ;
coherence
for b1 being non empty LattStr st b1 is meet-idempotent & b1 is meet-associative & b1 is meet-commutative & b1 is satisfying_QLT1 & b1 is join-idempotent & b1 is join-associative & b1 is join-commutative & b1 is satisfying_QLT2 & b1 is QLT-selfdistributive holds
b1 is distributive'
by Cluster3;
end;

definition
let L be non empty LattStr ;
attr L is satisfying_Bowden_inequality means :: LATQUASI:def 11
for x, y, z being Element of L holds (x "\/" y) "/\" z [= x "\/" (y "/\" z);
end;

:: deftheorem defines satisfying_Bowden_inequality LATQUASI:def 11 :
for L being non empty LattStr holds
( L is satisfying_Bowden_inequality iff for x, y, z being Element of L holds (x "\/" y) "/\" z [= x "\/" (y "/\" z) );

definition
let L be non empty join-commutative LattStr ;
redefine attr L is satisfying_Bowden_inequality means :BowdenRedef: :: LATQUASI:def 12
for v0, v2, v1 being Element of L holds (v0 "\/" (v1 "/\" v2)) "\/" ((v0 "\/" v1) "/\" v2) = v0 "\/" (v1 "/\" v2);
compatibility
( L is satisfying_Bowden_inequality iff for v0, v2, v1 being Element of L holds (v0 "\/" (v1 "/\" v2)) "\/" ((v0 "\/" v1) "/\" v2) = v0 "\/" (v1 "/\" v2) )
proof end;
end;

:: deftheorem BowdenRedef defines satisfying_Bowden_inequality LATQUASI:def 12 :
for L being non empty join-commutative LattStr holds
( L is satisfying_Bowden_inequality iff for v0, v2, v1 being Element of L holds (v0 "\/" (v1 "/\" v2)) "\/" ((v0 "\/" v1) "/\" v2) = v0 "\/" (v1 "/\" v2) );

theorem ThQLT4: :: LATQUASI:9
for L being non empty LattStr st ( for v0 being Element of L holds v0 "/\" v0 = v0 ) & ( for v1, v0 being Element of L holds v0 "/\" v1 = v1 "/\" v0 ) & ( for v0, v2, v1 being Element of L holds (v0 "/\" (v1 "\/" v2)) "\/" (v0 "/\" v1) = v0 "/\" (v1 "\/" v2) ) & ( for v0 being Element of L holds v0 "\/" v0 = v0 ) & ( for v2, v1, v0 being Element of L holds (v0 "\/" v1) "\/" v2 = v0 "\/" (v1 "\/" v2) ) & ( for v1, v0 being Element of L holds v0 "\/" v1 = v1 "\/" v0 ) & ( for v0, v2, v1 being Element of L holds (v0 "\/" (v1 "/\" v2)) "/\" (v0 "\/" v1) = v0 "\/" (v1 "/\" v2) ) & ( for v0, v2, v1 being Element of L holds (v0 "\/" (v1 "/\" v2)) "\/" ((v0 "\/" v1) "/\" v2) = v0 "\/" (v1 "/\" v2) ) holds
for v1, v2, v3 being Element of L holds v1 "\/" (v2 "/\" v3) = (v1 "\/" v2) "/\" (v1 "\/" v3)
proof end;

Cluster4: for L being non empty LattStr st L is meet-idempotent & L is meet-associative & L is meet-commutative & L is satisfying_QLT1 & L is join-idempotent & L is join-associative & L is join-commutative & L is satisfying_QLT2 & L is satisfying_Bowden_inequality holds
L is distributive'

proof end;

registration
cluster non empty join-commutative join-associative meet-commutative meet-associative join-idempotent meet-idempotent satisfying_QLT1 satisfying_QLT2 satisfying_Bowden_inequality -> non empty distributive' for LattStr ;
coherence
for b1 being non empty LattStr st b1 is meet-idempotent & b1 is meet-associative & b1 is meet-commutative & b1 is satisfying_QLT1 & b1 is join-idempotent & b1 is join-associative & b1 is join-commutative & b1 is satisfying_QLT2 & b1 is satisfying_Bowden_inequality holds
b1 is distributive'
by Cluster4;
end;

definition
let L be non empty LattStr ;
attr L is QLT-selfmodular means :: LATQUASI:def 13
for v2, v1, v0 being Element of L holds (v0 "/\" v1) "\/" (v2 "/\" (v0 "\/" v1)) = (v0 "\/" v1) "/\" (v2 "\/" (v0 "/\" v1));
end;

:: deftheorem defines QLT-selfmodular LATQUASI:def 13 :
for L being non empty LattStr holds
( L is QLT-selfmodular iff for v2, v1, v0 being Element of L holds (v0 "/\" v1) "\/" (v2 "/\" (v0 "\/" v1)) = (v0 "\/" v1) "/\" (v2 "\/" (v0 "/\" v1)) );

definition
let L be non empty join-idempotent LattStr ;
let a, b be Element of L;
:: original: [=
redefine pred a [= b;
reflexivity
for a being Element of L holds R29(L,b1,b1)
proof end;
end;

:: Modularity for Quasilattices
theorem QLTMod: :: LATQUASI:10
for L being non empty LattStr st ( for v0 being Element of L holds v0 "/\" v0 = v0 ) & ( for v2, v1, v0 being Element of L holds (v0 "/\" v1) "/\" v2 = v0 "/\" (v1 "/\" v2) ) & ( for v1, v0 being Element of L holds v0 "/\" v1 = v1 "/\" v0 ) & ( for v0, v2, v1 being Element of L holds (v0 "/\" (v1 "\/" v2)) "\/" (v0 "/\" v1) = v0 "/\" (v1 "\/" v2) ) & ( for v0 being Element of L holds v0 "\/" v0 = v0 ) & ( for v2, v1, v0 being Element of L holds (v0 "\/" v1) "\/" v2 = v0 "\/" (v1 "\/" v2) ) & ( for v1, v0 being Element of L holds v0 "\/" v1 = v1 "\/" v0 ) & ( for v0, v2, v1 being Element of L holds (v0 "\/" (v1 "/\" v2)) "/\" (v0 "\/" v1) = v0 "\/" (v1 "/\" v2) ) & ( for v0, v1, v2 being Element of L st v0 "\/" v1 = v1 holds
v0 "\/" (v2 "/\" v1) = (v0 "\/" v2) "/\" v1 ) holds
for v1, v2, v3 being Element of L holds (v1 "/\" v2) "\/" (v1 "/\" v3) = v1 "/\" (v2 "\/" (v1 "/\" v3))
proof end;

ClusterA: for L being non empty LattStr st L is meet-idempotent & L is join-idempotent & L is meet-commutative & L is join-commutative & L is meet-associative & L is join-associative & L is satisfying_QLT1 & L is satisfying_QLT2 & L is modular holds
for v1, v2, v3 being Element of L holds (v1 "/\" v2) "\/" (v1 "/\" v3) = v1 "/\" (v2 "\/" (v1 "/\" v3))

proof end;

theorem QLTMod2: :: LATQUASI:11
for L being non empty LattStr st ( for v1, v0 being Element of L holds v0 "/\" v1 = v1 "/\" v0 ) & ( for v0, v2, v1 being Element of L holds (v0 "/\" (v1 "\/" v2)) "\/" (v0 "/\" v1) = v0 "/\" (v1 "\/" v2) ) & ( for v0 being Element of L holds v0 "\/" v0 = v0 ) & ( for v2, v1, v0 being Element of L holds (v0 "\/" v1) "\/" v2 = v0 "\/" (v1 "\/" v2) ) & ( for v1, v0 being Element of L holds v0 "\/" v1 = v1 "\/" v0 ) & ( for v0, v2, v1 being Element of L holds (v0 "\/" (v1 "/\" v2)) "/\" (v0 "\/" v1) = v0 "\/" (v1 "/\" v2) ) & ( for v2, v1, v0 being Element of L holds (v0 "/\" v1) "\/" (v0 "/\" v2) = v0 "/\" (v1 "\/" (v0 "/\" v2)) ) holds
for v1, v2, v3 being Element of L st v1 "\/" v2 = v2 holds
v1 "\/" (v3 "/\" v2) = (v1 "\/" v3) "/\" v2
proof end;

ClusterB: for L being non empty LattStr st L is meet-idempotent & L is join-idempotent & L is meet-commutative & L is join-commutative & L is meet-associative & L is join-associative & L is satisfying_QLT1 & L is satisfying_QLT2 & ( for v2, v1, v0 being Element of L holds (v0 "/\" v1) "\/" (v0 "/\" v2) = v0 "/\" (v1 "\/" (v0 "/\" v2)) ) holds
L is modular

proof end;

definition
let L be non empty join-commutative join-associative meet-commutative meet-associative join-idempotent meet-idempotent satisfying_QLT1 satisfying_QLT2 LattStr ;
redefine attr L is modular means :ModRedef: :: LATQUASI:def 14
for v1, v2, v3 being Element of L holds (v1 "/\" v2) "\/" (v1 "/\" v3) = v1 "/\" (v2 "\/" (v1 "/\" v3));
compatibility
( L is modular iff for v1, v2, v3 being Element of L holds (v1 "/\" v2) "\/" (v1 "/\" v3) = v1 "/\" (v2 "\/" (v1 "/\" v3)) )
proof end;
end;

:: deftheorem ModRedef defines modular LATQUASI:def 14 :
for L being non empty join-commutative join-associative meet-commutative meet-associative join-idempotent meet-idempotent satisfying_QLT1 satisfying_QLT2 LattStr holds
( L is modular iff for v1, v2, v3 being Element of L holds (v1 "/\" v2) "\/" (v1 "/\" v3) = v1 "/\" (v2 "\/" (v1 "/\" v3)) );

theorem ThQLT5: :: LATQUASI:12
for L being non empty LattStr st ( for v0 being Element of L holds v0 "/\" v0 = v0 ) & ( for v2, v1, v0 being Element of L holds (v0 "/\" v1) "/\" v2 = v0 "/\" (v1 "/\" v2) ) & ( for v1, v0 being Element of L holds v0 "/\" v1 = v1 "/\" v0 ) & ( for v0, v2, v1 being Element of L holds (v0 "/\" (v1 "\/" v2)) "\/" (v0 "/\" v1) = v0 "/\" (v1 "\/" v2) ) & ( for v0 being Element of L holds v0 "\/" v0 = v0 ) & ( for v2, v1, v0 being Element of L holds (v0 "\/" v1) "\/" v2 = v0 "\/" (v1 "\/" v2) ) & ( for v1, v0 being Element of L holds v0 "\/" v1 = v1 "\/" v0 ) & ( for v0, v2, v1 being Element of L holds (v0 "\/" (v1 "/\" v2)) "/\" (v0 "\/" v1) = v0 "\/" (v1 "/\" v2) ) & ( for v2, v1, v0 being Element of L holds (v0 "/\" v1) "\/" (v2 "/\" (v0 "\/" v1)) = (v0 "\/" v1) "/\" (v2 "\/" (v0 "/\" v1)) ) holds
for v1, v2, v3 being Element of L holds (v1 "/\" v2) "\/" (v1 "/\" v3) = v1 "/\" (v2 "\/" (v1 "/\" v3))
proof end;

Cluster5: for L being non empty LattStr st L is meet-idempotent & L is meet-associative & L is meet-commutative & L is satisfying_QLT1 & L is join-idempotent & L is join-associative & L is join-commutative & L is satisfying_QLT2 & L is QLT-selfmodular holds
L is modular

proof end;

registration
cluster non empty join-commutative join-associative meet-commutative meet-associative join-idempotent meet-idempotent satisfying_QLT1 satisfying_QLT2 QLT-selfmodular -> non empty modular for LattStr ;
coherence
for b1 being non empty LattStr st b1 is meet-idempotent & b1 is meet-associative & b1 is meet-commutative & b1 is satisfying_QLT1 & b1 is join-idempotent & b1 is join-associative & b1 is join-commutative & b1 is satisfying_QLT2 & b1 is QLT-selfmodular holds
b1 is modular
by Cluster5;
end;

theorem ThQLT6: :: LATQUASI:13
for L being non empty LattStr st ( for v0 being Element of L holds v0 "/\" v0 = v0 ) & ( for v2, v1, v0 being Element of L holds (v0 "/\" v1) "/\" v2 = v0 "/\" (v1 "/\" v2) ) & ( for v1, v0 being Element of L holds v0 "/\" v1 = v1 "/\" v0 ) & ( for v0, v2, v1 being Element of L holds (v0 "/\" (v1 "\/" v2)) "\/" (v0 "/\" v1) = v0 "/\" (v1 "\/" v2) ) & ( for v0 being Element of L holds v0 "\/" v0 = v0 ) & ( for v2, v1, v0 being Element of L holds (v0 "\/" v1) "\/" v2 = v0 "\/" (v1 "\/" v2) ) & ( for v1, v0 being Element of L holds v0 "\/" v1 = v1 "\/" v0 ) & ( for v0, v2, v1 being Element of L holds (v0 "\/" (v1 "/\" v2)) "/\" (v0 "\/" v1) = v0 "\/" (v1 "/\" v2) ) & ( for v2, v1, v0 being Element of L holds ((v0 "\/" v1) "/\" v2) "\/" v1 = ((v2 "\/" v1) "/\" v0) "\/" v1 ) holds
for v1, v2, v3 being Element of L holds (v1 "/\" v2) "\/" (v1 "/\" v3) = v1 "/\" (v2 "\/" (v1 "/\" v3))
proof end;

definition
let L be non empty LattStr ;
attr L is QLT-selfmodular' means :: LATQUASI:def 15
for v2, v1, v0 being Element of L holds ((v0 "\/" v1) "/\" v2) "\/" v1 = ((v2 "\/" v1) "/\" v0) "\/" v1;
end;

:: deftheorem defines QLT-selfmodular' LATQUASI:def 15 :
for L being non empty LattStr holds
( L is QLT-selfmodular' iff for v2, v1, v0 being Element of L holds ((v0 "\/" v1) "/\" v2) "\/" v1 = ((v2 "\/" v1) "/\" v0) "\/" v1 );

Cluster6: for L being non empty LattStr st L is meet-idempotent & L is meet-associative & L is meet-commutative & L is satisfying_QLT1 & L is join-idempotent & L is join-associative & L is join-commutative & L is satisfying_QLT2 & L is QLT-selfmodular' holds
L is modular

proof end;

registration
cluster non empty join-commutative join-associative meet-commutative meet-associative join-idempotent meet-idempotent satisfying_QLT1 satisfying_QLT2 QLT-selfmodular' -> non empty modular for LattStr ;
coherence
for b1 being non empty LattStr st b1 is meet-idempotent & b1 is meet-associative & b1 is meet-commutative & b1 is satisfying_QLT1 & b1 is join-idempotent & b1 is join-associative & b1 is join-commutative & b1 is satisfying_QLT2 & b1 is QLT-selfmodular' holds
b1 is modular
by Cluster6;
end;

theorem :: LATQUASI:14
ex L1, L2 being QuasiLattice st
( the carrier of L1 = the carrier of L2 & the L_join of L1 = the L_join of L2 & the L_meet of L1 <> the L_meet of L2 )
proof end;