:: NAT_LAT semantic presentation

REAL is complex-membered ext-real-membered real-membered V49() set
NAT is non empty epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V49() Element of bool REAL
bool REAL is set
COMPLEX is complex-membered V49() set
NAT is non empty epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V49() set
bool NAT is set
{} is set
the empty V24() V28() ext-real epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V39() real complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V49() set is empty V24() V28() ext-real epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V39() real complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V49() set
1 is non empty ext-real positive epsilon-transitive epsilon-connected ordinal natural V39() real V41() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
0 is ext-real epsilon-transitive epsilon-connected ordinal natural V39() real V41() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
[:NAT,NAT:] is set
[:[:NAT,NAT:],NAT:] is set
bool [:[:NAT,NAT:],NAT:] is set
x is Relation-like [:NAT,NAT:] -defined NAT -valued Function-like V18([:NAT,NAT:], NAT ) Element of bool [:[:NAT,NAT:],NAT:]
y1 is ext-real epsilon-transitive epsilon-connected ordinal natural V39() real set
y2 is ext-real epsilon-transitive epsilon-connected ordinal natural V39() real set
x . (y1,y2) is set
[y1,y2] is set
{y1,y2} is V24() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered set
{y1} is V24() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered set
{{y1,y2},{y1}} is V24() V28() set
x . [y1,y2] is set
y1 gcd y2 is ext-real epsilon-transitive epsilon-connected ordinal natural V39() real V41() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
x is Relation-like [:NAT,NAT:] -defined NAT -valued Function-like V18([:NAT,NAT:], NAT ) Element of bool [:[:NAT,NAT:],NAT:]
y1 is Relation-like [:NAT,NAT:] -defined NAT -valued Function-like V18([:NAT,NAT:], NAT ) Element of bool [:[:NAT,NAT:],NAT:]
y2 is ext-real epsilon-transitive epsilon-connected ordinal natural V39() real V41() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
n is ext-real epsilon-transitive epsilon-connected ordinal natural V39() real V41() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
x . (y2,n) is ext-real epsilon-transitive epsilon-connected ordinal natural V39() real V41() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
[y2,n] is set
{y2,n} is V24() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered set
{y2} is V24() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered set
{{y2,n},{y2}} is V24() V28() set
x . [y2,n] is set
y2 gcd n is ext-real epsilon-transitive epsilon-connected ordinal natural V39() real V41() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
y1 . (y2,n) is ext-real epsilon-transitive epsilon-connected ordinal natural V39() real V41() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
y1 . [y2,n] is set
x is Relation-like [:NAT,NAT:] -defined NAT -valued Function-like V18([:NAT,NAT:], NAT ) Element of bool [:[:NAT,NAT:],NAT:]
y1 is ext-real epsilon-transitive epsilon-connected ordinal natural V39() real set
y2 is ext-real epsilon-transitive epsilon-connected ordinal natural V39() real set
x . (y1,y2) is set
[y1,y2] is set
{y1,y2} is V24() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered set
{y1} is V24() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered set
{{y1,y2},{y1}} is V24() V28() set
x . [y1,y2] is set
y1 lcm y2 is ext-real epsilon-transitive epsilon-connected ordinal natural V39() real V41() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
x is Relation-like [:NAT,NAT:] -defined NAT -valued Function-like V18([:NAT,NAT:], NAT ) Element of bool [:[:NAT,NAT:],NAT:]
y1 is Relation-like [:NAT,NAT:] -defined NAT -valued Function-like V18([:NAT,NAT:], NAT ) Element of bool [:[:NAT,NAT:],NAT:]
y2 is ext-real epsilon-transitive epsilon-connected ordinal natural V39() real V41() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
n is ext-real epsilon-transitive epsilon-connected ordinal natural V39() real V41() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
x . (y2,n) is ext-real epsilon-transitive epsilon-connected ordinal natural V39() real V41() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
[y2,n] is set
{y2,n} is V24() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered set
{y2} is V24() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered set
{{y2,n},{y2}} is V24() V28() set
x . [y2,n] is set
y2 lcm n is ext-real epsilon-transitive epsilon-connected ordinal natural V39() real V41() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
y1 . (y2,n) is ext-real epsilon-transitive epsilon-connected ordinal natural V39() real V41() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
y1 . [y2,n] is set
() is Relation-like [:NAT,NAT:] -defined NAT -valued Function-like V18([:NAT,NAT:], NAT ) Element of bool [:[:NAT,NAT:],NAT:]
() is Relation-like [:NAT,NAT:] -defined NAT -valued Function-like V18([:NAT,NAT:], NAT ) Element of bool [:[:NAT,NAT:],NAT:]
LattStr(# NAT,(),() #) is non empty strict LattStr
() is non empty strict LattStr
the carrier of () is non empty set
x is ext-real epsilon-transitive epsilon-connected ordinal natural V39() real V41() Element of the carrier of ()
y1 is ext-real epsilon-transitive epsilon-connected ordinal natural V39() real V41() Element of the carrier of ()
x "\/" y1 is ext-real epsilon-transitive epsilon-connected ordinal natural V39() real V41() Element of the carrier of ()
the L_join of () is Relation-like [: the carrier of (), the carrier of ():] -defined the carrier of () -valued Function-like V18([: the carrier of (), the carrier of ():], the carrier of ()) Element of bool [:[: the carrier of (), the carrier of ():], the carrier of ():]
[: the carrier of (), the carrier of ():] is set
[:[: the carrier of (), the carrier of ():], the carrier of ():] is set
bool [:[: the carrier of (), the carrier of ():], the carrier of ():] is set
the L_join of () . (x,y1) is ext-real epsilon-transitive epsilon-connected ordinal natural V39() real V41() Element of the carrier of ()
[x,y1] is set
{x,y1} is V24() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered set
{x} is V24() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered set
{{x,y1},{x}} is V24() V28() set
the L_join of () . [x,y1] is set
x lcm y1 is ext-real epsilon-transitive epsilon-connected ordinal natural V39() real V41() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
x "/\" y1 is ext-real epsilon-transitive epsilon-connected ordinal natural V39() real V41() Element of the carrier of ()
the L_meet of () is Relation-like [: the carrier of (), the carrier of ():] -defined the carrier of () -valued Function-like V18([: the carrier of (), the carrier of ():], the carrier of ()) Element of bool [:[: the carrier of (), the carrier of ():], the carrier of ():]
the L_meet of () . (x,y1) is ext-real epsilon-transitive epsilon-connected ordinal natural V39() real V41() Element of the carrier of ()
the L_meet of () . [x,y1] is set
x gcd y1 is ext-real epsilon-transitive epsilon-connected ordinal natural V39() real V41() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
x is ext-real epsilon-transitive epsilon-connected ordinal natural V39() real V41() Element of the carrier of ()
y1 is ext-real epsilon-transitive epsilon-connected ordinal natural V39() real V41() Element of the carrier of ()
x "\/" y1 is ext-real epsilon-transitive epsilon-connected ordinal natural V39() real V41() Element of the carrier of ()
the L_join of () . (x,y1) is ext-real epsilon-transitive epsilon-connected ordinal natural V39() real V41() Element of the carrier of ()
[x,y1] is set
{x,y1} is V24() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered set
{x} is V24() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered set
{{x,y1},{x}} is V24() V28() set
the L_join of () . [x,y1] is set
x lcm y1 is ext-real epsilon-transitive epsilon-connected ordinal natural V39() real V41() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
x is ext-real epsilon-transitive epsilon-connected ordinal natural V39() real V41() Element of the carrier of ()
y1 is ext-real epsilon-transitive epsilon-connected ordinal natural V39() real V41() Element of the carrier of ()
x "/\" y1 is ext-real epsilon-transitive epsilon-connected ordinal natural V39() real V41() Element of the carrier of ()
the L_meet of () . (x,y1) is ext-real epsilon-transitive epsilon-connected ordinal natural V39() real V41() Element of the carrier of ()
[x,y1] is set
{x,y1} is V24() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered set
{x} is V24() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered set
{{x,y1},{x}} is V24() V28() set
the L_meet of () . [x,y1] is set
x gcd y1 is ext-real epsilon-transitive epsilon-connected ordinal natural V39() real V41() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
x is ext-real epsilon-transitive epsilon-connected ordinal natural V39() real V41() Element of the carrier of ()
y1 is ext-real epsilon-transitive epsilon-connected ordinal natural V39() real V41() Element of the carrier of ()
x "\/" y1 is ext-real epsilon-transitive epsilon-connected ordinal natural V39() real V41() Element of the carrier of ()
the L_join of () . (x,y1) is ext-real epsilon-transitive epsilon-connected ordinal natural V39() real V41() Element of the carrier of ()
[x,y1] is set
{x,y1} is V24() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered set
{x} is V24() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered set
{{x,y1},{x}} is V24() V28() set
the L_join of () . [x,y1] is set
x lcm y1 is ext-real epsilon-transitive epsilon-connected ordinal natural V39() real V41() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
() is ext-real epsilon-transitive epsilon-connected ordinal natural V39() real V41() Element of the carrier of ()
() is ext-real epsilon-transitive epsilon-connected ordinal natural V39() real V41() Element of the carrier of ()
x is ext-real epsilon-transitive epsilon-connected ordinal natural V39() real V41() Element of the carrier of ()
() "/\" x is ext-real epsilon-transitive epsilon-connected ordinal natural V39() real V41() Element of the carrier of ()
the L_meet of () . ((),x) is ext-real epsilon-transitive epsilon-connected ordinal natural V39() real V41() Element of the carrier of ()
[(),x] is set
{(),x} is V24() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered set
{()} is V24() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered set
{{(),x},{()}} is V24() V28() set
the L_meet of () . [(),x] is set
() gcd x is ext-real epsilon-transitive epsilon-connected ordinal natural V39() real V41() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
y1 is ext-real epsilon-transitive epsilon-connected ordinal natural V39() real V41() Element of the carrier of ()
y1 "/\" () is ext-real epsilon-transitive epsilon-connected ordinal natural V39() real V41() Element of the carrier of ()
the L_meet of () . (y1,()) is ext-real epsilon-transitive epsilon-connected ordinal natural V39() real V41() Element of the carrier of ()
[y1,()] is set
{y1,()} is V24() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered set
{y1} is V24() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered set
{{y1,()},{y1}} is V24() V28() set
the L_meet of () . [y1,()] is set
y1 gcd () is ext-real epsilon-transitive epsilon-connected ordinal natural V39() real V41() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
x is ext-real epsilon-transitive epsilon-connected ordinal natural V39() real V41() Element of the carrier of ()
y1 is ext-real epsilon-transitive epsilon-connected ordinal natural V39() real V41() Element of the carrier of ()
x "\/" y1 is ext-real epsilon-transitive epsilon-connected ordinal natural V39() real V41() Element of the carrier of ()
the L_join of () . (x,y1) is ext-real epsilon-transitive epsilon-connected ordinal natural V39() real V41() Element of the carrier of ()
[x,y1] is set
{x,y1} is V24() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered set
{x} is V24() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered set
{{x,y1},{x}} is V24() V28() set
the L_join of () . [x,y1] is set
x lcm y1 is ext-real epsilon-transitive epsilon-connected ordinal natural V39() real V41() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
y1 "\/" x is ext-real epsilon-transitive epsilon-connected ordinal natural V39() real V41() Element of the carrier of ()
the L_join of () . (y1,x) is ext-real epsilon-transitive epsilon-connected ordinal natural V39() real V41() Element of the carrier of ()
[y1,x] is set
{y1,x} is V24() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered set
{y1} is V24() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered set
{{y1,x},{y1}} is V24() V28() set
the L_join of () . [y1,x] is set
y1 lcm x is ext-real epsilon-transitive epsilon-connected ordinal natural V39() real V41() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
y2 is ext-real epsilon-transitive epsilon-connected ordinal natural V39() real V41() Element of the carrier of ()
n is ext-real epsilon-transitive epsilon-connected ordinal natural V39() real V41() Element of the carrier of ()
k is ext-real epsilon-transitive epsilon-connected ordinal natural V39() real V41() Element of the carrier of ()
n "\/" k is ext-real epsilon-transitive epsilon-connected ordinal natural V39() real V41() Element of the carrier of ()
the L_join of () . (n,k) is ext-real epsilon-transitive epsilon-connected ordinal natural V39() real V41() Element of the carrier of ()
[n,k] is set
{n,k} is V24() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered set
{n} is V24() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered set
{{n,k},{n}} is V24() V28() set
the L_join of () . [n,k] is set
n lcm k is ext-real epsilon-transitive epsilon-connected ordinal natural V39() real V41() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
y2 "\/" (n "\/" k) is ext-real epsilon-transitive epsilon-connected ordinal natural V39() real V41() Element of the carrier of ()
the L_join of () . (y2,(n "\/" k)) is ext-real epsilon-transitive epsilon-connected ordinal natural V39() real V41() Element of the carrier of ()
[y2,(n "\/" k)] is set
{y2,(n "\/" k)} is V24() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered set
{y2} is V24() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered set
{{y2,(n "\/" k)},{y2}} is V24() V28() set
the L_join of () . [y2,(n "\/" k)] is set
y2 lcm (n "\/" k) is ext-real epsilon-transitive epsilon-connected ordinal natural V39() real V41() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
y2 "\/" n is ext-real epsilon-transitive epsilon-connected ordinal natural V39() real V41() Element of the carrier of ()
the L_join of () . (y2,n) is ext-real epsilon-transitive epsilon-connected ordinal natural V39() real V41() Element of the carrier of ()
[y2,n] is set
{y2,n} is V24() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered set
{{y2,n},{y2}} is V24() V28() set
the L_join of () . [y2,n] is set
y2 lcm n is ext-real epsilon-transitive epsilon-connected ordinal natural V39() real V41() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
(y2 "\/" n) "\/" k is ext-real epsilon-transitive epsilon-connected ordinal natural V39() real V41() Element of the carrier of ()
the L_join of () . ((y2 "\/" n),k) is ext-real epsilon-transitive epsilon-connected ordinal natural V39() real V41() Element of the carrier of ()
[(y2 "\/" n),k] is set
{(y2 "\/" n),k} is V24() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered set
{(y2 "\/" n)} is V24() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered set
{{(y2 "\/" n),k},{(y2 "\/" n)}} is V24() V28() set
the L_join of () . [(y2 "\/" n),k] is set
(y2 "\/" n) lcm k is ext-real epsilon-transitive epsilon-connected ordinal natural V39() real V41() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
n is ext-real epsilon-transitive epsilon-connected ordinal natural V39() real V41() Element of the carrier of ()
k is ext-real epsilon-transitive epsilon-connected ordinal natural V39() real V41() Element of the carrier of ()
n "/\" k is ext-real epsilon-transitive epsilon-connected ordinal natural V39() real V41() Element of the carrier of ()
the L_meet of () . (n,k) is ext-real epsilon-transitive epsilon-connected ordinal natural V39() real V41() Element of the carrier of ()
[n,k] is set
{n,k} is V24() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered set
{n} is V24() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered set
{{n,k},{n}} is V24() V28() set
the L_meet of () . [n,k] is set
n gcd k is ext-real epsilon-transitive epsilon-connected ordinal natural V39() real V41() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
(n "/\" k) "\/" k is ext-real epsilon-transitive epsilon-connected ordinal natural V39() real V41() Element of the carrier of ()
the L_join of () . ((n "/\" k),k) is ext-real epsilon-transitive epsilon-connected ordinal natural V39() real V41() Element of the carrier of ()
[(n "/\" k),k] is set
{(n "/\" k),k} is V24() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered set
{(n "/\" k)} is V24() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered set
{{(n "/\" k),k},{(n "/\" k)}} is V24() V28() set
the L_join of () . [(n "/\" k),k] is set
(n "/\" k) lcm k is ext-real epsilon-transitive epsilon-connected ordinal natural V39() real V41() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
c9 is ext-real epsilon-transitive epsilon-connected ordinal natural V39() real V41() Element of the carrier of ()
c₉ is ext-real epsilon-transitive epsilon-connected ordinal natural V39() real V41() Element of the carrier of ()
c9 "/\" c₉ is ext-real epsilon-transitive epsilon-connected ordinal natural V39() real V41() Element of the carrier of ()
the L_meet of () . (c9,c₉) is ext-real epsilon-transitive epsilon-connected ordinal natural V39() real V41() Element of the carrier of ()
[c9,c₉] is set
{c9,c₉} is V24() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered set
{c9} is V24() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered set
{{c9,c₉},{c9}} is V24() V28() set
the L_meet of () . [c9,c₉] is set
c9 gcd c₉ is ext-real epsilon-transitive epsilon-connected ordinal natural V39() real V41() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
c₉ "/\" c9 is ext-real epsilon-transitive epsilon-connected ordinal natural V39() real V41() Element of the carrier of ()
the L_meet of () . (c₉,c9) is ext-real epsilon-transitive epsilon-connected ordinal natural V39() real V41() Element of the carrier of ()
[c₉,c9] is set
{c₉,c9} is V24() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered set
{c₉} is V24() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered set
{{c₉,c9},{c₉}} is V24() V28() set
the L_meet of () . [c₉,c9] is set
c₉ gcd c9 is ext-real epsilon-transitive epsilon-connected ordinal natural V39() real V41() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
c₁₀ is ext-real epsilon-transitive epsilon-connected ordinal natural V39() real V41() Element of the carrier of ()
c₁₁ is ext-real epsilon-transitive epsilon-connected ordinal natural V39() real V41() Element of the carrier of ()
c₁₂ is ext-real epsilon-transitive epsilon-connected ordinal natural V39() real V41() Element of the carrier of ()
c₁₁ "/\" c₁₂ is ext-real epsilon-transitive epsilon-connected ordinal natural V39() real V41() Element of the carrier of ()
the L_meet of () . (c₁₁,c₁₂) is ext-real epsilon-transitive epsilon-connected ordinal natural V39() real V41() Element of the carrier of ()
[c₁₁,c₁₂] is set
{c₁₁,c₁₂} is V24() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered set
{c₁₁} is V24() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered set
{{c₁₁,c₁₂},{c₁₁}} is V24() V28() set
the L_meet of () . [c₁₁,c₁₂] is set
c₁₁ gcd c₁₂ is ext-real epsilon-transitive epsilon-connected ordinal natural V39() real V41() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
c₁₀ "/\" (c₁₁ "/\" c₁₂) is ext-real epsilon-transitive epsilon-connected ordinal natural V39() real V41() Element of the carrier of ()
the L_meet of () . (c₁₀,(c₁₁ "/\" c₁₂)) is ext-real epsilon-transitive epsilon-connected ordinal natural V39() real V41() Element of the carrier of ()
[c₁₀,(c₁₁ "/\" c₁₂)] is set
{c₁₀,(c₁₁ "/\" c₁₂)} is V24() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered set
{c₁₀} is V24() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered set
{{c₁₀,(c₁₁ "/\" c₁₂)},{c₁₀}} is V24() V28() set
the L_meet of () . [c₁₀,(c₁₁ "/\" c₁₂)] is set
c₁₀ gcd (c₁₁ "/\" c₁₂) is ext-real epsilon-transitive epsilon-connected ordinal natural V39() real V41() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
c₁₀ "/\" c₁₁ is ext-real epsilon-transitive epsilon-connected ordinal natural V39() real V41() Element of the carrier of ()
the L_meet of () . (c₁₀,c₁₁) is ext-real epsilon-transitive epsilon-connected ordinal natural V39() real V41() Element of the carrier of ()
[c₁₀,c₁₁] is set
{c₁₀,c₁₁} is V24() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered set
{{c₁₀,c₁₁},{c₁₀}} is V24() V28() set
the L_meet of () . [c₁₀,c₁₁] is set
c₁₀ gcd c₁₁ is ext-real epsilon-transitive epsilon-connected ordinal natural V39() real V41() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
(c₁₀ "/\" c₁₁) "/\" c₁₂ is ext-real epsilon-transitive epsilon-connected ordinal natural V39() real V41() Element of the carrier of ()
the L_meet of () . ((c₁₀ "/\" c₁₁),c₁₂) is ext-real epsilon-transitive epsilon-connected ordinal natural V39() real V41() Element of the carrier of ()
[(c₁₀ "/\" c₁₁),c₁₂] is set
{(c₁₀ "/\" c₁₁),c₁₂} is V24() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered set
{(c₁₀ "/\" c₁₁)} is V24() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered set
{{(c₁₀ "/\" c₁₁),c₁₂},{(c₁₀ "/\" c₁₁)}} is V24() V28() set
the L_meet of () . [(c₁₀ "/\" c₁₁),c₁₂] is set
(c₁₀ "/\" c₁₁) gcd c₁₂ is ext-real epsilon-transitive epsilon-connected ordinal natural V39() real V41() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
c₁₃ is ext-real epsilon-transitive epsilon-connected ordinal natural V39() real V41() Element of the carrier of ()
c₁₄ is ext-real epsilon-transitive epsilon-connected ordinal natural V39() real V41() Element of the carrier of ()
c₁₃ "\/" c₁₄ is ext-real epsilon-transitive epsilon-connected ordinal natural V39() real V41() Element of the carrier of ()
the L_join of () . (c₁₃,c₁₄) is ext-real epsilon-transitive epsilon-connected ordinal natural V39() real V41() Element of the carrier of ()
[c₁₃,c₁₄] is set
{c₁₃,c₁₄} is V24() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered set
{c₁₃} is V24() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered set
{{c₁₃,c₁₄},{c₁₃}} is V24() V28() set
the L_join of () . [c₁₃,c₁₄] is set
c₁₃ lcm c₁₄ is ext-real epsilon-transitive epsilon-connected ordinal natural V39() real V41() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
c₁₃ "/\" (c₁₃ "\/" c₁₄) is ext-real epsilon-transitive epsilon-connected ordinal natural V39() real V41() Element of the carrier of ()
the L_meet of () . (c₁₃,(c₁₃ "\/" c₁₄)) is ext-real epsilon-transitive epsilon-connected ordinal natural V39() real V41() Element of the carrier of ()
[c₁₃,(c₁₃ "\/" c₁₄)] is set
{c₁₃,(c₁₃ "\/" c₁₄)} is V24() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered set
{{c₁₃,(c₁₃ "\/" c₁₄)},{c₁₃}} is V24() V28() set
the L_meet of () . [c₁₃,(c₁₃ "\/" c₁₄)] is set
c₁₃ gcd (c₁₃ "\/" c₁₄) is ext-real epsilon-transitive epsilon-connected ordinal natural V39() real V41() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
x is ext-real epsilon-transitive epsilon-connected ordinal natural V39() real V41() Element of the carrier of ()
y1 is ext-real epsilon-transitive epsilon-connected ordinal natural V39() real V41() Element of the carrier of ()
() . (x,y1) is set
[x,y1] is set
{x,y1} is V24() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered set
{x} is V24() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered set
{{x,y1},{x}} is V24() V28() set
() . [x,y1] is set
() . (y1,x) is set
[y1,x] is set
{y1,x} is V24() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered set
{y1} is V24() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered set
{{y1,x},{y1}} is V24() V28() set
() . [y1,x] is set
y1 "\/" x is ext-real epsilon-transitive epsilon-connected ordinal natural V39() real V41() Element of the carrier of ()
the L_join of () . (y1,x) is ext-real epsilon-transitive epsilon-connected ordinal natural V39() real V41() Element of the carrier of ()
the L_join of () . [y1,x] is set
y1 lcm x is ext-real epsilon-transitive epsilon-connected ordinal natural V39() real V41() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
x is ext-real epsilon-transitive epsilon-connected ordinal natural V39() real V41() Element of the carrier of ()
y1 is ext-real epsilon-transitive epsilon-connected ordinal natural V39() real V41() Element of the carrier of ()
() . (x,y1) is set
[x,y1] is set
{x,y1} is V24() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered set
{x} is V24() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered set
{{x,y1},{x}} is V24() V28() set
() . [x,y1] is set
() . (y1,x) is set
[y1,x] is set
{y1,x} is V24() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered set
{y1} is V24() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered set
{{y1,x},{y1}} is V24() V28() set
() . [y1,x] is set
y1 "/\" x is ext-real epsilon-transitive epsilon-connected ordinal natural V39() real V41() Element of the carrier of ()
the L_meet of () . (y1,x) is ext-real epsilon-transitive epsilon-connected ordinal natural V39() real V41() Element of the carrier of ()
the L_meet of () . [y1,x] is set
y1 gcd x is ext-real epsilon-transitive epsilon-connected ordinal natural V39() real V41() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
x is ext-real epsilon-transitive epsilon-connected ordinal natural V39() real V41() Element of the carrier of ()
y1 is ext-real epsilon-transitive epsilon-connected ordinal natural V39() real V41() Element of the carrier of ()
() . (x,y1) is set
[x,y1] is set
{x,y1} is V24() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered set
{x} is V24() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered set
{{x,y1},{x}} is V24() V28() set
() . [x,y1] is set
y2 is ext-real epsilon-transitive epsilon-connected ordinal natural V39() real V41() Element of the carrier of ()
() . (y1,y2) is set
[y1,y2] is set
{y1,y2} is V24() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered set
{y1} is V24() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered set
{{y1,y2},{y1}} is V24() V28() set
() . [y1,y2] is set
() . (x,(() . (y1,y2))) is set
[x,(() . (y1,y2))] is set
{x,(() . (y1,y2))} is V24() set
{{x,(() . (y1,y2))},{x}} is V24() V28() set
() . [x,(() . (y1,y2))] is set
() . ((() . (x,y1)),y2) is set
[(() . (x,y1)),y2] is set
{(() . (x,y1)),y2} is V24() set
{(() . (x,y1))} is V24() set
{{(() . (x,y1)),y2},{(() . (x,y1))}} is V24() V28() set
() . [(() . (x,y1)),y2] is set
y1 "\/" y2 is ext-real epsilon-transitive epsilon-connected ordinal natural V39() real V41() Element of the carrier of ()
the L_join of () . (y1,y2) is ext-real epsilon-transitive epsilon-connected ordinal natural V39() real V41() Element of the carrier of ()
the L_join of () . [y1,y2] is set
y1 lcm y2 is ext-real epsilon-transitive epsilon-connected ordinal natural V39() real V41() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
x "\/" (y1 "\/" y2) is ext-real epsilon-transitive epsilon-connected ordinal natural V39() real V41() Element of the carrier of ()
the L_join of () . (x,(y1 "\/" y2)) is ext-real epsilon-transitive epsilon-connected ordinal natural V39() real V41() Element of the carrier of ()
[x,(y1 "\/" y2)] is set
{x,(y1 "\/" y2)} is V24() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered set
{{x,(y1 "\/" y2)},{x}} is V24() V28() set
the L_join of () . [x,(y1 "\/" y2)] is set
x lcm (y1 "\/" y2) is ext-real epsilon-transitive epsilon-connected ordinal natural V39() real V41() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
x "\/" y1 is ext-real epsilon-transitive epsilon-connected ordinal natural V39() real V41() Element of the carrier of ()
the L_join of () . (x,y1) is ext-real epsilon-transitive epsilon-connected ordinal natural V39() real V41() Element of the carrier of ()
the L_join of () . [x,y1] is set
x lcm y1 is ext-real epsilon-transitive epsilon-connected ordinal natural V39() real V41() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
(x "\/" y1) "\/" y2 is ext-real epsilon-transitive epsilon-connected ordinal natural V39() real V41() Element of the carrier of ()
the L_join of () . ((x "\/" y1),y2) is ext-real epsilon-transitive epsilon-connected ordinal natural V39() real V41() Element of the carrier of ()
[(x "\/" y1),y2] is set
{(x "\/" y1),y2} is V24() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered set
{(x "\/" y1)} is V24() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered set
{{(x "\/" y1),y2},{(x "\/" y1)}} is V24() V28() set
the L_join of () . [(x "\/" y1),y2] is set
(x "\/" y1) lcm y2 is ext-real epsilon-transitive epsilon-connected ordinal natural V39() real V41() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
x is ext-real epsilon-transitive epsilon-connected ordinal natural V39() real V41() Element of the carrier of ()
y1 is ext-real epsilon-transitive epsilon-connected ordinal natural V39() real V41() Element of the carrier of ()
() . (y1,x) is set
[y1,x] is set
{y1,x} is V24() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered set
{y1} is V24() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered set
{{y1,x},{y1}} is V24() V28() set
() . [y1,x] is set
y2 is ext-real epsilon-transitive epsilon-connected ordinal natural V39() real V41() Element of the carrier of ()
() . (y1,y2) is set
[y1,y2] is set
{y1,y2} is V24() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered set
{{y1,y2},{y1}} is V24() V28() set
() . [y1,y2] is set
() . (x,(() . (y1,y2))) is set
[x,(() . (y1,y2))] is set
{x,(() . (y1,y2))} is V24() set
{x} is V24() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered set
{{x,(() . (y1,y2))},{x}} is V24() V28() set
() . [x,(() . (y1,y2))] is set
() . ((() . (y1,x)),y2) is set
[(() . (y1,x)),y2] is set
{(() . (y1,x)),y2} is V24() set
{(() . (y1,x))} is V24() set
{{(() . (y1,x)),y2},{(() . (y1,x))}} is V24() V28() set
() . [(() . (y1,x)),y2] is set
() . (x,y2) is set
[x,y2] is set
{x,y2} is V24() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered set
{{x,y2},{x}} is V24() V28() set
() . [x,y2] is set
() . ((() . (x,y2)),y1) is set
[(() . (x,y2)),y1] is set
{(() . (x,y2)),y1} is V24() set
{(() . (x,y2))} is V24() set
{{(() . (x,y2)),y1},{(() . (x,y2))}} is V24() V28() set
() . [(() . (x,y2)),y1] is set
() . (y2,y1) is set
[y2,y1] is set
{y2,y1} is V24() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered set
{y2} is V24() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered set
{{y2,y1},{y2}} is V24() V28() set
() . [y2,y1] is set
() . ((() . (y2,y1)),x) is set
[(() . (y2,y1)),x] is set
{(() . (y2,y1)),x} is V24() set
{(() . (y2,y1))} is V24() set
{{(() . (y2,y1)),x},{(() . (y2,y1))}} is V24() V28() set
() . [(() . (y2,y1)),x] is set
() . (y2,x) is set
[y2,x] is set
{y2,x} is V24() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered set
{{y2,x},{y2}} is V24() V28() set
() . [y2,x] is set
() . ((() . (y2,x)),y1) is set
[(() . (y2,x)),y1] is set
{(() . (y2,x)),y1} is V24() set
{(() . (y2,x))} is V24() set
{{(() . (y2,x)),y1},{(() . (y2,x))}} is V24() V28() set
() . [(() . (y2,x)),y1] is set
y2 "\/" y1 is ext-real epsilon-transitive epsilon-connected ordinal natural V39() real V41() Element of the carrier of ()
the L_join of () . (y2,y1) is ext-real epsilon-transitive epsilon-connected ordinal natural V39() real V41() Element of the carrier of ()
the L_join of () . [y2,y1] is set
y2 lcm y1 is ext-real epsilon-transitive epsilon-connected ordinal natural V39() real V41() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
() . (x,y1) is set
[x,y1] is set
{x,y1} is V24() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered set
{{x,y1},{x}} is V24() V28() set
() . [x,y1] is set
() . ((() . (x,y1)),y2) is set
[(() . (x,y1)),y2] is set
{(() . (x,y1)),y2} is V24() set
{(() . (x,y1))} is V24() set
{{(() . (x,y1)),y2},{(() . (x,y1))}} is V24() V28() set
() . [(() . (x,y1)),y2] is set
() . (x,(() . (y2,y1))) is set
[x,(() . (y2,y1))] is set
{x,(() . (y2,y1))} is V24() set
{{x,(() . (y2,y1))},{x}} is V24() V28() set
() . [x,(() . (y2,y1))] is set
() . (x,(y2 "\/" y1)) is set
[x,(y2 "\/" y1)] is set
{x,(y2 "\/" y1)} is V24() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered set
{{x,(y2 "\/" y1)},{x}} is V24() V28() set
() . [x,(y2 "\/" y1)] is set
x is ext-real epsilon-transitive epsilon-connected ordinal natural V39() real V41() Element of the carrier of ()
y1 is ext-real epsilon-transitive epsilon-connected ordinal natural V39() real V41() Element of the carrier of ()
() . (x,y1) is set
[x,y1] is set
{x,y1} is V24() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered set
{x} is V24() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered set
{{x,y1},{x}} is V24() V28() set
() . [x,y1] is set
y2 is ext-real epsilon-transitive epsilon-connected ordinal natural V39() real V41() Element of the carrier of ()
() . (y1,y2) is set
[y1,y2] is set
{y1,y2} is V24() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered set
{y1} is V24() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered set
{{y1,y2},{y1}} is V24() V28() set
() . [y1,y2] is set
() . (x,(() . (y1,y2))) is set
[x,(() . (y1,y2))] is set
{x,(() . (y1,y2))} is V24() set
{{x,(() . (y1,y2))},{x}} is V24() V28() set
() . [x,(() . (y1,y2))] is set
() . ((() . (x,y1)),y2) is set
[(() . (x,y1)),y2] is set
{(() . (x,y1)),y2} is V24() set
{(() . (x,y1))} is V24() set
{{(() . (x,y1)),y2},{(() . (x,y1))}} is V24() V28() set
() . [(() . (x,y1)),y2] is set
y1 "/\" y2 is ext-real epsilon-transitive epsilon-connected ordinal natural V39() real V41() Element of the carrier of ()
the L_meet of () . (y1,y2) is ext-real epsilon-transitive epsilon-connected ordinal natural V39() real V41() Element of the carrier of ()
the L_meet of () . [y1,y2] is set
y1 gcd y2 is ext-real epsilon-transitive epsilon-connected ordinal natural V39() real V41() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
x "/\" (y1 "/\" y2) is ext-real epsilon-transitive epsilon-connected ordinal natural V39() real V41() Element of the carrier of ()
the L_meet of () . (x,(y1 "/\" y2)) is ext-real epsilon-transitive epsilon-connected ordinal natural V39() real V41() Element of the carrier of ()
[x,(y1 "/\" y2)] is set
{x,(y1 "/\" y2)} is V24() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered set
{{x,(y1 "/\" y2)},{x}} is V24() V28() set
the L_meet of () . [x,(y1 "/\" y2)] is set
x gcd (y1 "/\" y2) is ext-real epsilon-transitive epsilon-connected ordinal natural V39() real V41() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
x "/\" y1 is ext-real epsilon-transitive epsilon-connected ordinal natural V39() real V41() Element of the carrier of ()
the L_meet of () . (x,y1) is ext-real epsilon-transitive epsilon-connected ordinal natural V39() real V41() Element of the carrier of ()
the L_meet of () . [x,y1] is set
x gcd y1 is ext-real epsilon-transitive epsilon-connected ordinal natural V39() real V41() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
(x "/\" y1) "/\" y2 is ext-real epsilon-transitive epsilon-connected ordinal natural V39() real V41() Element of the carrier of ()
the L_meet of () . ((x "/\" y1),y2) is ext-real epsilon-transitive epsilon-connected ordinal natural V39() real V41() Element of the carrier of ()
[(x "/\" y1),y2] is set
{(x "/\" y1),y2} is V24() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered set
{(x "/\" y1)} is V24() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered set
{{(x "/\" y1),y2},{(x "/\" y1)}} is V24() V28() set
the L_meet of () . [(x "/\" y1),y2] is set
(x "/\" y1) gcd y2 is ext-real epsilon-transitive epsilon-connected ordinal natural V39() real V41() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
x is ext-real epsilon-transitive epsilon-connected ordinal natural V39() real V41() Element of the carrier of ()
y1 is ext-real epsilon-transitive epsilon-connected ordinal natural V39() real V41() Element of the carrier of ()
() . (y1,x) is set
[y1,x] is set
{y1,x} is V24() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered set
{y1} is V24() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered set
{{y1,x},{y1}} is V24() V28() set
() . [y1,x] is set
y2 is ext-real epsilon-transitive epsilon-connected ordinal natural V39() real V41() Element of the carrier of ()
() . (y1,y2) is set
[y1,y2] is set
{y1,y2} is V24() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered set
{{y1,y2},{y1}} is V24() V28() set
() . [y1,y2] is set
() . (x,(() . (y1,y2))) is set
[x,(() . (y1,y2))] is set
{x,(() . (y1,y2))} is V24() set
{x} is V24() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered set
{{x,(() . (y1,y2))},{x}} is V24() V28() set
() . [x,(() . (y1,y2))] is set
() . ((() . (y1,x)),y2) is set
[(() . (y1,x)),y2] is set
{(() . (y1,x)),y2} is V24() set
{(() . (y1,x))} is V24() set
{{(() . (y1,x)),y2},{(() . (y1,x))}} is V24() V28() set
() . [(() . (y1,x)),y2] is set
() . (x,y2) is set
[x,y2] is set
{x,y2} is V24() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered set
{{x,y2},{x}} is V24() V28() set
() . [x,y2] is set
() . ((() . (x,y2)),y1) is set
[(() . (x,y2)),y1] is set
{(() . (x,y2)),y1} is V24() set
{(() . (x,y2))} is V24() set
{{(() . (x,y2)),y1},{(() . (x,y2))}} is V24() V28() set
() . [(() . (x,y2)),y1] is set
() . (y2,y1) is set
[y2,y1] is set
{y2,y1} is V24() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered set
{y2} is V24() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered set
{{y2,y1},{y2}} is V24() V28() set
() . [y2,y1] is set
() . ((() . (y2,y1)),x) is set
[(() . (y2,y1)),x] is set
{(() . (y2,y1)),x} is V24() set
{(() . (y2,y1))} is V24() set
{{(() . (y2,y1)),x},{(() . (y2,y1))}} is V24() V28() set
() . [(() . (y2,y1)),x] is set
() . (y2,x) is set
[y2,x] is set
{y2,x} is V24() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered set
{{y2,x},{y2}} is V24() V28() set
() . [y2,x] is set
() . ((() . (y2,x)),y1) is set
[(() . (y2,x)),y1] is set
{(() . (y2,x)),y1} is V24() set
{(() . (y2,x))} is V24() set
{{(() . (y2,x)),y1},{(() . (y2,x))}} is V24() V28() set
() . [(() . (y2,x)),y1] is set
y2 "/\" y1 is ext-real epsilon-transitive epsilon-connected ordinal natural V39() real V41() Element of the carrier of ()
the L_meet of () . (y2,y1) is ext-real epsilon-transitive epsilon-connected ordinal natural V39() real V41() Element of the carrier of ()
the L_meet of () . [y2,y1] is set
y2 gcd y1 is ext-real epsilon-transitive epsilon-connected ordinal natural V39() real V41() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
() . (x,y1) is set
[x,y1] is set
{x,y1} is V24() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered set
{{x,y1},{x}} is V24() V28() set
() . [x,y1] is set
() . ((() . (x,y1)),y2) is set
[(() . (x,y1)),y2] is set
{(() . (x,y1)),y2} is V24() set
{(() . (x,y1))} is V24() set
{{(() . (x,y1)),y2},{(() . (x,y1))}} is V24() V28() set
() . [(() . (x,y1)),y2] is set
() . (x,(() . (y2,y1))) is set
[x,(() . (y2,y1))] is set
{x,(() . (y2,y1))} is V24() set
{{x,(() . (y2,y1))},{x}} is V24() V28() set
() . [x,(() . (y2,y1))] is set
() . (x,(y2 "/\" y1)) is set
[x,(y2 "/\" y1)] is set
{x,(y2 "/\" y1)} is V24() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered set
{{x,(y2 "/\" y1)},{x}} is V24() V28() set
() . [x,(y2 "/\" y1)] is set
x is ext-real epsilon-transitive epsilon-connected ordinal natural V39() real V41() Element of the carrier of ()
y1 is ext-real epsilon-transitive epsilon-connected ordinal natural V39() real V41() Element of the carrier of ()
() . (x,y1) is set
[x,y1] is set
{x,y1} is V24() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered set
{x} is V24() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered set
{{x,y1},{x}} is V24() V28() set
() . [x,y1] is set
() . (x,(() . (x,y1))) is set
[x,(() . (x,y1))] is set
{x,(() . (x,y1))} is V24() set
{{x,(() . (x,y1))},{x}} is V24() V28() set
() . [x,(() . (x,y1))] is set
() . (y1,x) is set
[y1,x] is set
{y1,x} is V24() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered set
{y1} is V24() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered set
{{y1,x},{y1}} is V24() V28() set
() . [y1,x] is set
() . ((() . (y1,x)),x) is set
[(() . (y1,x)),x] is set
{(() . (y1,x)),x} is V24() set
{(() . (y1,x))} is V24() set
{{(() . (y1,x)),x},{(() . (y1,x))}} is V24() V28() set
() . [(() . (y1,x)),x] is set
() . (x,(() . (y1,x))) is set
[x,(() . (y1,x))] is set
{x,(() . (y1,x))} is V24() set
{{x,(() . (y1,x))},{x}} is V24() V28() set
() . [x,(() . (y1,x))] is set
() . ((() . (x,y1)),x) is set
[(() . (x,y1)),x] is set
{(() . (x,y1)),x} is V24() set
{(() . (x,y1))} is V24() set
{{(() . (x,y1)),x},{(() . (x,y1))}} is V24() V28() set
() . [(() . (x,y1)),x] is set
x "\/" y1 is ext-real epsilon-transitive epsilon-connected ordinal natural V39() real V41() Element of the carrier of ()
the L_join of () . (x,y1) is ext-real epsilon-transitive epsilon-connected ordinal natural V39() real V41() Element of the carrier of ()
the L_join of () . [x,y1] is set
x lcm y1 is ext-real epsilon-transitive epsilon-connected ordinal natural V39() real V41() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
x "/\" (x "\/" y1) is ext-real epsilon-transitive epsilon-connected ordinal natural V39() real V41() Element of the carrier of ()
the L_meet of () . (x,(x "\/" y1)) is ext-real epsilon-transitive epsilon-connected ordinal natural V39() real V41() Element of the carrier of ()
[x,(x "\/" y1)] is set
{x,(x "\/" y1)} is V24() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered set
{{x,(x "\/" y1)},{x}} is V24() V28() set
the L_meet of () . [x,(x "\/" y1)] is set
x gcd (x "\/" y1) is ext-real epsilon-transitive epsilon-connected ordinal natural V39() real V41() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
y1 "\/" x is ext-real epsilon-transitive epsilon-connected ordinal natural V39() real V41() Element of the carrier of ()
the L_join of () . (y1,x) is ext-real epsilon-transitive epsilon-connected ordinal natural V39() real V41() Element of the carrier of ()
the L_join of () . [y1,x] is set
y1 lcm x is ext-real epsilon-transitive epsilon-connected ordinal natural V39() real V41() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
() . ((y1 "\/" x),x) is set
[(y1 "\/" x),x] is set
{(y1 "\/" x),x} is V24() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered set
{(y1 "\/" x)} is V24() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered set
{{(y1 "\/" x),x},{(y1 "\/" x)}} is V24() V28() set
() . [(y1 "\/" x),x] is set
x is ext-real epsilon-transitive epsilon-connected ordinal natural V39() real V41() Element of the carrier of ()
y1 is ext-real epsilon-transitive epsilon-connected ordinal natural V39() real V41() Element of the carrier of ()
() . (x,y1) is set
[x,y1] is set
{x,y1} is V24() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered set
{x} is V24() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered set
{{x,y1},{x}} is V24() V28() set
() . [x,y1] is set
() . (x,(() . (x,y1))) is set
[x,(() . (x,y1))] is set
{x,(() . (x,y1))} is V24() set
{{x,(() . (x,y1))},{x}} is V24() V28() set
() . [x,(() . (x,y1))] is set
() . (y1,x) is set
[y1,x] is set
{y1,x} is V24() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered set
{y1} is V24() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered set
{{y1,x},{y1}} is V24() V28() set
() . [y1,x] is set
() . ((() . (y1,x)),x) is set
[(() . (y1,x)),x] is set
{(() . (y1,x)),x} is V24() set
{(() . (y1,x))} is V24() set
{{(() . (y1,x)),x},{(() . (y1,x))}} is V24() V28() set
() . [(() . (y1,x)),x] is set
() . (x,(() . (y1,x))) is set
[x,(() . (y1,x))] is set
{x,(() . (y1,x))} is V24() set
{{x,(() . (y1,x))},{x}} is V24() V28() set
() . [x,(() . (y1,x))] is set
() . ((() . (x,y1)),x) is set
[(() . (x,y1)),x] is set
{(() . (x,y1)),x} is V24() set
{(() . (x,y1))} is V24() set
{{(() . (x,y1)),x},{(() . (x,y1))}} is V24() V28() set
() . [(() . (x,y1)),x] is set
y1 "/\" x is ext-real epsilon-transitive epsilon-connected ordinal natural V39() real V41() Element of the carrier of ()
the L_meet of () . (y1,x) is ext-real epsilon-transitive epsilon-connected ordinal natural V39() real V41() Element of the carrier of ()
the L_meet of () . [y1,x] is set
y1 gcd x is ext-real epsilon-transitive epsilon-connected ordinal natural V39() real V41() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
x "/\" y1 is ext-real epsilon-transitive epsilon-connected ordinal natural V39() real V41() Element of the carrier of ()
the L_meet of () . (x,y1) is ext-real epsilon-transitive epsilon-connected ordinal natural V39() real V41() Element of the carrier of ()
the L_meet of () . [x,y1] is set
x gcd y1 is ext-real epsilon-transitive epsilon-connected ordinal natural V39() real V41() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
() . (x,(x "/\" y1)) is set
[x,(x "/\" y1)] is set
{x,(x "/\" y1)} is V24() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered set
{{x,(x "/\" y1)},{x}} is V24() V28() set
() . [x,(x "/\" y1)] is set
(y1 "/\" x) "\/" x is ext-real epsilon-transitive epsilon-connected ordinal natural V39() real V41() Element of the carrier of ()
the L_join of () . ((y1 "/\" x),x) is ext-real epsilon-transitive epsilon-connected ordinal natural V39() real V41() Element of the carrier of ()
[(y1 "/\" x),x] is set
{(y1 "/\" x),x} is V24() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered set
{(y1 "/\" x)} is V24() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered set
{{(y1 "/\" x),x},{(y1 "/\" x)}} is V24() V28() set
the L_join of () . [(y1 "/\" x),x] is set
(y1 "/\" x) lcm x is ext-real epsilon-transitive epsilon-connected ordinal natural V39() real V41() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
bool NAT is set
x is complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of bool NAT
y1 is ext-real epsilon-transitive epsilon-connected ordinal natural V39() real set
x is complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of bool NAT
y1 is complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of bool NAT
y2 is set
n is ext-real epsilon-transitive epsilon-connected ordinal natural V39() real set
y2 is set
n is ext-real epsilon-transitive epsilon-connected ordinal natural V39() real set
() is complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of bool NAT
x is non empty set
bool x is set
y1 is non empty Element of bool x
bool y1 is set
y2 is non empty Element of bool y1
n is Element of y2
x is complex-membered ext-real-membered real-membered Element of bool REAL
y1 is ext-real V39() real Element of x
x is complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of bool NAT
y1 is ext-real epsilon-transitive epsilon-connected ordinal natural V39() real V41() Element of x
x is ext-real epsilon-transitive epsilon-connected ordinal natural V39() real set
x is ext-real epsilon-transitive epsilon-connected ordinal natural V39() real V41() Element of ()
y1 is ext-real epsilon-transitive epsilon-connected ordinal natural V39() real V41() Element of ()
[:(),():] is set
[:[:(),():],():] is set
bool [:[:(),():],():] is set
x is Relation-like [:(),():] -defined () -valued Function-like V18([:(),():],()) Element of bool [:[:(),():],():]
y1 is non empty ext-real epsilon-transitive epsilon-connected ordinal natural V39() real V41() Element of ()
y2 is non empty ext-real epsilon-transitive epsilon-connected ordinal natural V39() real V41() Element of ()
x . (y1,y2) is non empty ext-real epsilon-transitive epsilon-connected ordinal natural V39() real V41() Element of ()
[y1,y2] is set
{y1,y2} is V24() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered set
{y1} is V24() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered set
{{y1,y2},{y1}} is V24() V28() set
x . [y1,y2] is set
y1 gcd y2 is ext-real epsilon-transitive epsilon-connected ordinal natural V39() real V41() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
((y1 gcd y2)) is non empty ext-real epsilon-transitive epsilon-connected ordinal natural V39() real V41() Element of ()
x is Relation-like [:(),():] -defined () -valued Function-like V18([:(),():],()) Element of bool [:[:(),():],():]
y1 is non empty ext-real epsilon-transitive epsilon-connected ordinal natural V39() real V41() Element of ()
y2 is non empty ext-real epsilon-transitive epsilon-connected ordinal natural V39() real V41() Element of ()
x . (y1,y2) is non empty ext-real epsilon-transitive epsilon-connected ordinal natural V39() real V41() Element of ()
[y1,y2] is set
{y1,y2} is V24() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered set
{y1} is V24() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered set
{{y1,y2},{y1}} is V24() V28() set
x . [y1,y2] is set
y1 lcm y2 is ext-real epsilon-transitive epsilon-connected ordinal natural V39() real V41() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
((y1 lcm y2)) is non empty ext-real epsilon-transitive epsilon-connected ordinal natural V39() real V41() Element of ()
() is Relation-like [:(),():] -defined () -valued Function-like V18([:(),():],()) Element of bool [:[:(),():],():]
() is Relation-like [:(),():] -defined () -valued Function-like V18([:(),():],()) Element of bool [:[:(),():],():]
LattStr(# (),(),() #) is non empty strict LattStr
() is strict LattStr
the carrier of () is non empty set
x is Element of the carrier of ()
x is Element of the carrier of ()
y1 is Element of the carrier of ()
x is non empty ext-real epsilon-transitive epsilon-connected ordinal natural V39() real Element of the carrier of ()
y1 is non empty ext-real epsilon-transitive epsilon-connected ordinal natural V39() real Element of the carrier of ()
x "\/" y1 is non empty ext-real epsilon-transitive epsilon-connected ordinal natural V39() real Element of the carrier of ()
the L_join of () is Relation-like [: the carrier of (), the carrier of ():] -defined the carrier of () -valued Function-like V18([: the carrier of (), the carrier of ():], the carrier of ()) Element of bool [:[: the carrier of (), the carrier of ():], the carrier of ():]
[: the carrier of (), the carrier of ():] is set
[:[: the carrier of (), the carrier of ():], the carrier of ():] is set
bool [:[: the carrier of (), the carrier of ():], the carrier of ():] is set
the L_join of () . (x,y1) is non empty ext-real epsilon-transitive epsilon-connected ordinal natural V39() real Element of the carrier of ()
[x,y1] is set
{x,y1} is V24() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered set
{x} is V24() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered set
{{x,y1},{x}} is V24() V28() set
the L_join of () . [x,y1] is set
x lcm y1 is ext-real epsilon-transitive epsilon-connected ordinal natural V39() real V41() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
x "/\" y1 is non empty ext-real epsilon-transitive epsilon-connected ordinal natural V39() real Element of the carrier of ()
the L_meet of () is Relation-like [: the carrier of (), the carrier of ():] -defined the carrier of () -valued Function-like V18([: the carrier of (), the carrier of ():], the carrier of ()) Element of bool [:[: the carrier of (), the carrier of ():], the carrier of ():]
the L_meet of () . (x,y1) is non empty ext-real epsilon-transitive epsilon-connected ordinal natural V39() real Element of the carrier of ()
the L_meet of () . [x,y1] is set
x gcd y1 is ext-real epsilon-transitive epsilon-connected ordinal natural V39() real V41() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
x is non empty ext-real epsilon-transitive epsilon-connected ordinal natural V39() real Element of the carrier of ()
y1 is non empty ext-real epsilon-transitive epsilon-connected ordinal natural V39() real Element of the carrier of ()
x "\/" y1 is non empty ext-real epsilon-transitive epsilon-connected ordinal natural V39() real Element of the carrier of ()
the L_join of () . (x,y1) is non empty ext-real epsilon-transitive epsilon-connected ordinal natural V39() real Element of the carrier of ()
[x,y1] is set
{x,y1} is V24() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered set
{x} is V24() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered set
{{x,y1},{x}} is V24() V28() set
the L_join of () . [x,y1] is set
x lcm y1 is ext-real epsilon-transitive epsilon-connected ordinal natural V39() real V41() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
(x) is non empty ext-real epsilon-transitive epsilon-connected ordinal natural V39() real V41() Element of ()
(y1) is non empty ext-real epsilon-transitive epsilon-connected ordinal natural V39() real V41() Element of ()
(x) lcm (y1) is ext-real epsilon-transitive epsilon-connected ordinal natural V39() real V41() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
x is non empty ext-real epsilon-transitive epsilon-connected ordinal natural V39() real Element of the carrier of ()
y1 is non empty ext-real epsilon-transitive epsilon-connected ordinal natural V39() real Element of the carrier of ()
x "/\" y1 is non empty ext-real epsilon-transitive epsilon-connected ordinal natural V39() real Element of the carrier of ()
the L_meet of () . (x,y1) is non empty ext-real epsilon-transitive epsilon-connected ordinal natural V39() real Element of the carrier of ()
[x,y1] is set
{x,y1} is V24() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered set
{x} is V24() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered set
{{x,y1},{x}} is V24() V28() set
the L_meet of () . [x,y1] is set
x gcd y1 is ext-real epsilon-transitive epsilon-connected ordinal natural V39() real V41() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
(x) is non empty ext-real epsilon-transitive epsilon-connected ordinal natural V39() real V41() Element of ()
(y1) is non empty ext-real epsilon-transitive epsilon-connected ordinal natural V39() real V41() Element of ()
(x) gcd (y1) is ext-real epsilon-transitive epsilon-connected ordinal natural V39() real V41() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
x is non empty ext-real epsilon-transitive epsilon-connected ordinal natural V39() real Element of the carrier of ()
y1 is non empty ext-real epsilon-transitive epsilon-connected ordinal natural V39() real Element of the carrier of ()
x "\/" y1 is non empty ext-real epsilon-transitive epsilon-connected ordinal natural V39() real Element of the carrier of ()
the L_join of () . (x,y1) is non empty ext-real epsilon-transitive epsilon-connected ordinal natural V39() real Element of the carrier of ()
[x,y1] is set
{x,y1} is V24() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered set
{x} is V24() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered set
{{x,y1},{x}} is V24() V28() set
the L_join of () . [x,y1] is set
x lcm y1 is ext-real epsilon-transitive epsilon-connected ordinal natural V39() real V41() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
y1 "\/" x is non empty ext-real epsilon-transitive epsilon-connected ordinal natural V39() real Element of the carrier of ()
the L_join of () . (y1,x) is non empty ext-real epsilon-transitive epsilon-connected ordinal natural V39() real Element of the carrier of ()
[y1,x] is set
{y1,x} is V24() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered set
{y1} is V24() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered set
{{y1,x},{y1}} is V24() V28() set
the L_join of () . [y1,x] is set
y1 lcm x is ext-real epsilon-transitive epsilon-connected ordinal natural V39() real V41() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
y2 is non empty ext-real epsilon-transitive epsilon-connected ordinal natural V39() real Element of the carrier of ()
n is non empty ext-real epsilon-transitive epsilon-connected ordinal natural V39() real Element of the carrier of ()
k is non empty ext-real epsilon-transitive epsilon-connected ordinal natural V39() real Element of the carrier of ()
n "\/" k is non empty ext-real epsilon-transitive epsilon-connected ordinal natural V39() real Element of the carrier of ()
the L_join of () . (n,k) is non empty ext-real epsilon-transitive epsilon-connected ordinal natural V39() real Element of the carrier of ()
[n,k] is set
{n,k} is V24() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered set
{n} is V24() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered set
{{n,k},{n}} is V24() V28() set
the L_join of () . [n,k] is set
n lcm k is ext-real epsilon-transitive epsilon-connected ordinal natural V39() real V41() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
y2 "\/" (n "\/" k) is non empty ext-real epsilon-transitive epsilon-connected ordinal natural V39() real Element of the carrier of ()
the L_join of () . (y2,(n "\/" k)) is non empty ext-real epsilon-transitive epsilon-connected ordinal natural V39() real Element of the carrier of ()
[y2,(n "\/" k)] is set
{y2,(n "\/" k)} is V24() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered set
{y2} is V24() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered set
{{y2,(n "\/" k)},{y2}} is V24() V28() set
the L_join of () . [y2,(n "\/" k)] is set
y2 lcm (n "\/" k) is ext-real epsilon-transitive epsilon-connected ordinal natural V39() real V41() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
y2 "\/" n is non empty ext-real epsilon-transitive epsilon-connected ordinal natural V39() real Element of the carrier of ()
the L_join of () . (y2,n) is non empty ext-real epsilon-transitive epsilon-connected ordinal natural V39() real Element of the carrier of ()
[y2,n] is set
{y2,n} is V24() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered set
{{y2,n},{y2}} is V24() V28() set
the L_join of () . [y2,n] is set
y2 lcm n is ext-real epsilon-transitive epsilon-connected ordinal natural V39() real V41() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
(y2 "\/" n) "\/" k is non empty ext-real epsilon-transitive epsilon-connected ordinal natural V39() real Element of the carrier of ()
the L_join of () . ((y2 "\/" n),k) is non empty ext-real epsilon-transitive epsilon-connected ordinal natural V39() real Element of the carrier of ()
[(y2 "\/" n),k] is set
{(y2 "\/" n),k} is V24() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered set
{(y2 "\/" n)} is V24() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered set
{{(y2 "\/" n),k},{(y2 "\/" n)}} is V24() V28() set
the L_join of () . [(y2 "\/" n),k] is set
(y2 "\/" n) lcm k is ext-real epsilon-transitive epsilon-connected ordinal natural V39() real V41() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
x is non empty ext-real epsilon-transitive epsilon-connected ordinal natural V39() real Element of the carrier of ()
y1 is non empty ext-real epsilon-transitive epsilon-connected ordinal natural V39() real Element of the carrier of ()
x "/\" y1 is non empty ext-real epsilon-transitive epsilon-connected ordinal natural V39() real Element of the carrier of ()
the L_meet of () . (x,y1) is non empty ext-real epsilon-transitive epsilon-connected ordinal natural V39() real Element of the carrier of ()
[x,y1] is set
{x,y1} is V24() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered set
{x} is V24() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered set
{{x,y1},{x}} is V24() V28() set
the L_meet of () . [x,y1] is set
x gcd y1 is ext-real epsilon-transitive epsilon-connected ordinal natural V39() real V41() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
(x "/\" y1) "\/" y1 is non empty ext-real epsilon-transitive epsilon-connected ordinal natural V39() real Element of the carrier of ()
the L_join of () . ((x "/\" y1),y1) is non empty ext-real epsilon-transitive epsilon-connected ordinal natural V39() real Element of the carrier of ()
[(x "/\" y1),y1] is set
{(x "/\" y1),y1} is V24() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered set
{(x "/\" y1)} is V24() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered set
{{(x "/\" y1),y1},{(x "/\" y1)}} is V24() V28() set
the L_join of () . [(x "/\" y1),y1] is set
(x "/\" y1) lcm y1 is ext-real epsilon-transitive epsilon-connected ordinal natural V39() real V41() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
y2 is non empty ext-real epsilon-transitive epsilon-connected ordinal natural V39() real Element of the carrier of ()
n is non empty ext-real epsilon-transitive epsilon-connected ordinal natural V39() real Element of the carrier of ()
y2 "/\" n is non empty ext-real epsilon-transitive epsilon-connected ordinal natural V39() real Element of the carrier of ()
the L_meet of () . (y2,n) is non empty ext-real epsilon-transitive epsilon-connected ordinal natural V39() real Element of the carrier of ()
[y2,n] is set
{y2,n} is V24() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered set
{y2} is V24() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered set
{{y2,n},{y2}} is V24() V28() set
the L_meet of () . [y2,n] is set
y2 gcd n is ext-real epsilon-transitive epsilon-connected ordinal natural V39() real V41() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
n "/\" y2 is non empty ext-real epsilon-transitive epsilon-connected ordinal natural V39() real Element of the carrier of ()
the L_meet of () . (n,y2) is non empty ext-real epsilon-transitive epsilon-connected ordinal natural V39() real Element of the carrier of ()
[n,y2] is set
{n,y2} is V24() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered set
{n} is V24() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered set
{{n,y2},{n}} is V24() V28() set
the L_meet of () . [n,y2] is set
n gcd y2 is ext-real epsilon-transitive epsilon-connected ordinal natural V39() real V41() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
x is non empty ext-real epsilon-transitive epsilon-connected ordinal natural V39() real Element of the carrier of ()
y1 is non empty ext-real epsilon-transitive epsilon-connected ordinal natural V39() real Element of the carrier of ()
y2 is non empty ext-real epsilon-transitive epsilon-connected ordinal natural V39() real Element of the carrier of ()
y1 "/\" y2 is non empty ext-real epsilon-transitive epsilon-connected ordinal natural V39() real Element of the carrier of ()
the L_meet of () . (y1,y2) is non empty ext-real epsilon-transitive epsilon-connected ordinal natural V39() real Element of the carrier of ()
[y1,y2] is set
{y1,y2} is V24() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered set
{y1} is V24() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered set
{{y1,y2},{y1}} is V24() V28() set
the L_meet of () . [y1,y2] is set
y1 gcd y2 is ext-real epsilon-transitive epsilon-connected ordinal natural V39() real V41() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
x "/\" (y1 "/\" y2) is non empty ext-real epsilon-transitive epsilon-connected ordinal natural V39() real Element of the carrier of ()
the L_meet of () . (x,(y1 "/\" y2)) is non empty ext-real epsilon-transitive epsilon-connected ordinal natural V39() real Element of the carrier of ()
[x,(y1 "/\" y2)] is set
{x,(y1 "/\" y2)} is V24() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered set
{x} is V24() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered set
{{x,(y1 "/\" y2)},{x}} is V24() V28() set
the L_meet of () . [x,(y1 "/\" y2)] is set
x gcd (y1 "/\" y2) is ext-real epsilon-transitive epsilon-connected ordinal natural V39() real V41() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
x "/\" y1 is non empty ext-real epsilon-transitive epsilon-connected ordinal natural V39() real Element of the carrier of ()
the L_meet of () . (x,y1) is non empty ext-real epsilon-transitive epsilon-connected ordinal natural V39() real Element of the carrier of ()
[x,y1] is set
{x,y1} is V24() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered set
{{x,y1},{x}} is V24() V28() set
the L_meet of () . [x,y1] is set
x gcd y1 is ext-real epsilon-transitive epsilon-connected ordinal natural V39() real V41() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
(x "/\" y1) "/\" y2 is non empty ext-real epsilon-transitive epsilon-connected ordinal natural V39() real Element of the carrier of ()
the L_meet of () . ((x "/\" y1),y2) is non empty ext-real epsilon-transitive epsilon-connected ordinal natural V39() real Element of the carrier of ()
[(x "/\" y1),y2] is set
{(x "/\" y1),y2} is V24() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered set
{(x "/\" y1)} is V24() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered set
{{(x "/\" y1),y2},{(x "/\" y1)}} is V24() V28() set
the L_meet of () . [(x "/\" y1),y2] is set
(x "/\" y1) gcd y2 is ext-real epsilon-transitive epsilon-connected ordinal natural V39() real V41() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
n is non empty ext-real epsilon-transitive epsilon-connected ordinal natural V39() real Element of the carrier of ()
k is non empty ext-real epsilon-transitive epsilon-connected ordinal natural V39() real Element of the carrier of ()
n "\/" k is non empty ext-real epsilon-transitive epsilon-connected ordinal natural V39() real Element of the carrier of ()
the L_join of () . (n,k) is non empty ext-real epsilon-transitive epsilon-connected ordinal natural V39() real Element of the carrier of ()
[n,k] is set
{n,k} is V24() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered set
{n} is V24() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered set
{{n,k},{n}} is V24() V28() set
the L_join of () . [n,k] is set
n lcm k is ext-real epsilon-transitive epsilon-connected ordinal natural V39() real V41() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
n "/\" (n "\/" k) is non empty ext-real epsilon-transitive epsilon-connected ordinal natural V39() real Element of the carrier of ()
the L_meet of () . (n,(n "\/" k)) is non empty ext-real epsilon-transitive epsilon-connected ordinal natural V39() real Element of the carrier of ()
[n,(n "\/" k)] is set
{n,(n "\/" k)} is V24() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered set
{{n,(n "\/" k)},{n}} is V24() V28() set
the L_meet of () . [n,(n "\/" k)] is set
n gcd (n "\/" k) is ext-real epsilon-transitive epsilon-connected ordinal natural V39() real V41() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
x is non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like LattStr
the carrier of x is non empty set
[: the carrier of x, the carrier of x:] is set
the L_join of x is Relation-like [: the carrier of x, the carrier of x:] -defined the carrier of x -valued Function-like V18([: the carrier of x, the carrier of x:], the carrier of x) Element of bool [:[: the carrier of x, the carrier of x:], the carrier of x:]
[:[: the carrier of x, the carrier of x:], the carrier of x:] is set
bool [:[: the carrier of x, the carrier of x:], the carrier of x:] is set
dom the L_join of x is Relation-like set
the L_join of x || the carrier of x is set
the L_join of x | [: the carrier of x, the carrier of x:] is Relation-like set
the L_meet of x is Relation-like [: the carrier of x, the carrier of x:] -defined the carrier of x -valued Function-like V18([: the carrier of x, the carrier of x:], the carrier of x) Element of bool [:[: the carrier of x, the carrier of x:], the carrier of x:]
dom the L_meet of x is Relation-like set
the L_meet of x || the carrier of x is set
the L_meet of x | [: the carrier of x, the carrier of x:] is Relation-like set
x is non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like LattStr
the carrier of x is non empty set
the L_join of x is Relation-like [: the carrier of x, the carrier of x:] -defined the carrier of x -valued Function-like V18([: the carrier of x, the carrier of x:], the carrier of x) Element of bool [:[: the carrier of x, the carrier of x:], the carrier of x:]
[: the carrier of x, the carrier of x:] is set
[:[: the carrier of x, the carrier of x:], the carrier of x:] is set
bool [:[: the carrier of x, the carrier of x:], the carrier of x:] is set
the L_meet of x is Relation-like [: the carrier of x, the carrier of x:] -defined the carrier of x -valued Function-like V18([: the carrier of x, the carrier of x:], the carrier of x) Element of bool [:[: the carrier of x, the carrier of x:], the carrier of x:]
the L_join of x || the carrier of x is set
the L_join of x | [: the carrier of x, the carrier of x:] is Relation-like set
the L_meet of x || the carrier of x is set
the L_meet of x | [: the carrier of x, the carrier of x:] is Relation-like set
x is non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like LattStr
the carrier of x is non empty set
the L_join of x is Relation-like [: the carrier of x, the carrier of x:] -defined the carrier of x -valued Function-like V18([: the carrier of x, the carrier of x:], the carrier of x) Element of bool [:[: the carrier of x, the carrier of x:], the carrier of x:]
[: the carrier of x, the carrier of x:] is set
[:[: the carrier of x, the carrier of x:], the carrier of x:] is set
bool [:[: the carrier of x, the carrier of x:], the carrier of x:] is set
the L_meet of x is Relation-like [: the carrier of x, the carrier of x:] -defined the carrier of x -valued Function-like V18([: the carrier of x, the carrier of x:], the carrier of x) Element of bool [:[: the carrier of x, the carrier of x:], the carrier of x:]
LattStr(# the carrier of x, the L_join of x, the L_meet of x #) is non empty strict LattStr
the carrier of LattStr(# the carrier of x, the L_join of x, the L_meet of x #) is non empty set
y2 is Element of the carrier of LattStr(# the carrier of x, the L_join of x, the L_meet of x #)
n is Element of the carrier of LattStr(# the carrier of x, the L_join of x, the L_meet of x #)
k is Element of the carrier of LattStr(# the carrier of x, the L_join of x, the L_meet of x #)
n "\/" k is Element of the carrier of LattStr(# the carrier of x, the L_join of x, the L_meet of x #)
the L_join of LattStr(# the carrier of x, the L_join of x, the L_meet of x #) is Relation-like [: the carrier of LattStr(# the carrier of x, the L_join of x, the L_meet of x #), the carrier of LattStr(# the carrier of x, the L_join of x, the L_meet of x #):] -defined the carrier of LattStr(# the carrier of x, the L_join of x, the L_meet of x #) -valued Function-like V18([: the carrier of LattStr(# the carrier of x, the L_join of x, the L_meet of x #), the carrier of LattStr(# the carrier of x, the L_join of x, the L_meet of x #):], the carrier of LattStr(# the carrier of x, the L_join of x, the L_meet of x #)) Element of bool [:[: the carrier of LattStr(# the carrier of x, the L_join of x, the L_meet of x #), the carrier of LattStr(# the carrier of x, the L_join of x, the L_meet of x #):], the carrier of LattStr(# the carrier of x, the L_join of x, the L_meet of x #):]
[: the carrier of LattStr(# the carrier of x, the L_join of x, the L_meet of x #), the carrier of LattStr(# the carrier of x, the L_join of x, the L_meet of x #):] is set
[:[: the carrier of LattStr(# the carrier of x, the L_join of x, the L_meet of x #), the carrier of LattStr(# the carrier of x, the L_join of x, the L_meet of x #):], the carrier of LattStr(# the carrier of x, the L_join of x, the L_meet of x #):] is set
bool [:[: the carrier of LattStr(# the carrier of x, the L_join of x, the L_meet of x #), the carrier of LattStr(# the carrier of x, the L_join of x, the L_meet of x #):], the carrier of LattStr(# the carrier of x, the L_join of x, the L_meet of x #):] is set
the L_join of LattStr(# the carrier of x, the L_join of x, the L_meet of x #) . (n,k) is Element of the carrier of LattStr(# the carrier of x, the L_join of x, the L_meet of x #)
[n,k] is set
{n,k} is V24() set
{n} is V24() set
{{n,k},{n}} is V24() V28() set
the L_join of LattStr(# the carrier of x, the L_join of x, the L_meet of x #) . [n,k] is set
y2 "\/" (n "\/" k) is Element of the carrier of LattStr(# the carrier of x, the L_join of x, the L_meet of x #)
the L_join of LattStr(# the carrier of x, the L_join of x, the L_meet of x #) . (y2,(n "\/" k)) is Element of the carrier of LattStr(# the carrier of x, the L_join of x, the L_meet of x #)
[y2,(n "\/" k)] is set
{y2,(n "\/" k)} is V24() set
{y2} is V24() set
{{y2,(n "\/" k)},{y2}} is V24() V28() set
the L_join of LattStr(# the carrier of x, the L_join of x, the L_meet of x #) . [y2,(n "\/" k)] is set
n is Element of the carrier of x
k is Element of the carrier of x
c9 is Element of the carrier of x
k "\/" c9 is Element of the carrier of x
the L_join of x . (k,c9) is Element of the carrier of x
[k,c9] is set
{k,c9} is V24() set
{k} is V24() set
{{k,c9},{k}} is V24() V28() set
the L_join of x . [k,c9] is set
n "\/" (k "\/" c9) is Element of the carrier of x
the L_join of x . (n,(k "\/" c9)) is Element of the carrier of x
[n,(k "\/" c9)] is set
{n,(k "\/" c9)} is V24() set
{n} is V24() set
{{n,(k "\/" c9)},{n}} is V24() V28() set
the L_join of x . [n,(k "\/" c9)] is set
n "\/" k is Element of the carrier of x
the L_join of x . (n,k) is Element of the carrier of x
[n,k] is set
{n,k} is V24() set
{{n,k},{n}} is V24() V28() set
the L_join of x . [n,k] is set
(n "\/" k) "\/" c9 is Element of the carrier of x
the L_join of x . ((n "\/" k),c9) is Element of the carrier of x
[(n "\/" k),c9] is set
{(n "\/" k),c9} is V24() set
{(n "\/" k)} is V24() set
{{(n "\/" k),c9},{(n "\/" k)}} is V24() V28() set
the L_join of x . [(n "\/" k),c9] is set
y2 "\/" n is Element of the carrier of LattStr(# the carrier of x, the L_join of x, the L_meet of x #)
the L_join of LattStr(# the carrier of x, the L_join of x, the L_meet of x #) . (y2,n) is Element of the carrier of LattStr(# the carrier of x, the L_join of x, the L_meet of x #)
[y2,n] is set
{y2,n} is V24() set
{{y2,n},{y2}} is V24() V28() set
the L_join of LattStr(# the carrier of x, the L_join of x, the L_meet of x #) . [y2,n] is set
(y2 "\/" n) "\/" k is Element of the carrier of LattStr(# the carrier of x, the L_join of x, the L_meet of x #)
the L_join of LattStr(# the carrier of x, the L_join of x, the L_meet of x #) . ((y2 "\/" n),k) is Element of the carrier of LattStr(# the carrier of x, the L_join of x, the L_meet of x #)
[(y2 "\/" n),k] is set
{(y2 "\/" n),k} is V24() set
{(y2 "\/" n)} is V24() set
{{(y2 "\/" n),k},{(y2 "\/" n)}} is V24() V28() set
the L_join of LattStr(# the carrier of x, the L_join of x, the L_meet of x #) . [(y2 "\/" n),k] is set
y2 is Element of the carrier of LattStr(# the carrier of x, the L_join of x, the L_meet of x #)
n is Element of the carrier of LattStr(# the carrier of x, the L_join of x, the L_meet of x #)
y2 "/\" n is Element of the carrier of LattStr(# the carrier of x, the L_join of x, the L_meet of x #)
the L_meet of LattStr(# the carrier of x, the L_join of x, the L_meet of x #) is Relation-like [: the carrier of LattStr(# the carrier of x, the L_join of x, the L_meet of x #), the carrier of LattStr(# the carrier of x, the L_join of x, the L_meet of x #):] -defined the carrier of LattStr(# the carrier of x, the L_join of x, the L_meet of x #) -valued Function-like V18([: the carrier of LattStr(# the carrier of x, the L_join of x, the L_meet of x #), the carrier of LattStr(# the carrier of x, the L_join of x, the L_meet of x #):], the carrier of LattStr(# the carrier of x, the L_join of x, the L_meet of x #)) Element of bool [:[: the carrier of LattStr(# the carrier of x, the L_join of x, the L_meet of x #), the carrier of LattStr(# the carrier of x, the L_join of x, the L_meet of x #):], the carrier of LattStr(# the carrier of x, the L_join of x, the L_meet of x #):]
the L_meet of LattStr(# the carrier of x, the L_join of x, the L_meet of x #) . (y2,n) is Element of the carrier of LattStr(# the carrier of x, the L_join of x, the L_meet of x #)
[y2,n] is set
{y2,n} is V24() set
{y2} is V24() set
{{y2,n},{y2}} is V24() V28() set
the L_meet of LattStr(# the carrier of x, the L_join of x, the L_meet of x #) . [y2,n] is set
(y2 "/\" n) "\/" n is Element of the carrier of LattStr(# the carrier of x, the L_join of x, the L_meet of x #)
the L_join of LattStr(# the carrier of x, the L_join of x, the L_meet of x #) . ((y2 "/\" n),n) is Element of the carrier of LattStr(# the carrier of x, the L_join of x, the L_meet of x #)
[(y2 "/\" n),n] is set
{(y2 "/\" n),n} is V24() set
{(y2 "/\" n)} is V24() set
{{(y2 "/\" n),n},{(y2 "/\" n)}} is V24() V28() set
the L_join of LattStr(# the carrier of x, the L_join of x, the L_meet of x #) . [(y2 "/\" n),n] is set
k is Element of the carrier of x
n is Element of the carrier of x
k "/\" n is Element of the carrier of x
the L_meet of x . (k,n) is Element of the carrier of x
[k,n] is set
{k,n} is V24() set
{k} is V24() set
{{k,n},{k}} is V24() V28() set
the L_meet of x . [k,n] is set
(k "/\" n) "\/" n is Element of the carrier of x
the L_join of x . ((k "/\" n),n) is Element of the carrier of x
[(k "/\" n),n] is set
{(k "/\" n),n} is V24() set
{(k "/\" n)} is V24() set
{{(k "/\" n),n},{(k "/\" n)}} is V24() V28() set
the L_join of x . [(k "/\" n),n] is set
y2 is Element of the carrier of LattStr(# the carrier of x, the L_join of x, the L_meet of x #)
n is Element of the carrier of LattStr(# the carrier of x, the L_join of x, the L_meet of x #)
y2 "\/" n is Element of the carrier of LattStr(# the carrier of x, the L_join of x, the L_meet of x #)
the L_join of LattStr(# the carrier of x, the L_join of x, the L_meet of x #) . (y2,n) is Element of the carrier of LattStr(# the carrier of x, the L_join of x, the L_meet of x #)
[y2,n] is set
{y2,n} is V24() set
{y2} is V24() set
{{y2,n},{y2}} is V24() V28() set
the L_join of LattStr(# the carrier of x, the L_join of x, the L_meet of x #) . [y2,n] is set
y2 "/\" (y2 "\/" n) is Element of the carrier of LattStr(# the carrier of x, the L_join of x, the L_meet of x #)
the L_meet of LattStr(# the carrier of x, the L_join of x, the L_meet of x #) . (y2,(y2 "\/" n)) is Element of the carrier of LattStr(# the carrier of x, the L_join of x, the L_meet of x #)
[y2,(y2 "\/" n)] is set
{y2,(y2 "\/" n)} is V24() set
{{y2,(y2 "\/" n)},{y2}} is V24() V28() set
the L_meet of LattStr(# the carrier of x, the L_join of x, the L_meet of x #) . [y2,(y2 "\/" n)] is set
k is Element of the carrier of x
n is Element of the carrier of x
k "\/" n is Element of the carrier of x
the L_join of x . (k,n) is Element of the carrier of x
[k,n] is set
{k,n} is V24() set
{k} is V24() set
{{k,n},{k}} is V24() V28() set
the L_join of x . [k,n] is set
k "/\" (k "\/" n) is Element of the carrier of x
the L_meet of x . (k,(k "\/" n)) is Element of the carrier of x
[k,(k "\/" n)] is set
{k,(k "\/" n)} is V24() set
{{k,(k "\/" n)},{k}} is V24() V28() set
the L_meet of x . [k,(k "\/" n)] is set
y2 is Element of the carrier of LattStr(# the carrier of x, the L_join of x, the L_meet of x #)
n is Element of the carrier of LattStr(# the carrier of x, the L_join of x, the L_meet of x #)
k is Element of the carrier of LattStr(# the carrier of x, the L_join of x, the L_meet of x #)
n "/\" k is Element of the carrier of LattStr(# the carrier of x, the L_join of x, the L_meet of x #)
the L_meet of LattStr(# the carrier of x, the L_join of x, the L_meet of x #) . (n,k) is Element of the carrier of LattStr(# the carrier of x, the L_join of x, the L_meet of x #)
[n,k] is set
{n,k} is V24() set
{n} is V24() set
{{n,k},{n}} is V24() V28() set
the L_meet of LattStr(# the carrier of x, the L_join of x, the L_meet of x #) . [n,k] is set
y2 "/\" (n "/\" k) is Element of the carrier of LattStr(# the carrier of x, the L_join of x, the L_meet of x #)
the L_meet of LattStr(# the carrier of x, the L_join of x, the L_meet of x #) . (y2,(n "/\" k)) is Element of the carrier of LattStr(# the carrier of x, the L_join of x, the L_meet of x #)
[y2,(n "/\" k)] is set
{y2,(n "/\" k)} is V24() set
{y2} is V24() set
{{y2,(n "/\" k)},{y2}} is V24() V28() set
the L_meet of LattStr(# the carrier of x, the L_join of x, the L_meet of x #) . [y2,(n "/\" k)] is set
n is Element of the carrier of x
k is Element of the carrier of x
c9 is Element of the carrier of x
k "/\" c9 is Element of the carrier of x
the L_meet of x . (k,c9) is Element of the carrier of x
[k,c9] is set
{k,c9} is V24() set
{k} is V24() set
{{k,c9},{k}} is V24() V28() set
the L_meet of x . [k,c9] is set
n "/\" (k "/\" c9) is Element of the carrier of x
the L_meet of x . (n,(k "/\" c9)) is Element of the carrier of x
[n,(k "/\" c9)] is set
{n,(k "/\" c9)} is V24() set
{n} is V24() set
{{n,(k "/\" c9)},{n}} is V24() V28() set
the L_meet of x . [n,(k "/\" c9)] is set
n "/\" k is Element of the carrier of x
the L_meet of x . (n,k) is Element of the carrier of x
[n,k] is set
{n,k} is V24() set
{{n,k},{n}} is V24() V28() set
the L_meet of x . [n,k] is set
(n "/\" k) "/\" c9 is Element of the carrier of x
the L_meet of x . ((n "/\" k),c9) is Element of the carrier of x
[(n "/\" k),c9] is set
{(n "/\" k),c9} is V24() set
{(n "/\" k)} is V24() set
{{(n "/\" k),c9},{(n "/\" k)}} is V24() V28() set
the L_meet of x . [(n "/\" k),c9] is set
y2 "/\" n is Element of the carrier of LattStr(# the carrier of x, the L_join of x, the L_meet of x #)
the L_meet of LattStr(# the carrier of x, the L_join of x, the L_meet of x #) . (y2,n) is Element of the carrier of LattStr(# the carrier of x, the L_join of x, the L_meet of x #)
[y2,n] is set
{y2,n} is V24() set
{{y2,n},{y2}} is V24() V28() set
the L_meet of LattStr(# the carrier of x, the L_join of x, the L_meet of x #) . [y2,n] is set
(y2 "/\" n) "/\" k is Element of the carrier of LattStr(# the carrier of x, the L_join of x, the L_meet of x #)
the L_meet of LattStr(# the carrier of x, the L_join of x, the L_meet of x #) . ((y2 "/\" n),k) is Element of the carrier of LattStr(# the carrier of x, the L_join of x, the L_meet of x #)
[(y2 "/\" n),k] is set
{(y2 "/\" n),k} is V24() set
{(y2 "/\" n)} is V24() set
{{(y2 "/\" n),k},{(y2 "/\" n)}} is V24() V28() set
the L_meet of LattStr(# the carrier of x, the L_join of x, the L_meet of x #) . [(y2 "/\" n),k] is set
y2 is Element of the carrier of LattStr(# the carrier of x, the L_join of x, the L_meet of x #)
k is Element of the carrier of x
n is Element of the carrier of LattStr(# the carrier of x, the L_join of x, the L_meet of x #)
n is Element of the carrier of x
y2 "\/" n is Element of the carrier of LattStr(# the carrier of x, the L_join of x, the L_meet of x #)
the L_join of LattStr(# the carrier of x, the L_join of x, the L_meet of x #) . (y2,n) is Element of the carrier of LattStr(# the carrier of x, the L_join of x, the L_meet of x #)
[y2,n] is set
{y2,n} is V24() set
{y2} is V24() set
{{y2,n},{y2}} is V24() V28() set
the L_join of LattStr(# the carrier of x, the L_join of x, the L_meet of x #) . [y2,n] is set
k "\/" n is Element of the carrier of x
the L_join of x . (k,n) is Element of the carrier of x
[k,n] is set
{k,n} is V24() set
{k} is V24() set
{{k,n},{k}} is V24() V28() set
the L_join of x . [k,n] is set
y2 "/\" n is Element of the carrier of LattStr(# the carrier of x, the L_join of x, the L_meet of x #)
the L_meet of LattStr(# the carrier of x, the L_join of x, the L_meet of x #) . (y2,n) is Element of the carrier of LattStr(# the carrier of x, the L_join of x, the L_meet of x #)
the L_meet of LattStr(# the carrier of x, the L_join of x, the L_meet of x #) . [y2,n] is set
k "/\" n is Element of the carrier of x
the L_meet of x . (k,n) is Element of the carrier of x
the L_meet of x . [k,n] is set
y2 is Element of the carrier of LattStr(# the carrier of x, the L_join of x, the L_meet of x #)
n is Element of the carrier of LattStr(# the carrier of x, the L_join of x, the L_meet of x #)
y2 "/\" n is Element of the carrier of LattStr(# the carrier of x, the L_join of x, the L_meet of x #)
the L_meet of LattStr(# the carrier of x, the L_join of x, the L_meet of x #) . (y2,n) is Element of the carrier of LattStr(# the carrier of x, the L_join of x, the L_meet of x #)
[y2,n] is set
{y2,n} is V24() set
{y2} is V24() set
{{y2,n},{y2}} is V24() V28() set
the L_meet of LattStr(# the carrier of x, the L_join of x, the L_meet of x #) . [y2,n] is set
n is Element of the carrier of x
k is Element of the carrier of x
n "/\" k is Element of the carrier of x
the L_meet of x . (n,k) is Element of the carrier of x
[n,k] is set
{n,k} is V24() set
{n} is V24() set
{{n,k},{n}} is V24() V28() set
the L_meet of x . [n,k] is set
n "/\" y2 is Element of the carrier of LattStr(# the carrier of x, the L_join of x, the L_meet of x #)
the L_meet of LattStr(# the carrier of x, the L_join of x, the L_meet of x #) . (n,y2) is Element of the carrier of LattStr(# the carrier of x, the L_join of x, the L_meet of x #)
[n,y2] is set
{n,y2} is V24() set
{n} is V24() set
{{n,y2},{n}} is V24() V28() set
the L_meet of LattStr(# the carrier of x, the L_join of x, the L_meet of x #) . [n,y2] is set
y2 is Element of the carrier of LattStr(# the carrier of x, the L_join of x, the L_meet of x #)
n is Element of the carrier of LattStr(# the carrier of x, the L_join of x, the L_meet of x #)
y2 "\/" n is Element of the carrier of LattStr(# the carrier of x, the L_join of x, the L_meet of x #)
the L_join of LattStr(# the carrier of x, the L_join of x, the L_meet of x #) . (y2,n) is Element of the carrier of LattStr(# the carrier of x, the L_join of x, the L_meet of x #)
[y2,n] is set
{y2,n} is V24() set
{y2} is V24() set
{{y2,n},{y2}} is V24() V28() set
the L_join of LattStr(# the carrier of x, the L_join of x, the L_meet of x #) . [y2,n] is set
n is Element of the carrier of x
k is Element of the carrier of x
n "\/" k is Element of the carrier of x
the L_join of x . (n,k) is Element of the carrier of x
[n,k] is set
{n,k} is V24() set
{n} is V24() set
{{n,k},{n}} is V24() V28() set
the L_join of x . [n,k] is set
n "\/" y2 is Element of the carrier of LattStr(# the carrier of x, the L_join of x, the L_meet of x #)
the L_join of LattStr(# the carrier of x, the L_join of x, the L_meet of x #) . (n,y2) is Element of the carrier of LattStr(# the carrier of x, the L_join of x, the L_meet of x #)
[n,y2] is set
{n,y2} is V24() set
{n} is V24() set
{{n,y2},{n}} is V24() V28() set
the L_join of LattStr(# the carrier of x, the L_join of x, the L_meet of x #) . [n,y2] is set
y2 is non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like LattStr
the L_join of y2 is Relation-like [: the carrier of y2, the carrier of y2:] -defined the carrier of y2 -valued Function-like V18([: the carrier of y2, the carrier of y2:], the carrier of y2) Element of bool [:[: the carrier of y2, the carrier of y2:], the carrier of y2:]
the carrier of y2 is non empty set
[: the carrier of y2, the carrier of y2:] is set
[:[: the carrier of y2, the carrier of y2:], the carrier of y2:] is set
bool [:[: the carrier of y2, the carrier of y2:], the carrier of y2:] is set
the L_join of x || the carrier of y2 is set
the L_join of x | [: the carrier of y2, the carrier of y2:] is Relation-like set
the L_meet of y2 is Relation-like [: the carrier of y2, the carrier of y2:] -defined the carrier of y2 -valued Function-like V18([: the carrier of y2, the carrier of y2:], the carrier of y2) Element of bool [:[: the carrier of y2, the carrier of y2:], the carrier of y2:]
the L_meet of x || the carrier of y2 is set
the L_meet of x | [: the carrier of y2, the carrier of y2:] is Relation-like set
x is non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like LattStr
the carrier of x is non empty set
the L_join of x is Relation-like [: the carrier of x, the carrier of x:] -defined the carrier of x -valued Function-like V18([: the carrier of x, the carrier of x:], the carrier of x) Element of bool [:[: the carrier of x, the carrier of x:], the carrier of x:]
[: the carrier of x, the carrier of x:] is set
[:[: the carrier of x, the carrier of x:], the carrier of x:] is set
bool [:[: the carrier of x, the carrier of x:], the carrier of x:] is set
the L_join of x || the carrier of x is set
the L_join of x | [: the carrier of x, the carrier of x:] is Relation-like set
the L_meet of x is Relation-like [: the carrier of x, the carrier of x:] -defined the carrier of x -valued Function-like V18([: the carrier of x, the carrier of x:], the carrier of x) Element of bool [:[: the carrier of x, the carrier of x:], the carrier of x:]
the L_meet of x || the carrier of x is set
the L_meet of x | [: the carrier of x, the carrier of x:] is Relation-like set
dom () is Relation-like set
x is set
() . x is set
() . x is set
y1 is set
y2 is set
[y1,y2] is set
{y1,y2} is V24() set
{y1} is V24() set
{{y1,y2},{y1}} is V24() V28() set
n is ext-real epsilon-transitive epsilon-connected ordinal natural V39() real set
k is ext-real epsilon-transitive epsilon-connected ordinal natural V39() real set
() . (n,k) is set
[n,k] is set
{n,k} is V24() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered set
{n} is V24() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered set
{{n,k},{n}} is V24() V28() set
() . [n,k] is set
n gcd k is ext-real epsilon-transitive epsilon-connected ordinal natural V39() real V41() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
n is non empty ext-real epsilon-transitive epsilon-connected ordinal natural V39() real V41() Element of ()
k is non empty ext-real epsilon-transitive epsilon-connected ordinal natural V39() real V41() Element of ()
() . (n,k) is non empty ext-real epsilon-transitive epsilon-connected ordinal natural V39() real V41() Element of ()
[n,k] is set
{n,k} is V24() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered set
{n} is V24() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered set
{{n,k},{n}} is V24() V28() set
() . [n,k] is set
() . (n,k) is ext-real epsilon-transitive epsilon-connected ordinal natural V39() real V41() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
() . [n,k] is set
dom () is Relation-like set
(dom ()) /\ [:(),():] is set
() || () is set
() | [:(),():] is Relation-like set
dom () is Relation-like set
x is set
() . x is set
() . x is set
y1 is set
y2 is set
[y1,y2] is set
{y1,y2} is V24() set
{y1} is V24() set
{{y1,y2},{y1}} is V24() V28() set
n is ext-real epsilon-transitive epsilon-connected ordinal natural V39() real set
k is ext-real epsilon-transitive epsilon-connected ordinal natural V39() real set
() . (n,k) is set
[n,k] is set
{n,k} is V24() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered set
{n} is V24() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered set
{{n,k},{n}} is V24() V28() set
() . [n,k] is set
n lcm k is ext-real epsilon-transitive epsilon-connected ordinal natural V39() real V41() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
n is non empty ext-real epsilon-transitive epsilon-connected ordinal natural V39() real V41() Element of ()
k is non empty ext-real epsilon-transitive epsilon-connected ordinal natural V39() real V41() Element of ()
() . (n,k) is non empty ext-real epsilon-transitive epsilon-connected ordinal natural V39() real V41() Element of ()
[n,k] is set
{n,k} is V24() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered set
{n} is V24() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered set
{{n,k},{n}} is V24() V28() set
() . [n,k] is set
() . (n,k) is ext-real epsilon-transitive epsilon-connected ordinal natural V39() real V41() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
() . [n,k] is set
dom () is Relation-like set
(dom ()) /\ [:(),():] is set
() || () is set
() | [:(),():] is Relation-like set