:: 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

c9 "/\" c

the L_meet of () . (c9,c

[c9,c

{c9,c

{c9} is V24() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered set

{{c9,c

the L_meet of () . [c9,c

c9 gcd c

c

the L_meet of () . (c

[c

{c

{c

{{c

the L_meet of () . [c

c

c

c

c

c

the L_meet of () . (c

[c

{c

{c

{{c

the L_meet of () . [c

c

c

the L_meet of () . (c

[c

{c

{c

{{c

the L_meet of () . [c

c

c

the L_meet of () . (c

[c

{c

{{c

the L_meet of () . [c

c

(c

the L_meet of () . ((c

[(c

{(c

{(c

{{(c

the L_meet of () . [(c

(c

c

c

c

the L_join of () . (c

[c

{c

{c

{{c

the L_join of () . [c

c

c

the L_meet of () . (c

[c

{c

{{c

the L_meet of () . [c

c

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