:: YELLOW10 semantic presentation

K260() is M2( bool K256())
K256() is set
bool K256() is non empty set
K112() is set
bool K112() is non empty set
bool K260() is non empty set
{} is empty V7() V8() V9() set
the empty V7() V8() V9() set is empty V7() V8() V9() set
1 is non empty set
S is non empty upper-bounded RelStr
T is non empty upper-bounded RelStr
[:S,T:] is non empty strict RelStr
the carrier of T is non empty set
x is M2( the carrier of T)
the carrier of S is non empty set
y is M2( the carrier of S)
[y,x] is V1() M2( the carrier of [:S,T:])
the carrier of [:S,T:] is non empty set
{y,x} is non empty set
{y} is non empty set
{{y,x},{y}} is non empty set
[: the carrier of S, the carrier of T:] is non empty V7() set
S is non empty lower-bounded RelStr
T is non empty lower-bounded RelStr
[:S,T:] is non empty strict RelStr
the carrier of T is non empty set
x is M2( the carrier of T)
the carrier of S is non empty set
y is M2( the carrier of S)
[y,x] is V1() M2( the carrier of [:S,T:])
the carrier of [:S,T:] is non empty set
{y,x} is non empty set
{y} is non empty set
{{y,x},{y}} is non empty set
[: the carrier of S, the carrier of T:] is non empty V7() set
S is non empty RelStr
T is non empty RelStr
[:S,T:] is non empty strict RelStr
the carrier of [:S,T:] is non empty set
x is M2( the carrier of [:S,T:])
the carrier of S is non empty set
the carrier of T is non empty set
[: the carrier of S, the carrier of T:] is non empty V7() set
y is set
y is set
[y,y] is V1() set
{y,y} is non empty set
{y} is non empty set
{{y,y},{y}} is non empty set
ST is M2( the carrier of S)
s9 is M2( the carrier of T)
[ST,s9] is V1() M2( the carrier of [:S,T:])
{ST,s9} is non empty set
{ST} is non empty set
{{ST,s9},{ST}} is non empty set
S is non empty RelStr
T is non empty RelStr
[:S,T:] is non empty strict RelStr
the carrier of [:S,T:] is non empty set
x is M2( the carrier of [:S,T:])
the carrier of S is non empty set
the carrier of T is non empty set
[: the carrier of S, the carrier of T:] is non empty V7() set
y is set
y is set
[y,y] is V1() set
{y,y} is non empty set
{y} is non empty set
{{y,y},{y}} is non empty set
ST is M2( the carrier of S)
s9 is M2( the carrier of T)
[ST,s9] is V1() M2( the carrier of [:S,T:])
{ST,s9} is non empty set
{ST} is non empty set
{{ST,s9},{ST}} is non empty set
S is non empty antisymmetric upper-bounded RelStr
T is non empty antisymmetric upper-bounded RelStr
[:S,T:] is non empty strict antisymmetric upper-bounded RelStr
Top [:S,T:] is M2( the carrier of [:S,T:])
the carrier of [:S,T:] is non empty set
"/\" ({},[:S,T:]) is M2( the carrier of [:S,T:])
Top S is M2( the carrier of S)
the carrier of S is non empty set
"/\" ({},S) is M2( the carrier of S)
Top T is M2( the carrier of T)
the carrier of T is non empty set
"/\" ({},T) is M2( the carrier of T)
[(Top S),(Top T)] is V1() M2( the carrier of [:S,T:])
{(Top S),(Top T)} is non empty set
{(Top S)} is non empty set
{{(Top S),(Top T)},{(Top S)}} is non empty set
x is M2( the carrier of [:S,T:])
[: the carrier of S, the carrier of T:] is non empty V7() set
y is set
y is set
[y,y] is V1() set
{y,y} is non empty set
{y} is non empty set
{{y,y},{y}} is non empty set
ST is M2( the carrier of S)
s9 is M2( the carrier of T)
S is non empty antisymmetric lower-bounded RelStr
T is non empty antisymmetric lower-bounded RelStr
[:S,T:] is non empty strict antisymmetric lower-bounded RelStr
Bottom [:S,T:] is M2( the carrier of [:S,T:])
the carrier of [:S,T:] is non empty set
"\/" ({},[:S,T:]) is M2( the carrier of [:S,T:])
Bottom S is M2( the carrier of S)
the carrier of S is non empty set
"\/" ({},S) is M2( the carrier of S)
Bottom T is M2( the carrier of T)
the carrier of T is non empty set
"\/" ({},T) is M2( the carrier of T)
[(Bottom S),(Bottom T)] is V1() M2( the carrier of [:S,T:])
{(Bottom S),(Bottom T)} is non empty set
{(Bottom S)} is non empty set
{{(Bottom S),(Bottom T)},{(Bottom S)}} is non empty set
x is M2( the carrier of [:S,T:])
[: the carrier of S, the carrier of T:] is non empty V7() set
y is set
y is set
[y,y] is V1() set
{y,y} is non empty set
{y} is non empty set
{{y,y},{y}} is non empty set
ST is M2( the carrier of S)
s9 is M2( the carrier of T)
S is non empty antisymmetric lower-bounded RelStr
T is non empty antisymmetric lower-bounded RelStr
[:S,T:] is non empty strict antisymmetric lower-bounded RelStr
the carrier of [:S,T:] is non empty set
bool the carrier of [:S,T:] is non empty set
x is M2( bool the carrier of [:S,T:])
"\/" (x,[:S,T:]) is M2( the carrier of [:S,T:])
proj1 x is M2( bool the carrier of S)
the carrier of S is non empty set
bool the carrier of S is non empty set
"\/" ((proj1 x),S) is M2( the carrier of S)
proj2 x is M2( bool the carrier of T)
the carrier of T is non empty set
bool the carrier of T is non empty set
"\/" ((proj2 x),T) is M2( the carrier of T)
[("\/" ((proj1 x),S)),("\/" ((proj2 x),T))] is V1() M2( the carrier of [:S,T:])
{("\/" ((proj1 x),S)),("\/" ((proj2 x),T))} is non empty set
{("\/" ((proj1 x),S))} is non empty set
{{("\/" ((proj1 x),S)),("\/" ((proj2 x),T))},{("\/" ((proj1 x),S))}} is non empty set
Bottom T is M2( the carrier of T)
"\/" ({},T) is M2( the carrier of T)
Bottom [:S,T:] is M2( the carrier of [:S,T:])
"\/" ({},[:S,T:]) is M2( the carrier of [:S,T:])
Bottom S is M2( the carrier of S)
"\/" ({},S) is M2( the carrier of S)
S is non empty antisymmetric upper-bounded RelStr
T is non empty antisymmetric upper-bounded RelStr
[:S,T:] is non empty strict antisymmetric upper-bounded RelStr
the carrier of [:S,T:] is non empty set
bool the carrier of [:S,T:] is non empty set
x is M2( bool the carrier of [:S,T:])
"/\" (x,[:S,T:]) is M2( the carrier of [:S,T:])
proj1 x is M2( bool the carrier of S)
the carrier of S is non empty set
bool the carrier of S is non empty set
"/\" ((proj1 x),S) is M2( the carrier of S)
proj2 x is M2( bool the carrier of T)
the carrier of T is non empty set
bool the carrier of T is non empty set
"/\" ((proj2 x),T) is M2( the carrier of T)
[("/\" ((proj1 x),S)),("/\" ((proj2 x),T))] is V1() M2( the carrier of [:S,T:])
{("/\" ((proj1 x),S)),("/\" ((proj2 x),T))} is non empty set
{("/\" ((proj1 x),S))} is non empty set
{{("/\" ((proj1 x),S)),("/\" ((proj2 x),T))},{("/\" ((proj1 x),S))}} is non empty set
Top T is M2( the carrier of T)
"/\" ({},T) is M2( the carrier of T)
Top [:S,T:] is M2( the carrier of [:S,T:])
"/\" ({},[:S,T:]) is M2( the carrier of [:S,T:])
Top S is M2( the carrier of S)
"/\" ({},S) is M2( the carrier of S)
S is non empty RelStr
T is non empty RelStr
[:S,T:] is non empty strict RelStr
the carrier of [:S,T:] is non empty set
the carrier of S is non empty set
the carrier of T is non empty set
y is M2( the carrier of [:S,T:])
{y} is non empty M2( bool the carrier of [:S,T:])
bool the carrier of [:S,T:] is non empty set
x is M2( the carrier of [:S,T:])
y `1 is M2( the carrier of S)
{(y `1)} is non empty M2( bool the carrier of S)
bool the carrier of S is non empty set
x `1 is M2( the carrier of S)
y `2 is M2( the carrier of T)
{(y `2)} is non empty M2( bool the carrier of T)
bool the carrier of T is non empty set
x `2 is M2( the carrier of T)
[: the carrier of S, the carrier of T:] is non empty V7() set
[(x `1),(x `2)] is V1() M2( the carrier of [:S,T:])
{(x `1),(x `2)} is non empty set
{(x `1)} is non empty set
{{(x `1),(x `2)},{(x `1)}} is non empty set
[(y `1),(y `2)] is V1() M2( the carrier of [:S,T:])
{(y `1),(y `2)} is non empty set
{(y `1)} is non empty set
{{(y `1),(y `2)},{(y `1)}} is non empty set
y is M2( the carrier of S)
y is M2( the carrier of T)
y is M2( the carrier of [:S,T:])
y `2 is M2( the carrier of T)
y `1 is M2( the carrier of S)
S is non empty RelStr
T is non empty RelStr
[:S,T:] is non empty strict RelStr
the carrier of [:S,T:] is non empty set
the carrier of S is non empty set
the carrier of T is non empty set
y is M2( the carrier of [:S,T:])
y is M2( the carrier of [:S,T:])
{y,y} is non empty M2( bool the carrier of [:S,T:])
bool the carrier of [:S,T:] is non empty set
x is M2( the carrier of [:S,T:])
y `1 is M2( the carrier of S)
y `1 is M2( the carrier of S)
{(y `1),(y `1)} is non empty M2( bool the carrier of S)
bool the carrier of S is non empty set
x `1 is M2( the carrier of S)
y `2 is M2( the carrier of T)
y `2 is M2( the carrier of T)
{(y `2),(y `2)} is non empty M2( bool the carrier of T)
bool the carrier of T is non empty set
x `2 is M2( the carrier of T)
[: the carrier of S, the carrier of T:] is non empty V7() set
[(y `1),(y `2)] is V1() M2( the carrier of [:S,T:])
{(y `1),(y `2)} is non empty set
{(y `1)} is non empty set
{{(y `1),(y `2)},{(y `1)}} is non empty set
[(y `1),(y `2)] is V1() M2( the carrier of [:S,T:])
{(y `1),(y `2)} is non empty set
{(y `1)} is non empty set
{{(y `1),(y `2)},{(y `1)}} is non empty set
[(x `1),(x `2)] is V1() M2( the carrier of [:S,T:])
{(x `1),(x `2)} is non empty set
{(x `1)} is non empty set
{{(x `1),(x `2)},{(x `1)}} is non empty set
s9 is M2( the carrier of S)
s9 is M2( the carrier of T)
s9 is M2( the carrier of [:S,T:])
s9 `2 is M2( the carrier of T)
s9 `1 is M2( the carrier of S)
S is non empty RelStr
T is non empty RelStr
[:S,T:] is non empty strict RelStr
the carrier of [:S,T:] is non empty set
the carrier of S is non empty set
the carrier of T is non empty set
y is M2( the carrier of [:S,T:])
{y} is non empty M2( bool the carrier of [:S,T:])
bool the carrier of [:S,T:] is non empty set
x is M2( the carrier of [:S,T:])
y `1 is M2( the carrier of S)
{(y `1)} is non empty M2( bool the carrier of S)
bool the carrier of S is non empty set
x `1 is M2( the carrier of S)
y `2 is M2( the carrier of T)
{(y `2)} is non empty M2( bool the carrier of T)
bool the carrier of T is non empty set
x `2 is M2( the carrier of T)
[: the carrier of S, the carrier of T:] is non empty V7() set
[(x `1),(x `2)] is V1() M2( the carrier of [:S,T:])
{(x `1),(x `2)} is non empty set
{(x `1)} is non empty set
{{(x `1),(x `2)},{(x `1)}} is non empty set
[(y `1),(y `2)] is V1() M2( the carrier of [:S,T:])
{(y `1),(y `2)} is non empty set
{(y `1)} is non empty set
{{(y `1),(y `2)},{(y `1)}} is non empty set
y is M2( the carrier of S)
y is M2( the carrier of T)
y is M2( the carrier of [:S,T:])
y `2 is M2( the carrier of T)
y `1 is M2( the carrier of S)
S is non empty RelStr
T is non empty RelStr
[:S,T:] is non empty strict RelStr
the carrier of [:S,T:] is non empty set
the carrier of S is non empty set
the carrier of T is non empty set
y is M2( the carrier of [:S,T:])
y is M2( the carrier of [:S,T:])
{y,y} is non empty M2( bool the carrier of [:S,T:])
bool the carrier of [:S,T:] is non empty set
x is M2( the carrier of [:S,T:])
y `1 is M2( the carrier of S)
y `1 is M2( the carrier of S)
{(y `1),(y `1)} is non empty M2( bool the carrier of S)
bool the carrier of S is non empty set
x `1 is M2( the carrier of S)
y `2 is M2( the carrier of T)
y `2 is M2( the carrier of T)
{(y `2),(y `2)} is non empty M2( bool the carrier of T)
bool the carrier of T is non empty set
x `2 is M2( the carrier of T)
[: the carrier of S, the carrier of T:] is non empty V7() set
[(y `1),(y `2)] is V1() M2( the carrier of [:S,T:])
{(y `1),(y `2)} is non empty set
{(y `1)} is non empty set
{{(y `1),(y `2)},{(y `1)}} is non empty set
[(y `1),(y `2)] is V1() M2( the carrier of [:S,T:])
{(y `1),(y `2)} is non empty set
{(y `1)} is non empty set
{{(y `1),(y `2)},{(y `1)}} is non empty set
[(x `1),(x `2)] is V1() M2( the carrier of [:S,T:])
{(x `1),(x `2)} is non empty set
{(x `1)} is non empty set
{{(x `1),(x `2)},{(x `1)}} is non empty set
s9 is M2( the carrier of S)
s9 is M2( the carrier of T)
s9 is M2( the carrier of [:S,T:])
s9 `2 is M2( the carrier of T)
s9 `1 is M2( the carrier of S)
S is non empty antisymmetric RelStr
T is non empty antisymmetric RelStr
[:S,T:] is non empty strict antisymmetric RelStr
the carrier of [:S,T:] is non empty set
the carrier of S is non empty set
the carrier of T is non empty set
x is M2( the carrier of [:S,T:])
y is M2( the carrier of [:S,T:])
{x,y} is non empty M2( bool the carrier of [:S,T:])
bool the carrier of [:S,T:] is non empty set
x `1 is M2( the carrier of S)
y `1 is M2( the carrier of S)
{(x `1),(y `1)} is non empty M2( bool the carrier of S)
bool the carrier of S is non empty set
x `2 is M2( the carrier of T)
y `2 is M2( the carrier of T)
{(x `2),(y `2)} is non empty M2( bool the carrier of T)
bool the carrier of T is non empty set
[: the carrier of S, the carrier of T:] is non empty V7() set
[(x `1),(x `2)] is V1() M2( the carrier of [:S,T:])
{(x `1),(x `2)} is non empty set
{(x `1)} is non empty set
{{(x `1),(x `2)},{(x `1)}} is non empty set
[(y `1),(y `2)] is V1() M2( the carrier of [:S,T:])
{(y `1),(y `2)} is non empty set
{(y `1)} is non empty set
{{(y `1),(y `2)},{(y `1)}} is non empty set
proj1 {x,y} is M2( bool the carrier of S)
proj2 {x,y} is M2( bool the carrier of T)
S is non empty antisymmetric RelStr
T is non empty antisymmetric RelStr
[:S,T:] is non empty strict antisymmetric RelStr
the carrier of [:S,T:] is non empty set
the carrier of S is non empty set
the carrier of T is non empty set
x is M2( the carrier of [:S,T:])
y is M2( the carrier of [:S,T:])
{x,y} is non empty M2( bool the carrier of [:S,T:])
bool the carrier of [:S,T:] is non empty set
x `1 is M2( the carrier of S)
y `1 is M2( the carrier of S)
{(x `1),(y `1)} is non empty M2( bool the carrier of S)
bool the carrier of S is non empty set
x `2 is M2( the carrier of T)
y `2 is M2( the carrier of T)
{(x `2),(y `2)} is non empty M2( bool the carrier of T)
bool the carrier of T is non empty set
[: the carrier of S, the carrier of T:] is non empty V7() set
[(x `1),(x `2)] is V1() M2( the carrier of [:S,T:])
{(x `1),(x `2)} is non empty set
{(x `1)} is non empty set
{{(x `1),(x `2)},{(x `1)}} is non empty set
[(y `1),(y `2)] is V1() M2( the carrier of [:S,T:])
{(y `1),(y `2)} is non empty set
{(y `1)} is non empty set
{{(y `1),(y `2)},{(y `1)}} is non empty set
proj1 {x,y} is M2( bool the carrier of S)
proj2 {x,y} is M2( bool the carrier of T)
S is non empty antisymmetric with_infima RelStr
T is non empty antisymmetric with_infima RelStr
[:S,T:] is non empty strict antisymmetric with_infima RelStr
the carrier of [:S,T:] is non empty set
x is M2( the carrier of [:S,T:])
y is M2( the carrier of [:S,T:])
x "/\" y is M2( the carrier of [:S,T:])
(x "/\" y) `1 is M2( the carrier of S)
the carrier of S is non empty set
x `1 is M2( the carrier of S)
y `1 is M2( the carrier of S)
(x `1) "/\" (y `1) is M2( the carrier of S)
(x "/\" y) `2 is M2( the carrier of T)
the carrier of T is non empty set
x `2 is M2( the carrier of T)
y `2 is M2( the carrier of T)
(x `2) "/\" (y `2) is M2( the carrier of T)
[: the carrier of S, the carrier of T:] is non empty V7() set
[(x `1),(x `2)] is V1() M2( the carrier of [:S,T:])
{(x `1),(x `2)} is non empty set
{(x `1)} is non empty set
{{(x `1),(x `2)},{(x `1)}} is non empty set
[(y `1),(y `2)] is V1() M2( the carrier of [:S,T:])
{(y `1),(y `2)} is non empty set
{(y `1)} is non empty set
{{(y `1),(y `2)},{(y `1)}} is non empty set
t is M2( the carrier of S)
[t,((x `2) "/\" (y `2))] is V1() M2( the carrier of [:S,T:])
{t,((x `2) "/\" (y `2))} is non empty set
{t} is non empty set
{{t,((x `2) "/\" (y `2))},{t}} is non empty set
[t,((x `2) "/\" (y `2))] `1 is M2( the carrier of S)
t is M2( the carrier of T)
[((x `1) "/\" (y `1)),t] is V1() M2( the carrier of [:S,T:])
{((x `1) "/\" (y `1)),t} is non empty set
{((x `1) "/\" (y `1))} is non empty set
{{((x `1) "/\" (y `1)),t},{((x `1) "/\" (y `1))}} is non empty set
[((x `1) "/\" (y `1)),t] `2 is M2( the carrier of T)
S is non empty antisymmetric with_suprema RelStr
T is non empty antisymmetric with_suprema RelStr
[:S,T:] is non empty strict antisymmetric with_suprema RelStr
the carrier of [:S,T:] is non empty set
x is M2( the carrier of [:S,T:])
y is M2( the carrier of [:S,T:])
x "\/" y is M2( the carrier of [:S,T:])
(x "\/" y) `1 is M2( the carrier of S)
the carrier of S is non empty set
x `1 is M2( the carrier of S)
y `1 is M2( the carrier of S)
(x `1) "\/" (y `1) is M2( the carrier of S)
(x "\/" y) `2 is M2( the carrier of T)
the carrier of T is non empty set
x `2 is M2( the carrier of T)
y `2 is M2( the carrier of T)
(x `2) "\/" (y `2) is M2( the carrier of T)
[: the carrier of S, the carrier of T:] is non empty V7() set
[(x `1),(x `2)] is V1() M2( the carrier of [:S,T:])
{(x `1),(x `2)} is non empty set
{(x `1)} is non empty set
{{(x `1),(x `2)},{(x `1)}} is non empty set
[(y `1),(y `2)] is V1() M2( the carrier of [:S,T:])
{(y `1),(y `2)} is non empty set
{(y `1)} is non empty set
{{(y `1),(y `2)},{(y `1)}} is non empty set
t is M2( the carrier of S)
[t,((x `2) "\/" (y `2))] is V1() M2( the carrier of [:S,T:])
{t,((x `2) "\/" (y `2))} is non empty set
{t} is non empty set
{{t,((x `2) "\/" (y `2))},{t}} is non empty set
[t,((x `2) "\/" (y `2))] `1 is M2( the carrier of S)
t is M2( the carrier of T)
[((x `1) "\/" (y `1)),t] is V1() M2( the carrier of [:S,T:])
{((x `1) "\/" (y `1)),t} is non empty set
{((x `1) "\/" (y `1))} is non empty set
{{((x `1) "\/" (y `1)),t},{((x `1) "\/" (y `1))}} is non empty set
[((x `1) "\/" (y `1)),t] `2 is M2( the carrier of T)
S is non empty antisymmetric with_infima RelStr
the carrier of S is non empty set
T is non empty antisymmetric with_infima RelStr
the carrier of T is non empty set
[:S,T:] is non empty strict antisymmetric with_infima RelStr
x is M2( the carrier of S)
y is M2( the carrier of S)
x "/\" y is M2( the carrier of S)
y is M2( the carrier of T)
s9 is M2( the carrier of T)
y "/\" s9 is M2( the carrier of T)
[(x "/\" y),(y "/\" s9)] is V1() M2( the carrier of [:S,T:])
the carrier of [:S,T:] is non empty set
{(x "/\" y),(y "/\" s9)} is non empty set
{(x "/\" y)} is non empty set
{{(x "/\" y),(y "/\" s9)},{(x "/\" y)}} is non empty set
[x,y] is V1() M2( the carrier of [:S,T:])
{x,y} is non empty set
{x} is non empty set
{{x,y},{x}} is non empty set
[y,s9] is V1() M2( the carrier of [:S,T:])
{y,s9} is non empty set
{y} is non empty set
{{y,s9},{y}} is non empty set
[x,y] "/\" [y,s9] is M2( the carrier of [:S,T:])
[: the carrier of S, the carrier of T:] is non empty V7() set
([x,y] "/\" [y,s9]) `2 is M2( the carrier of T)
[x,y] `2 is M2( the carrier of T)
[y,s9] `2 is M2( the carrier of T)
([x,y] `2) "/\" ([y,s9] `2) is M2( the carrier of T)
y "/\" ([y,s9] `2) is M2( the carrier of T)
[(x "/\" y),(y "/\" s9)] `2 is M2( the carrier of T)
([x,y] "/\" [y,s9]) `1 is M2( the carrier of S)
[x,y] `1 is M2( the carrier of S)
[y,s9] `1 is M2( the carrier of S)
([x,y] `1) "/\" ([y,s9] `1) is M2( the carrier of S)
x "/\" ([y,s9] `1) is M2( the carrier of S)
[(x "/\" y),(y "/\" s9)] `1 is M2( the carrier of S)
S is non empty antisymmetric with_suprema RelStr
the carrier of S is non empty set
T is non empty antisymmetric with_suprema RelStr
the carrier of T is non empty set
[:S,T:] is non empty strict antisymmetric with_suprema RelStr
x is M2( the carrier of S)
y is M2( the carrier of S)
x "\/" y is M2( the carrier of S)
y is M2( the carrier of T)
s9 is M2( the carrier of T)
y "\/" s9 is M2( the carrier of T)
[(x "\/" y),(y "\/" s9)] is V1() M2( the carrier of [:S,T:])
the carrier of [:S,T:] is non empty set
{(x "\/" y),(y "\/" s9)} is non empty set
{(x "\/" y)} is non empty set
{{(x "\/" y),(y "\/" s9)},{(x "\/" y)}} is non empty set
[x,y] is V1() M2( the carrier of [:S,T:])
{x,y} is non empty set
{x} is non empty set
{{x,y},{x}} is non empty set
[y,s9] is V1() M2( the carrier of [:S,T:])
{y,s9} is non empty set
{y} is non empty set
{{y,s9},{y}} is non empty set
[x,y] "\/" [y,s9] is M2( the carrier of [:S,T:])
[: the carrier of S, the carrier of T:] is non empty V7() set
([x,y] "\/" [y,s9]) `2 is M2( the carrier of T)
[x,y] `2 is M2( the carrier of T)
[y,s9] `2 is M2( the carrier of T)
([x,y] `2) "\/" ([y,s9] `2) is M2( the carrier of T)
y "\/" ([y,s9] `2) is M2( the carrier of T)
[(x "\/" y),(y "\/" s9)] `2 is M2( the carrier of T)
([x,y] "\/" [y,s9]) `1 is M2( the carrier of S)
[x,y] `1 is M2( the carrier of S)
[y,s9] `1 is M2( the carrier of S)
([x,y] `1) "\/" ([y,s9] `1) is M2( the carrier of S)
x "\/" ([y,s9] `1) is M2( the carrier of S)
[(x "\/" y),(y "\/" s9)] `1 is M2( the carrier of S)
S is non empty antisymmetric with_suprema with_infima RelStr
the carrier of S is non empty set
y is M2( the carrier of S)
y is M2( the carrier of S)
y "\/" y is M2( the carrier of S)
Top S is M2( the carrier of S)
"/\" ({},S) is M2( the carrier of S)
y "/\" y is M2( the carrier of S)
Bottom S is M2( the carrier of S)
"\/" ({},S) is M2( the carrier of S)
S is non empty antisymmetric lower-bounded upper-bounded bounded with_suprema with_infima RelStr
T is non empty antisymmetric lower-bounded upper-bounded bounded with_suprema with_infima RelStr
[:S,T:] is non empty strict antisymmetric lower-bounded upper-bounded bounded with_suprema with_infima RelStr
the carrier of [:S,T:] is non empty set
y is M2( the carrier of [:S,T:])
x is M2( the carrier of [:S,T:])
y `1 is M2( the carrier of S)
the carrier of S is non empty set
x `1 is M2( the carrier of S)
y `2 is M2( the carrier of T)
the carrier of T is non empty set
x `2 is M2( the carrier of T)
[: the carrier of S, the carrier of T:] is non empty V7() set
(y `1) "/\" (x `1) is M2( the carrier of S)
y "/\" x is M2( the carrier of [:S,T:])
(y "/\" x) `1 is M2( the carrier of S)
Bottom [:S,T:] is M2( the carrier of [:S,T:])
"\/" ({},[:S,T:]) is M2( the carrier of [:S,T:])
(Bottom [:S,T:]) `1 is M2( the carrier of S)
Bottom S is M2( the carrier of S)
"\/" ({},S) is M2( the carrier of S)
Bottom T is M2( the carrier of T)
"\/" ({},T) is M2( the carrier of T)
[(Bottom S),(Bottom T)] is V1() M2( the carrier of [:S,T:])
{(Bottom S),(Bottom T)} is non empty set
{(Bottom S)} is non empty set
{{(Bottom S),(Bottom T)},{(Bottom S)}} is non empty set
[(Bottom S),(Bottom T)] `1 is M2( the carrier of S)
(y `1) "\/" (x `1) is M2( the carrier of S)
y "\/" x is M2( the carrier of [:S,T:])
(y "\/" x) `1 is M2( the carrier of S)
Top [:S,T:] is M2( the carrier of [:S,T:])
"/\" ({},[:S,T:]) is M2( the carrier of [:S,T:])
(Top [:S,T:]) `1 is M2( the carrier of S)
Top S is M2( the carrier of S)
"/\" ({},S) is M2( the carrier of S)
Top T is M2( the carrier of T)
"/\" ({},T) is M2( the carrier of T)
[(Top S),(Top T)] is V1() M2( the carrier of [:S,T:])
{(Top S),(Top T)} is non empty set
{(Top S)} is non empty set
{{(Top S),(Top T)},{(Top S)}} is non empty set
[(Top S),(Top T)] `1 is M2( the carrier of S)
(y `2) "/\" (x `2) is M2( the carrier of T)
(y "/\" x) `2 is M2( the carrier of T)
(Bottom [:S,T:]) `2 is M2( the carrier of T)
[(Bottom S),(Bottom T)] `2 is M2( the carrier of T)
(y `2) "\/" (x `2) is M2( the carrier of T)
(y "\/" x) `2 is M2( the carrier of T)
(Top [:S,T:]) `2 is M2( the carrier of T)
[(Top S),(Top T)] `2 is M2( the carrier of T)
y "/\" x is M2( the carrier of [:S,T:])
S is non empty reflexive antisymmetric up-complete non void RelStr
the carrier of S is non empty set
T is non empty reflexive antisymmetric up-complete non void RelStr
the carrier of T is non empty set
[:S,T:] is non empty strict reflexive antisymmetric up-complete non void RelStr
x is M2( the carrier of S)
y is M2( the carrier of S)
y is M2( the carrier of T)
[x,y] is V1() M2( the carrier of [:S,T:])
the carrier of [:S,T:] is non empty set
{x,y} is non empty set
{x} is non empty set
{{x,y},{x}} is non empty set
s9 is M2( the carrier of T)
[y,s9] is V1() M2( the carrier of [:S,T:])
{y,s9} is non empty set
{y} is non empty set
{{y,s9},{y}} is non empty set
bool the carrier of [:S,T:] is non empty set
[: the carrier of S, the carrier of T:] is non empty V7() set
bool the carrier of T is non empty set
{s9} is non empty M2( bool the carrier of T)
bool the carrier of S is non empty set
t is non empty directed M2( bool the carrier of S)
"\/" (t,S) is M2( the carrier of S)
ST is non empty directed M2( bool the carrier of T)
"\/" (ST,T) is M2( the carrier of T)
[:t,ST:] is non empty V7() directed M2( bool the carrier of [:S,T:])
"\/" ([:t,ST:],[:S,T:]) is M2( the carrier of [:S,T:])
[("\/" (t,S)),("\/" (ST,T))] is V1() M2( the carrier of [:S,T:])
{("\/" (t,S)),("\/" (ST,T))} is non empty set
{("\/" (t,S))} is non empty set
{{("\/" (t,S)),("\/" (ST,T))},{("\/" (t,S))}} is non empty set
t1 is M2( the carrier of [:S,T:])
t1 `1 is M2( the carrier of S)
t1 `2 is M2( the carrier of T)
[(t1 `1),(t1 `2)] is V1() M2( the carrier of [:S,T:])
{(t1 `1),(t1 `2)} is non empty set
{(t1 `1)} is non empty set
{{(t1 `1),(t1 `2)},{(t1 `1)}} is non empty set
bool the carrier of T is non empty set
ST is non empty directed M2( bool the carrier of T)
"\/" (ST,T) is M2( the carrier of T)
bool the carrier of S is non empty set
{y} is non empty M2( bool the carrier of S)
t is non empty directed M2( bool the carrier of S)
"\/" (t,S) is M2( the carrier of S)
[:t,ST:] is non empty V7() directed M2( bool the carrier of [:S,T:])
"\/" ([:t,ST:],[:S,T:]) is M2( the carrier of [:S,T:])
[("\/" (t,S)),("\/" (ST,T))] is V1() M2( the carrier of [:S,T:])
{("\/" (t,S)),("\/" (ST,T))} is non empty set
{("\/" (t,S))} is non empty set
{{("\/" (t,S)),("\/" (ST,T))},{("\/" (t,S))}} is non empty set
t1 is M2( the carrier of [:S,T:])
t1 `2 is M2( the carrier of T)
t1 `1 is M2( the carrier of S)
[(t1 `1),(t1 `2)] is V1() M2( the carrier of [:S,T:])
{(t1 `1),(t1 `2)} is non empty set
{(t1 `1)} is non empty set
{{(t1 `1),(t1 `2)},{(t1 `1)}} is non empty set
S is non empty reflexive transitive antisymmetric up-complete non void RelStr
the carrier of S is non empty set
T is non empty reflexive transitive antisymmetric up-complete non void RelStr
the carrier of T is non empty set
[:S,T:] is non empty strict reflexive transitive antisymmetric up-complete non void RelStr
x is M2( the carrier of S)
y is M2( the carrier of S)
y is M2( the carrier of T)
[x,y] is V1() M2( the carrier of [:S,T:])
the carrier of [:S,T:] is non empty set
{x,y} is non empty set
{x} is non empty set
{{x,y},{x}} is non empty set
s9 is M2( the carrier of T)
[y,s9] is V1() M2( the carrier of [:S,T:])
{y,s9} is non empty set
{y} is non empty set
{{y,s9},{y}} is non empty set
bool the carrier of S is non empty set
bool the carrier of T is non empty set
bool the carrier of [:S,T:] is non empty set
ST is non empty directed M2( bool the carrier of [:S,T:])
"\/" (ST,[:S,T:]) is M2( the carrier of [:S,T:])
proj1 ST is M2( bool the carrier of S)
"\/" ((proj1 ST),S) is M2( the carrier of S)
proj2 ST is M2( bool the carrier of T)
"\/" ((proj2 ST),T) is M2( the carrier of T)
[("\/" ((proj1 ST),S)),("\/" ((proj2 ST),T))] is V1() M2( the carrier of [:S,T:])
{("\/" ((proj1 ST),S)),("\/" ((proj2 ST),T))} is non empty set
{("\/" ((proj1 ST),S))} is non empty set
{{("\/" ((proj1 ST),S)),("\/" ((proj2 ST),T))},{("\/" ((proj1 ST),S))}} is non empty set
t is M2( the carrier of S)
t1 is set
[t,t1] is V1() set
{t,t1} is non empty set
{t} is non empty set
{{t,t1},{t}} is non empty set
s2 is M2( the carrier of T)
t1 is set
[t1,s2] is V1() set
{t1,s2} is non empty set
{t1} is non empty set
{{t1,s2},{t1}} is non empty set
[: the carrier of S, the carrier of T:] is non empty V7() set
z is M2( the carrier of T)
[t,z] is V1() M2( the carrier of [:S,T:])
{t,z} is non empty set
{{t,z},{t}} is non empty set
x is M2( the carrier of S)
[x,s2] is V1() M2( the carrier of [:S,T:])
{x,s2} is non empty set
{x} is non empty set
{{x,s2},{x}} is non empty set
z is M2( the carrier of [:S,T:])
z `1 is M2( the carrier of S)
z `2 is M2( the carrier of T)
[(z `1),(z `2)] is V1() M2( the carrier of [:S,T:])
{(z `1),(z `2)} is non empty set
{(z `1)} is non empty set
{{(z `1),(z `2)},{(z `1)}} is non empty set
[t,s2] is V1() M2( the carrier of [:S,T:])
{t,s2} is non empty set
{{t,s2},{t}} is non empty set
S is non empty reflexive antisymmetric up-complete non void RelStr
T is non empty reflexive antisymmetric up-complete non void RelStr
[:S,T:] is non empty strict reflexive antisymmetric up-complete non void RelStr
the carrier of [:S,T:] is non empty set
x is M2( the carrier of [:S,T:])
y is M2( the carrier of [:S,T:])
x `1 is M2( the carrier of S)
the carrier of S is non empty set
y `1 is M2( the carrier of S)
x `2 is M2( the carrier of T)
the carrier of T is non empty set
y `2 is M2( the carrier of T)
[: the carrier of S, the carrier of T:] is non empty V7() set
[(x `1),(x `2)] is V1() M2( the carrier of [:S,T:])
{(x `1),(x `2)} is non empty set
{(x `1)} is non empty set
{{(x `1),(x `2)},{(x `1)}} is non empty set
[(y `1),(y `2)] is V1() M2( the carrier of [:S,T:])
{(y `1),(y `2)} is non empty set
{(y `1)} is non empty set
{{(y `1),(y `2)},{(y `1)}} is non empty set
S is non empty reflexive transitive antisymmetric up-complete non void RelStr
T is non empty reflexive transitive antisymmetric up-complete non void RelStr
[:S,T:] is non empty strict reflexive transitive antisymmetric up-complete non void RelStr
the carrier of [:S,T:] is non empty set
x is M2( the carrier of [:S,T:])
y is M2( the carrier of [:S,T:])
x `1 is M2( the carrier of S)
the carrier of S is non empty set
y `1 is M2( the carrier of S)
x `2 is M2( the carrier of T)
the carrier of T is non empty set
y `2 is M2( the carrier of T)
[: the carrier of S, the carrier of T:] is non empty V7() set
[(x `1),(x `2)] is V1() M2( the carrier of [:S,T:])
{(x `1),(x `2)} is non empty set
{(x `1)} is non empty set
{{(x `1),(x `2)},{(x `1)}} is non empty set
[(y `1),(y `2)] is V1() M2( the carrier of [:S,T:])
{(y `1),(y `2)} is non empty set
{(y `1)} is non empty set
{{(y `1),(y `2)},{(y `1)}} is non empty set
S is non empty reflexive antisymmetric up-complete non void RelStr
T is non empty reflexive antisymmetric up-complete non void RelStr
[:S,T:] is non empty strict reflexive antisymmetric up-complete non void RelStr
the carrier of [:S,T:] is non empty set
x is M2( the carrier of [:S,T:])
x `1 is M2( the carrier of S)
the carrier of S is non empty set
x `2 is M2( the carrier of T)
the carrier of T is non empty set
S is non empty reflexive transitive antisymmetric up-complete non void RelStr
T is non empty reflexive transitive antisymmetric up-complete non void RelStr
[:S,T:] is non empty strict reflexive transitive antisymmetric up-complete non void RelStr
the carrier of [:S,T:] is non empty set
x is M2( the carrier of [:S,T:])
x `1 is M2( the carrier of S)
the carrier of S is non empty set
x `2 is M2( the carrier of T)
the carrier of T is non empty set
S is non empty antisymmetric with_infima RelStr
T is non empty antisymmetric with_infima RelStr
[:S,T:] is non empty strict antisymmetric with_infima RelStr
the carrier of [:S,T:] is non empty set
bool the carrier of [:S,T:] is non empty set
x is M2( bool the carrier of [:S,T:])
y is M2( bool the carrier of [:S,T:])
x "/\" y is M2( bool the carrier of [:S,T:])
proj1 (x "/\" y) is M2( bool the carrier of S)
the carrier of S is non empty set
bool the carrier of S is non empty set
proj1 x is M2( bool the carrier of S)
proj1 y is M2( bool the carrier of S)
(proj1 x) "/\" (proj1 y) is M2( bool the carrier of S)
proj2 (x "/\" y) is M2( bool the carrier of T)
the carrier of T is non empty set
bool the carrier of T is non empty set
proj2 x is M2( bool the carrier of T)
proj2 y is M2( bool the carrier of T)
(proj2 x) "/\" (proj2 y) is M2( bool the carrier of T)
[: the carrier of S, the carrier of T:] is non empty V7() set
{ (b₁ "/\" b₂) where b₁, b₂ is M2( the carrier of [:S,T:]) : ( b₁ in x & b₂ in y ) } is set
{ (b₁ "/\" b₂) where b₁, b₂ is M2( the carrier of S) : ( b₁ in proj1 x & b₂ in proj1 y ) } is set
y is set
s9 is set
[y,s9] is V1() set
{y,s9} is non empty set
{y} is non empty set
{{y,s9},{y}} is non empty set
ST is M2( the carrier of [:S,T:])
t is M2( the carrier of [:S,T:])
ST "/\" t is M2( the carrier of [:S,T:])
ST `1 is M2( the carrier of S)
ST `2 is M2( the carrier of T)
[(ST `1),(ST `2)] is V1() M2( the carrier of [:S,T:])
{(ST `1),(ST `2)} is non empty set
{(ST `1)} is non empty set
{{(ST `1),(ST `2)},{(ST `1)}} is non empty set
t `1 is M2( the carrier of S)
t `2 is M2( the carrier of T)
[(t `1),(t `2)] is V1() M2( the carrier of [:S,T:])
{(t `1),(t `2)} is non empty set
{(t `1)} is non empty set
{{(t `1),(t `2)},{(t `1)}} is non empty set
[y,s9] `1 is set
(ST `1) "/\" (t `1) is M2( the carrier of S)
y is set
s9 is M2( the carrier of S)
ST is M2( the carrier of S)
s9 "/\" ST is M2( the carrier of S)
t is set
[s9,t] is V1() set
{s9,t} is non empty set
{s9} is non empty set
{{s9,t},{s9}} is non empty set
t1 is set
[ST,t1] is V1() set
{ST,t1} is non empty set
{ST} is non empty set
{{ST,t1},{ST}} is non empty set
s2 is M2( the carrier of T)
[s9,s2] is V1() M2( the carrier of [:S,T:])
{s9,s2} is non empty set
{{s9,s2},{s9}} is non empty set
t1 is M2( the carrier of T)
[ST,t1] is V1() M2( the carrier of [:S,T:])
{ST,t1} is non empty set
{{ST,t1},{ST}} is non empty set
[s9,s2] "/\" [ST,t1] is M2( the carrier of [:S,T:])
s2 "/\" t1 is M2( the carrier of T)
[y,(s2 "/\" t1)] is V1() set
{y,(s2 "/\" t1)} is non empty set
{y} is non empty set
{{y,(s2 "/\" t1)},{y}} is non empty set
y is set
s9 is set
[s9,y] is V1() set
{s9,y} is non empty set
{s9} is non empty set
{{s9,y},{s9}} is non empty set
ST is M2( the carrier of [:S,T:])
t is M2( the carrier of [:S,T:])
ST "/\" t is M2( the carrier of [:S,T:])
ST `1 is M2( the carrier of S)
ST `2 is M2( the carrier of T)
[(ST `1),(ST `2)] is V1() M2( the carrier of [:S,T:])
{(ST `1),(ST `2)} is non empty set
{(ST `1)} is non empty set
{{(ST `1),(ST `2)},{(ST `1)}} is non empty set
t `1 is M2( the carrier of S)
t `2 is M2( the carrier of T)
[(t `1),(t `2)] is V1() M2( the carrier of [:S,T:])
{(t `1),(t `2)} is non empty set
{(t `1)} is non empty set
{{(t `1),(t `2)},{(t `1)}} is non empty set
[s9,y] `2 is set
(ST `2) "/\" (t `2) is M2( the carrier of T)
y is set
{ (b₁ "/\" b₂) where b₁, b₂ is M2( the carrier of T) : ( b₁ in proj2 x & b₂ in proj2 y ) } is set
s9 is M2( the carrier of T)
ST is M2( the carrier of T)
s9 "/\" ST is M2( the carrier of T)
t is set
[t,s9] is V1() set
{t,s9} is non empty set
{t} is non empty set
{{t,s9},{t}} is non empty set
t1 is set
[t1,ST] is V1() set
{t1,ST} is non empty set
{t1} is non empty set
{{t1,ST},{t1}} is non empty set
s2 is M2( the carrier of S)
[s2,s9] is V1() M2( the carrier of [:S,T:])
{s2,s9} is non empty set
{s2} is non empty set
{{s2,s9},{s2}} is non empty set
t1 is M2( the carrier of S)
[t1,ST] is V1() M2( the carrier of [:S,T:])
{t1,ST} is non empty set
{t1} is non empty set
{{t1,ST},{t1}} is non empty set
[s2,s9] "/\" [t1,ST] is M2( the carrier of [:S,T:])
s2 "/\" t1 is M2( the carrier of S)
[(s2 "/\" t1),y] is V1() set
{(s2 "/\" t1),y} is non empty set
{(s2 "/\" t1)} is non empty set
{{(s2 "/\" t1),y},{(s2 "/\" t1)}} is non empty set
S is non empty antisymmetric with_suprema RelStr
T is non empty antisymmetric with_suprema RelStr
[:S,T:] is non empty strict antisymmetric with_suprema RelStr
the carrier of [:S,T:] is non empty set
bool the carrier of [:S,T:] is non empty set
x is M2( bool the carrier of [:S,T:])
y is M2( bool the carrier of [:S,T:])
x "\/" y is M2( bool the carrier of [:S,T:])
proj1 (x "\/" y) is M2( bool the carrier of S)
the carrier of S is non empty set
bool the carrier of S is non empty set
proj1 x is M2( bool the carrier of S)
proj1 y is M2( bool the carrier of S)
(proj1 x) "\/" (proj1 y) is M2( bool the carrier of S)
proj2 (x "\/" y) is M2( bool the carrier of T)
the carrier of T is non empty set
bool the carrier of T is non empty set
proj2 x is M2( bool the carrier of T)
proj2 y is M2( bool the carrier of T)
(proj2 x) "\/" (proj2 y) is M2( bool the carrier of T)
[: the carrier of S, the carrier of T:] is non empty V7() set
{ (b₁ "\/" b₂) where b₁, b₂ is M2( the carrier of [:S,T:]) : ( b₁ in x & b₂ in y ) } is set
{ (b₁ "\/" b₂) where b₁, b₂ is M2( the carrier of S) : ( b₁ in proj1 x & b₂ in proj1 y ) } is set
y is set
s9 is set
[y,s9] is V1() set
{y,s9} is non empty set
{y} is non empty set
{{y,s9},{y}} is non empty set
ST is M2( the carrier of [:S,T:])
t is M2( the carrier of [:S,T:])
ST "\/" t is M2( the carrier of [:S,T:])
ST `1 is M2( the carrier of S)
ST `2 is M2( the carrier of T)
[(ST `1),(ST `2)] is V1() M2( the carrier of [:S,T:])
{(ST `1),(ST `2)} is non empty set
{(ST `1)} is non empty set
{{(ST `1),(ST `2)},{(ST `1)}} is non empty set
t `1 is M2( the carrier of S)
t `2 is M2( the carrier of T)
[(t `1),(t `2)] is V1() M2( the carrier of [:S,T:])
{(t `1),(t `2)} is non empty set
{(t `1)} is non empty set
{{(t `1),(t `2)},{(t `1)}} is non empty set
[y,s9] `1 is set
(ST `1) "\/" (t `1) is M2( the carrier of S)
y is set
s9 is M2( the carrier of S)
ST is M2( the carrier of S)
s9 "\/" ST is M2( the carrier of S)
t is set
[s9,t] is V1() set
{s9,t} is non empty set
{s9} is non empty set
{{s9,t},{s9}} is non empty set
t1 is set
[ST,t1] is V1() set
{ST,t1} is non empty set
{ST} is non empty set
{{ST,t1},{ST}} is non empty set
s2 is M2( the carrier of T)
[s9,s2] is V1() M2( the carrier of [:S,T:])
{s9,s2} is non empty set
{{s9,s2},{s9}} is non empty set
t1 is M2( the carrier of T)
[ST,t1] is V1() M2( the carrier of [:S,T:])
{ST,t1} is non empty set
{{ST,t1},{ST}} is non empty set
[s9,s2] "\/" [ST,t1] is M2( the carrier of [:S,T:])
s2 "\/" t1 is M2( the carrier of T)
[y,(s2 "\/" t1)] is V1() set
{y,(s2 "\/" t1)} is non empty set
{y} is non empty set
{{y,(s2 "\/" t1)},{y}} is non empty set
y is set
s9 is set
[s9,y] is V1() set
{s9,y} is non empty set
{s9} is non empty set
{{s9,y},{s9}} is non empty set
ST is M2( the carrier of [:S,T:])
t is M2( the carrier of [:S,T:])
ST "\/" t is M2( the carrier of [:S,T:])
ST `1 is M2( the carrier of S)
ST `2 is M2( the carrier of T)
[(ST `1),(ST `2)] is V1() M2( the carrier of [:S,T:])
{(ST `1),(ST `2)} is non empty set
{(ST `1)} is non empty set
{{(ST `1),(ST `2)},{(ST `1)}} is non empty set
t `1 is M2( the carrier of S)
t `2 is M2( the carrier of T)
[(t `1),(t `2)] is V1() M2( the carrier of [:S,T:])
{(t `1),(t `2)} is non empty set
{(t `1)} is non empty set
{{(t `1),(t `2)},{(t `1)}} is non empty set
[s9,y] `2 is set
(ST `2) "\/" (t `2) is M2( the carrier of T)
y is set
{ (b₁ "\/" b₂) where b₁, b₂ is M2( the carrier of T) : ( b₁ in proj2 x & b₂ in proj2 y ) } is set
s9 is M2( the carrier of T)
ST is M2( the carrier of T)
s9 "\/" ST is M2( the carrier of T)
t is set
[t,s9] is V1() set
{t,s9} is non empty set
{t} is non empty set
{{t,s9},{t}} is non empty set
t1 is set
[t1,ST] is V1() set
{t1,ST} is non empty set
{t1} is non empty set
{{t1,ST},{t1}} is non empty set
s2 is M2( the carrier of S)
[s2,s9] is V1() M2( the carrier of [:S,T:])
{s2,s9} is non empty set
{s2} is non empty set
{{s2,s9},{s2}} is non empty set
t1 is M2( the carrier of S)
[t1,ST] is V1() M2( the carrier of [:S,T:])
{t1,ST} is non empty set
{t1} is non empty set
{{t1,ST},{t1}} is non empty set
[s2,s9] "\/" [t1,ST] is M2( the carrier of [:S,T:])
s2 "\/" t1 is M2( the carrier of S)
[(s2 "\/" t1),y] is V1() set
{(s2 "\/" t1),y} is non empty set
{(s2 "\/" t1)} is non empty set
{{(s2 "\/" t1),y},{(s2 "\/" t1)}} is non empty set
S is RelStr
T is RelStr
[:S,T:] is strict RelStr
the carrier of [:S,T:] is set
bool the carrier of [:S,T:] is non empty set
x is M2( bool the carrier of [:S,T:])
downarrow x is M2( bool the carrier of [:S,T:])
proj1 x is M2( bool the carrier of S)
the carrier of S is set
bool the carrier of S is non empty set
downarrow (proj1 x) is M2( bool the carrier of S)
proj2 x is M2( bool the carrier of T)
the carrier of T is set
bool the carrier of T is non empty set
downarrow (proj2 x) is M2( bool the carrier of T)
[:(downarrow (proj1 x)),(downarrow (proj2 x)):] is V7() M2( bool the carrier of [:S,T:])
y is set
[: the carrier of S, the carrier of T:] is V7() set
ST is set
t is set
[ST,t] is V1() set
{ST,t} is non empty set
{ST} is non empty set
{{ST,t},{ST}} is non empty set
y is non empty RelStr
s9 is non empty RelStr
[:y,s9:] is non empty strict RelStr
the carrier of [:y,s9:] is non empty set
ST is M2( the carrier of [:y,s9:])
t is M2( the carrier of [:y,s9:])
ST `1 is M2( the carrier of y)
the carrier of y is non empty set
t `1 is M2( the carrier of y)
t `2 is M2( the carrier of s9)
the carrier of s9 is non empty set
[(t `1),(t `2)] is V1() M2( the carrier of [:y,s9:])
{(t `1),(t `2)} is non empty set
{(t `1)} is non empty set
{{(t `1),(t `2)},{(t `1)}} is non empty set
y `1 is set
ST `2 is M2( the carrier of s9)
y `2 is set
[(ST `1),(ST `2)] is V1() M2( the carrier of [:y,s9:])
{(ST `1),(ST `2)} is non empty set
{(ST `1)} is non empty set
{{(ST `1),(ST `2)},{(ST `1)}} is non empty set
S is RelStr
the carrier of S is set
bool the carrier of S is non empty set
T is RelStr
the carrier of T is set
bool the carrier of T is non empty set
[:S,T:] is strict RelStr
x is M2( bool the carrier of S)
downarrow x is M2( bool the carrier of S)
y is M2( bool the carrier of T)
downarrow y is M2( bool the carrier of T)
[:(downarrow x),(downarrow y):] is V7() M2( bool the carrier of [:S,T:])
the carrier of [:S,T:] is set
bool the carrier of [:S,T:] is non empty set
[:x,y:] is V7() M2( bool the carrier of [:S,T:])
downarrow [:x,y:] is M2( bool the carrier of [:S,T:])
y is set
s9 is set
ST is set
[s9,ST] is V1() set
{s9,ST} is non empty set
{s9} is non empty set
{{s9,ST},{s9}} is non empty set
t is non empty RelStr
the carrier of t is non empty set
s2 is M2( the carrier of t)
t1 is M2( the carrier of t)
t1 is non empty RelStr
the carrier of t1 is non empty set
z is M2( the carrier of t1)
x is M2( the carrier of t1)
[t1,x] is V1() M2( the carrier of [:t,t1:])
[:t,t1:] is non empty strict RelStr
the carrier of [:t,t1:] is non empty set
{t1,x} is non empty set
{t1} is non empty set
{{t1,x},{t1}} is non empty set
[s2,z] is V1() M2( the carrier of [:t,t1:])
{s2,z} is non empty set
{s2} is non empty set
{{s2,z},{s2}} is non empty set
y is set
[: the carrier of S, the carrier of T:] is V7() set
t is set
t1 is set
[t,t1] is V1() set
{t,t1} is non empty set
{t} is non empty set
{{t,t1},{t}} is non empty set
s9 is non empty RelStr
ST is non empty RelStr
[:s9,ST:] is non empty strict RelStr
the carrier of [:s9,ST:] is non empty set
t is M2( the carrier of [:s9,ST:])
t1 is M2( the carrier of [:s9,ST:])
t `2 is M2( the carrier of ST)
the carrier of ST is non empty set
t1 `2 is M2( the carrier of ST)
y `2 is set
t `1 is M2( the carrier of s9)
the carrier of s9 is non empty set
t1 `1 is M2( the carrier of s9)
y `1 is set
[(t `1),(t `2)] is V1() M2( the carrier of [:s9,ST:])
{(t `1),(t `2)} is non empty set
{(t `1)} is non empty set
{{(t `1),(t `2)},{(t `1)}} is non empty set
S is RelStr
T is RelStr
[:S,T:] is strict RelStr
the carrier of [:S,T:] is set
bool the carrier of [:S,T:] is non empty set
x is M2( bool the carrier of [:S,T:])
downarrow x is M2( bool the carrier of [:S,T:])
proj1 (downarrow x) is M2( bool the carrier of S)
the carrier of S is set
bool the carrier of S is non empty set
proj1 x is M2( bool the carrier of S)
downarrow (proj1 x) is M2( bool the carrier of S)
proj2 (downarrow x) is M2( bool the carrier of T)
the carrier of T is set
bool the carrier of T is non empty set
proj2 x is M2( bool the carrier of T)
downarrow (proj2 x) is M2( bool the carrier of T)
[: the carrier of S, the carrier of T:] is V7() set
y is set
y is set
[y,y] is V1() set
{y,y} is non empty set
{y} is non empty set
{{y,y},{y}} is non empty set
ST is non empty RelStr
the carrier of ST is non empty set
s9 is non empty RelStr
the carrier of s9 is non empty set
[:s9,ST:] is non empty strict RelStr
the carrier of [:s9,ST:] is non empty set
t1 is M2( the carrier of s9)
t is M2( the carrier of ST)
[t1,t] is V1() M2( the carrier of [:s9,ST:])
{t1,t} is non empty set
{t1} is non empty set
{{t1,t},{t1}} is non empty set
s2 is M2( the carrier of [:s9,ST:])
s2 `1 is M2( the carrier of s9)
s2 `2 is M2( the carrier of ST)
[(s2 `1),(s2 `2)] is V1() M2( the carrier of [:s9,ST:])
{(s2 `1),(s2 `2)} is non empty set
{(s2 `1)} is non empty set
{{(s2 `1),(s2 `2)},{(s2 `1)}} is non empty set
y is set
y is set
[y,y] is V1() set
{y,y} is non empty set
{y} is non empty set
{{y,y},{y}} is non empty set
ST is non empty RelStr
the carrier of ST is non empty set
s9 is non empty RelStr
the carrier of s9 is non empty set
[:s9,ST:] is non empty strict RelStr
the carrier of [:s9,ST:] is non empty set
t1 is M2( the carrier of s9)
t is M2( the carrier of ST)
[t1,t] is V1() M2( the carrier of [:s9,ST:])
{t1,t} is non empty set
{t1} is non empty set
{{t1,t},{t1}} is non empty set
s2 is M2( the carrier of [:s9,ST:])
s2 `1 is M2( the carrier of s9)
s2 `2 is M2( the carrier of ST)
[(s2 `1),(s2 `2)] is V1() M2( the carrier of [:s9,ST:])
{(s2 `1),(s2 `2)} is non empty set
{(s2 `1)} is non empty set
{{(s2 `1),(s2 `2)},{(s2 `1)}} is non empty set
S is RelStr
T is reflexive RelStr
[:S,T:] is strict RelStr
the carrier of [:S,T:] is set
bool the carrier of [:S,T:] is non empty set
x is M2( bool the carrier of [:S,T:])
downarrow x is M2( bool the carrier of [:S,T:])
proj1 (downarrow x) is M2( bool the carrier of S)
the carrier of S is set
bool the carrier of S is non empty set
proj1 x is M2( bool the carrier of S)
downarrow (proj1 x) is M2( bool the carrier of S)
y is set
y is non empty RelStr
the carrier of y is non empty set
s9 is M2( the carrier of y)
ST is M2( the carrier of y)
t is set
[ST,t] is V1() set
{ST,t} is non empty set
{ST} is non empty set
{{ST,t},{ST}} is non empty set
the carrier of T is set
[: the carrier of S, the carrier of T:] is V7() set
t1 is non empty reflexive non void RelStr
the carrier of t1 is non empty set
s2 is M2( the carrier of t1)
[:y,t1:] is non empty strict RelStr
[s9,s2] is V1() M2( the carrier of [:y,t1:])
the carrier of [:y,t1:] is non empty set
{s9,s2} is non empty set
{s9} is non empty set
{{s9,s2},{s9}} is non empty set
[ST,s2] is V1() M2( the carrier of [:y,t1:])
{ST,s2} is non empty set
{{ST,s2},{ST}} is non empty set
S is reflexive RelStr
T is RelStr
[:S,T:] is strict RelStr
the carrier of [:S,T:] is set
bool the carrier of [:S,T:] is non empty set
x is M2( bool the carrier of [:S,T:])
downarrow x is M2( bool the carrier of [:S,T:])
proj2 (downarrow x) is M2( bool the carrier of T)
the carrier of T is set
bool the carrier of T is non empty set
proj2 x is M2( bool the carrier of T)
downarrow (proj2 x) is M2( bool the carrier of T)
y is set
y is non empty RelStr
the carrier of y is non empty set
s9 is M2( the carrier of y)
ST is M2( the carrier of y)
t is set
[t,ST] is V1() set
{t,ST} is non empty set
{t} is non empty set
{{t,ST},{t}} is non empty set
the carrier of S is set
[: the carrier of S, the carrier of T:] is V7() set
t1 is non empty reflexive non void RelStr
the carrier of t1 is non empty set
s2 is M2( the carrier of t1)
[:t1,y:] is non empty strict RelStr
[s2,s9] is V1() M2( the carrier of [:t1,y:])
the carrier of [:t1,y:] is non empty set
{s2,s9} is non empty set
{s2} is non empty set
{{s2,s9},{s2}} is non empty set
[s2,ST] is V1() M2( the carrier of [:t1,y:])
{s2,ST} is non empty set
{{s2,ST},{s2}} is non empty set
S is RelStr
T is RelStr
[:S,T:] is strict RelStr
the carrier of [:S,T:] is set
bool the carrier of [:S,T:] is non empty set
x is M2( bool the carrier of [:S,T:])
uparrow x is M2( bool the carrier of [:S,T:])
proj1 x is M2( bool the carrier of S)
the carrier of S is set
bool the carrier of S is non empty set
uparrow (proj1 x) is M2( bool the carrier of S)
proj2 x is M2( bool the carrier of T)
the carrier of T is set
bool the carrier of T is non empty set
uparrow (proj2 x) is M2( bool the carrier of T)
[:(uparrow (proj1 x)),(uparrow (proj2 x)):] is V7() M2( bool the carrier of [:S,T:])
y is set
[: the carrier of S, the carrier of T:] is V7() set
ST is set
t is set
[ST,t] is V1() set
{ST,t} is non empty set
{ST} is non empty set
{{ST,t},{ST}} is non empty set
y is non empty RelStr
s9 is non empty RelStr
[:y,s9:] is non empty strict RelStr
the carrier of [:y,s9:] is non empty set
ST is M2( the carrier of [:y,s9:])
t is M2( the carrier of [:y,s9:])
t `1 is M2( the carrier of y)
the carrier of y is non empty set
ST `1 is M2( the carrier of y)
t `2 is M2( the carrier of s9)
the carrier of s9 is non empty set
[(t `1),(t `2)] is V1() M2( the carrier of [:y,s9:])
{(t `1),(t `2)} is non empty set
{(t `1)} is non empty set
{{(t `1),(t `2)},{(t `1)}} is non empty set
y `1 is set
ST `2 is M2( the carrier of s9)
y `2 is set
[(ST `1),(ST `2)] is V1() M2( the carrier of [:y,s9:])
{(ST `1),(ST `2)} is non empty set
{(ST `1)} is non empty set
{{(ST `1),(ST `2)},{(ST `1)}} is non empty set
S is RelStr
the carrier of S is set
bool the carrier of S is non empty set
T is RelStr
the carrier of T is set
bool the carrier of T is non empty set
[:S,T:] is strict RelStr
x is M2( bool the carrier of S)
uparrow x is M2( bool the carrier of S)
y is M2( bool the carrier of T)
uparrow y is M2( bool the carrier of T)
[:(uparrow x),(uparrow y):] is V7() M2( bool the carrier of [:S,T:])
the carrier of [:S,T:] is set
bool the carrier of [:S,T:] is non empty set
[:x,y:] is V7() M2( bool the carrier of [:S,T:])
uparrow [:x,y:] is M2( bool the carrier of [:S,T:])
y is set
s9 is set
ST is set
[s9,ST] is V1() set
{s9,ST} is non empty set
{s9} is non empty set
{{s9,ST},{s9}} is non empty set
t is non empty RelStr
the carrier of t is non empty set
s2 is M2( the carrier of t)
t1 is M2( the carrier of t)
t1 is non empty RelStr
the carrier of t1 is non empty set
z is M2( the carrier of t1)
x is M2( the carrier of t1)
[t1,x] is V1() M2( the carrier of [:t,t1:])
[:t,t1:] is non empty strict RelStr
the carrier of [:t,t1:] is non empty set
{t1,x} is non empty set
{t1} is non empty set
{{t1,x},{t1}} is non empty set
[s2,z] is V1() M2( the carrier of [:t,t1:])
{s2,z} is non empty set
{s2} is non empty set
{{s2,z},{s2}} is non empty set
y is set
[: the carrier of S, the carrier of T:] is V7() set
t is set
t1 is set
[t,t1] is V1() set
{t,t1} is non empty set
{t} is non empty set
{{t,t1},{t}} is non empty set
s9 is non empty RelStr
ST is non empty RelStr
[:s9,ST:] is non empty strict RelStr
the carrier of [:s9,ST:] is non empty set
t is M2( the carrier of [:s9,ST:])
t1 is M2( the carrier of [:s9,ST:])
t1 `2 is M2( the carrier of ST)
the carrier of ST is non empty set
t `2 is M2( the carrier of ST)
y `2 is set
t1 `1 is M2( the carrier of s9)
the carrier of s9 is non empty set
t `1 is M2( the carrier of s9)
y `1 is set
[(t `1),(t `2)] is V1() M2( the carrier of [:s9,ST:])
{(t `1),(t `2)} is non empty set
{(t `1)} is non empty set
{{(t `1),(t `2)},{(t `1)}} is non empty set
S is RelStr
T is RelStr
[:S,T:] is strict RelStr
the carrier of [:S,T:] is set
bool the carrier of [:S,T:] is non empty set
x is M2( bool the carrier of [:S,T:])
uparrow x is M2( bool the carrier of [:S,T:])
proj1 (uparrow x) is M2( bool the carrier of S)
the carrier of S is set
bool the carrier of S is non empty set
proj1 x is M2( bool the carrier of S)
uparrow (proj1 x) is M2( bool the carrier of S)
proj2 (uparrow x) is M2( bool the carrier of T)
the carrier of T is set
bool the carrier of T is non empty set
proj2 x is M2( bool the carrier of T)
uparrow (proj2 x) is M2( bool the carrier of T)
[: the carrier of S, the carrier of T:] is V7() set
y is set
y is set
[y,y] is V1() set
{y,y} is non empty set
{y} is non empty set
{{y,y},{y}} is non empty set
ST is non empty RelStr
the carrier of ST is non empty set
s9 is non empty RelStr
the carrier of s9 is non empty set
[:s9,ST:] is non empty strict RelStr
the carrier of [:s9,ST:] is non empty set
t1 is M2( the carrier of s9)
t is M2( the carrier of ST)
[t1,t] is V1() M2( the carrier of [:s9,ST:])
{t1,t} is non empty set
{t1} is non empty set
{{t1,t},{t1}} is non empty set
s2 is M2( the carrier of [:s9,ST:])
s2 `1 is M2( the carrier of s9)
s2 `2 is M2( the carrier of ST)
[(s2 `1),(s2 `2)] is V1() M2( the carrier of [:s9,ST:])
{(s2 `1),(s2 `2)} is non empty set
{(s2 `1)} is non empty set
{{(s2 `1),(s2 `2)},{(s2 `1)}} is non empty set
y is set
y is set
[y,y] is V1() set
{y,y} is non empty set
{y} is non empty set
{{y,y},{y}} is non empty set
ST is non empty RelStr
the carrier of ST is non empty set
s9 is non empty RelStr
the carrier of s9 is non empty set
[:s9,ST:] is non empty strict RelStr
the carrier of [:s9,ST:] is non empty set
t1 is M2( the carrier of s9)
t is M2( the carrier of ST)
[t1,t] is V1() M2( the carrier of [:s9,ST:])
{t1,t} is non empty set
{t1} is non empty set
{{t1,t},{t1}} is non empty set
s2 is M2( the carrier of [:s9,ST:])
s2 `1 is M2( the carrier of s9)
s2 `2 is M2( the carrier of ST)
[(s2 `1),(s2 `2)] is V1() M2( the carrier of [:s9,ST:])
{(s2 `1),(s2 `2)} is non empty set
{(s2 `1)} is non empty set
{{(s2 `1),(s2 `2)},{(s2 `1)}} is non empty set
S is RelStr
T is reflexive RelStr
[:S,T:] is strict RelStr
the carrier of [:S,T:] is set
bool the carrier of [:S,T:] is non empty set
x is M2( bool the carrier of [:S,T:])
uparrow x is M2( bool the carrier of [:S,T:])
proj1 (uparrow x) is M2( bool the carrier of S)
the carrier of S is set
bool the carrier of S is non empty set
proj1 x is M2( bool the carrier of S)
uparrow (proj1 x) is M2( bool the carrier of S)
y is set
y is non empty RelStr
the carrier of y is non empty set
s9 is M2( the carrier of y)
ST is M2( the carrier of y)
t is set
[ST,t] is V1() set
{ST,t} is non empty set
{ST} is non empty set
{{ST,t},{ST}} is non empty set
the carrier of T is set
[: the carrier of S, the carrier of T:] is V7() set
t1 is non empty reflexive non void RelStr
the carrier of t1 is non empty set
s2 is M2( the carrier of t1)
[:y,t1:] is non empty strict RelStr
[ST,s2] is V1() M2( the carrier of [:y,t1:])
the carrier of [:y,t1:] is non empty set
{ST,s2} is non empty set
{{ST,s2},{ST}} is non empty set
[s9,s2] is V1() M2( the carrier of [:y,t1:])
{s9,s2} is non empty set
{s9} is non empty set
{{s9,s2},{s9}} is non empty set
S is reflexive RelStr
T is RelStr
[:S,T:] is strict RelStr
the carrier of [:S,T:] is set
bool the carrier of [:S,T:] is non empty set
x is M2( bool the carrier of [:S,T:])
uparrow x is M2( bool the carrier of [:S,T:])
proj2 (uparrow x) is M2( bool the carrier of T)
the carrier of T is set
bool the carrier of T is non empty set
proj2 x is M2( bool the carrier of T)
uparrow (proj2 x) is M2( bool the carrier of T)
y is set
y is non empty RelStr
the carrier of y is non empty set
s9 is M2( the carrier of y)
ST is M2( the carrier of y)
t is set
[t,ST] is V1() set
{t,ST} is non empty set
{t} is non empty set
{{t,ST},{t}} is non empty set
the carrier of S is set
[: the carrier of S, the carrier of T:] is V7() set
t1 is non empty reflexive non void RelStr
the carrier of t1 is non empty set
s2 is M2( the carrier of t1)
[:t1,y:] is non empty strict RelStr
[s2,ST] is V1() M2( the carrier of [:t1,y:])
the carrier of [:t1,y:] is non empty set
{s2,ST} is non empty set
{s2} is non empty set
{{s2,ST},{s2}} is non empty set
[s2,s9] is V1() M2( the carrier of [:t1,y:])
{s2,s9} is non empty set
{{s2,s9},{s2}} is non empty set
S is non empty RelStr
the carrier of S is non empty set
T is non empty RelStr
the carrier of T is non empty set
[:S,T:] is non empty strict RelStr
x is M2( the carrier of S)
downarrow x is M2( bool the carrier of S)
bool the carrier of S is non empty set
{x} is non empty M2( bool the carrier of S)
downarrow {x} is M2( bool the carrier of S)
y is M2( the carrier of T)
downarrow y is M2( bool the carrier of T)
bool the carrier of T is non empty set
{y} is non empty M2( bool the carrier of T)
downarrow {y} is M2( bool the carrier of T)
[:(downarrow x),(downarrow y):] is V7() M2( bool the carrier of [:S,T:])
the carrier of [:S,T:] is non empty set
bool the carrier of [:S,T:] is non empty set
[x,y] is V1() M2( the carrier of [:S,T:])
{x,y} is non empty set
{x} is non empty set
{{x,y},{x}} is non empty set
downarrow [x,y] is M2( bool the carrier of [:S,T:])
{[x,y]} is non empty V7() M2( bool the carrier of [:S,T:])
downarrow {[x,y]} is M2( bool the carrier of [:S,T:])
y is set
s9 is set
ST is set
[s9,ST] is V1() set
{s9,ST} is non empty set
{s9} is non empty set
{{s9,ST},{s9}} is non empty set
t1 is M2( the carrier of S)
t is M2( the carrier of T)
[t1,t] is V1() M2( the carrier of [:S,T:])
{t1,t} is non empty set
{t1} is non empty set
{{t1,t},{t1}} is non empty set
y is set
[: the carrier of S, the carrier of T:] is non empty V7() set
s9 is M2( the carrier of [:S,T:])
s9 `1 is M2( the carrier of S)
s9 `2 is M2( the carrier of T)
[(s9 `1),(s9 `2)] is V1() M2( the carrier of [:S,T:])
{(s9 `1),(s9 `2)} is non empty set
{(s9 `1)} is non empty set
{{(s9 `1),(s9 `2)},{(s9 `1)}} is non empty set
y `2 is set
y `1 is set
S is non empty RelStr
T is non empty RelStr
[:S,T:] is non empty strict RelStr
the carrier of [:S,T:] is non empty set
x is M2( the carrier of [:S,T:])
downarrow x is M2( bool the carrier of [:S,T:])
bool the carrier of [:S,T:] is non empty set
{x} is non empty M2( bool the carrier of [:S,T:])
downarrow {x} is M2( bool the carrier of [:S,T:])
proj1 (downarrow x) is M2( bool the carrier of S)
the carrier of S is non empty set
bool the carrier of S is non empty set
x `1 is M2( the carrier of S)
downarrow (x `1) is M2( bool the carrier of S)
{(x `1)} is non empty M2( bool the carrier of S)
downarrow {(x `1)} is M2( bool the carrier of S)
proj2 (downarrow x) is M2( bool the carrier of T)
the carrier of T is non empty set
bool the carrier of T is non empty set
x `2 is M2( the carrier of T)
downarrow (x `2) is M2( bool the carrier of T)
{(x `2)} is non empty M2( bool the carrier of T)
downarrow {(x `2)} is M2( bool the carrier of T)
[: the carrier of S, the carrier of T:] is non empty V7() set
[(x `1),(x `2)] is V1() M2( the carrier of [:S,T:])
{(x `1),(x `2)} is non empty set
{(x `1)} is non empty set
{{(x `1),(x `2)},{(x `1)}} is non empty set
y is set
y is set
[y,y] is V1() set
{y,y} is non empty set
{y} is non empty set
{{y,y},{y}} is non empty set
ST is M2( the carrier of S)
s9 is M2( the carrier of T)
[ST,s9] is V1() M2( the carrier of [:S,T:])
{ST,s9} is non empty set
{ST} is non empty set
{{ST,s9},{ST}} is non empty set
y is set
y is set
[y,y] is V1() set
{y,y} is non empty set
{y} is non empty set
{{y,y},{y}} is non empty set
s9 is M2( the carrier of S)
ST is M2( the carrier of T)
[s9,ST] is V1() M2( the carrier of [:S,T:])
{s9,ST} is non empty set
{s9} is non empty set
{{s9,ST},{s9}} is non empty set
S is non empty RelStr
T is non empty reflexive non void RelStr
[:S,T:] is non empty strict RelStr
the carrier of [:S,T:] is non empty set
x is M2( the carrier of [:S,T:])
downarrow x is M2( bool the carrier of [:S,T:])
bool the carrier of [:S,T:] is non empty set
{x} is non empty M2( bool the carrier of [:S,T:])
downarrow {x} is M2( bool the carrier of [:S,T:])
proj1 (downarrow x) is M2( bool the carrier of S)
the carrier of S is non empty set
bool the carrier of S is non empty set
x `1 is M2( the carrier of S)
downarrow (x `1) is M2( bool the carrier of S)
{(x `1)} is non empty M2( bool the carrier of S)
downarrow {(x `1)} is M2( bool the carrier of S)
x `2 is M2( the carrier of T)
the carrier of T is non empty set
y is set
y is M2( the carrier of S)
[y,(x `2)] is V1() M2( the carrier of [:S,T:])
{y,(x `2)} is non empty set
{y} is non empty set
{{y,(x `2)},{y}} is non empty set
[(x `1),(x `2)] is V1() M2( the carrier of [:S,T:])
{(x `1),(x `2)} is non empty set
{(x `1)} is non empty set
{{(x `1),(x `2)},{(x `1)}} is non empty set
downarrow [(x `1),(x `2)] is M2( bool the carrier of [:S,T:])
{[(x `1),(x `2)]} is non empty V7() M2( bool the carrier of [:S,T:])
downarrow {[(x `1),(x `2)]} is M2( bool the carrier of [:S,T:])
[: the carrier of S, the carrier of T:] is non empty V7() set
S is non empty reflexive non void RelStr
T is non empty RelStr
[:S,T:] is non empty strict RelStr
the carrier of [:S,T:] is non empty set
x is M2( the carrier of [:S,T:])
downarrow x is M2( bool the carrier of [:S,T:])
bool the carrier of [:S,T:] is non empty set
{x} is non empty M2( bool the carrier of [:S,T:])
downarrow {x} is M2( bool the carrier of [:S,T:])
proj2 (downarrow x) is M2( bool the carrier of T)
the carrier of T is non empty set
bool the carrier of T is non empty set
x `2 is M2( the carrier of T)
downarrow (x `2) is M2( bool the carrier of T)
{(x `2)} is non empty M2( bool the carrier of T)
downarrow {(x `2)} is M2( bool the carrier of T)
x `1 is M2( the carrier of S)
the carrier of S is non empty set
y is set
y is M2( the carrier of T)
[(x `1),y] is V1() M2( the carrier of [:S,T:])
{(x `1),y} is non empty set
{(x `1)} is non empty set
{{(x `1),y},{(x `1)}} is non empty set
[(x `1),(x `2)] is V1() M2( the carrier of [:S,T:])
{(x `1),(x `2)} is non empty set
{{(x `1),(x `2)},{(x `1)}} is non empty set
downarrow [(x `1),(x `2)] is M2( bool the carrier of [:S,T:])
{[(x `1),(x `2)]} is non empty V7() M2( bool the carrier of [:S,T:])
downarrow {[(x `1),(x `2)]} is M2( bool the carrier of [:S,T:])
[: the carrier of S, the carrier of T:] is non empty V7() set
S is non empty RelStr
the carrier of S is non empty set
T is non empty RelStr
the carrier of T is non empty set
[:S,T:] is non empty strict RelStr
x is M2( the carrier of S)
uparrow x is M2( bool the carrier of S)
bool the carrier of S is non empty set
{x} is non empty M2( bool the carrier of S)
uparrow {x} is M2( bool the carrier of S)
y is M2( the carrier of T)
uparrow y is M2( bool the carrier of T)
bool the carrier of T is non empty set
{y} is non empty M2( bool the carrier of T)
uparrow {y} is M2( bool the carrier of T)
[:(uparrow x),(uparrow y):] is V7() M2( bool the carrier of [:S,T:])
the carrier of [:S,T:] is non empty set
bool the carrier of [:S,T:] is non empty set
[x,y] is V1() M2( the carrier of [:S,T:])
{x,y} is non empty set
{x} is non empty set
{{x,y},{x}} is non empty set
uparrow [x,y] is M2( bool the carrier of [:S,T:])
{[x,y]} is non empty V7() M2( bool the carrier of [:S,T:])
uparrow {[x,y]} is M2( bool the carrier of [:S,T:])
y is set
s9 is set
ST is set
[s9,ST] is V1() set
{s9,ST} is non empty set
{s9} is non empty set
{{s9,ST},{s9}} is non empty set
t1 is M2( the carrier of S)
t is M2( the carrier of T)
[t1,t] is V1() M2( the carrier of [:S,T:])
{t1,t} is non empty set
{t1} is non empty set
{{t1,t},{t1}} is non empty set
y is set
[: the carrier of S, the carrier of T:] is non empty V7() set
s9 is M2( the carrier of [:S,T:])
s9 `1 is M2( the carrier of S)
s9 `2 is M2( the carrier of T)
[(s9 `1),(s9 `2)] is V1() M2( the carrier of [:S,T:])
{(s9 `1),(s9 `2)} is non empty set
{(s9 `1)} is non empty set
{{(s9 `1),(s9 `2)},{(s9 `1)}} is non empty set
y `2 is set
y `1 is set
S is non empty RelStr
T is non empty RelStr
[:S,T:] is non empty strict RelStr
the carrier of [:S,T:] is non empty set
x is M2( the carrier of [:S,T:])
uparrow x is M2( bool the carrier of [:S,T:])
bool the carrier of [:S,T:] is non empty set
{x} is non empty M2( bool the carrier of [:S,T:])
uparrow {x} is M2( bool the carrier of [:S,T:])
proj1 (uparrow x) is M2( bool the carrier of S)
the carrier of S is non empty set
bool the carrier of S is non empty set
x `1 is M2( the carrier of S)
uparrow (x `1) is M2( bool the carrier of S)
{(x `1)} is non empty M2( bool the carrier of S)
uparrow {(x `1)} is M2( bool the carrier of S)
proj2 (uparrow x) is M2( bool the carrier of T)
the carrier of T is non empty set
bool the carrier of T is non empty set
x `2 is M2( the carrier of T)
uparrow (x `2) is M2( bool the carrier of T)
{(x `2)} is non empty M2( bool the carrier of T)
uparrow {(x `2)} is M2( bool the carrier of T)
[: the carrier of S, the carrier of T:] is non empty V7() set
[(x `1),(x `2)] is V1() M2( the carrier of [:S,T:])
{(x `1),(x `2)} is non empty set
{(x `1)} is non empty set
{{(x `1),(x `2)},{(x `1)}} is non empty set
y is set
y is set
[y,y] is V1() set
{y,y} is non empty set
{y} is non empty set
{{y,y},{y}} is non empty set
ST is M2( the carrier of S)
s9 is M2( the carrier of T)
[ST,s9] is V1() M2( the carrier of [:S,T:])
{ST,s9} is non empty set
{ST} is non empty set
{{ST,s9},{ST}} is non empty set
y is set
y is set
[y,y] is V1() set
{y,y} is non empty set
{y} is non empty set
{{y,y},{y}} is non empty set
s9 is M2( the carrier of S)
ST is M2( the carrier of T)
[s9,ST] is V1() M2( the carrier of [:S,T:])
{s9,ST} is non empty set
{s9} is non empty set
{{s9,ST},{s9}} is non empty set
S is non empty RelStr
T is non empty reflexive non void RelStr
[:S,T:] is non empty strict RelStr
the carrier of [:S,T:] is non empty set
x is M2( the carrier of [:S,T:])
uparrow x is M2( bool the carrier of [:S,T:])
bool the carrier of [:S,T:] is non empty set
{x} is non empty M2( bool the carrier of [:S,T:])
uparrow {x} is M2( bool the carrier of [:S,T:])
proj1 (uparrow x) is M2( bool the carrier of S)
the carrier of S is non empty set
bool the carrier of S is non empty set
x `1 is M2( the carrier of S)
uparrow (x `1) is M2( bool the carrier of S)
{(x `1)} is non empty M2( bool the carrier of S)
uparrow {(x `1)} is M2( bool the carrier of S)
x `2 is M2( the carrier of T)
the carrier of T is non empty set
y is set
y is M2( the carrier of S)
[(x `1),(x `2)] is V1() M2( the carrier of [:S,T:])
{(x `1),(x `2)} is non empty set
{(x `1)} is non empty set
{{(x `1),(x `2)},{(x `1)}} is non empty set
[y,(x `2)] is V1() M2( the carrier of [:S,T:])
{y,(x `2)} is non empty set
{y} is non empty set
{{y,(x `2)},{y}} is non empty set
uparrow [(x `1),(x `2)] is M2( bool the carrier of [:S,T:])
{[(x `1),(x `2)]} is non empty V7() M2( bool the carrier of [:S,T:])
uparrow {[(x `1),(x `2)]} is M2( bool the carrier of [:S,T:])
[: the carrier of S, the carrier of T:] is non empty V7() set
S is non empty reflexive non void RelStr
T is non empty RelStr
[:S,T:] is non empty strict RelStr
the carrier of [:S,T:] is non empty set
x is M2( the carrier of [:S,T:])
uparrow x is M2( bool the carrier of [:S,T:])
bool the carrier of [:S,T:] is non empty set
{x} is non empty M2( bool the carrier of [:S,T:])
uparrow {x} is M2( bool the carrier of [:S,T:])
proj2 (uparrow x) is M2( bool the carrier of T)
the carrier of T is non empty set
bool the carrier of T is non empty set
x `2 is M2( the carrier of T)
uparrow (x `2) is M2( bool the carrier of T)
{(x `2)} is non empty M2( bool the carrier of T)
uparrow {(x `2)} is M2( bool the carrier of T)
x `1 is M2( the carrier of S)
the carrier of S is non empty set
y is set
y is M2( the carrier of T)
[(x `1),(x `2)] is V1() M2( the carrier of [:S,T:])
{(x `1),(x `2)} is non empty set
{(x `1)} is non empty set
{{(x `1),(x `2)},{(x `1)}} is non empty set
[(x `1),y] is V1() M2( the carrier of [:S,T:])
{(x `1),y} is non empty set
{{(x `1),y},{(x `1)}} is non empty set
uparrow [(x `1),(x `2)] is M2( bool the carrier of [:S,T:])
{[(x `1),(x `2)]} is non empty V7() M2( bool the carrier of [:S,T:])
uparrow {[(x `1),(x `2)]} is M2( bool the carrier of [:S,T:])
[: the carrier of S, the carrier of T:] is non empty V7() set
S is non empty reflexive transitive antisymmetric up-complete non void RelStr
the carrier of S is non empty set
T is non empty reflexive transitive antisymmetric up-complete non void RelStr
the carrier of T is non empty set
[:S,T:] is non empty strict reflexive transitive antisymmetric up-complete non void RelStr
x is M2( the carrier of S)
waybelow x is lower M2( bool the carrier of S)
bool the carrier of S is non empty set
{ b₁ where b₁ is M2( the carrier of S) : b₁ is_way_below x } is set
y is M2( the carrier of T)
waybelow y is lower M2( bool the carrier of T)
bool the carrier of T is non empty set
{ b₁ where b₁ is M2( the carrier of T) : b₁ is_way_below y } is set
[:(waybelow x),(waybelow y):] is V7() lower M2( bool the carrier of [:S,T:])
the carrier of [:S,T:] is non empty set
bool the carrier of [:S,T:] is non empty set
[x,y] is V1() M2( the carrier of [:S,T:])
{x,y} is non empty set
{x} is non empty set
{{x,y},{x}} is non empty set
waybelow [x,y] is lower M2( bool the carrier of [:S,T:])
{ b₁ where b₁ is M2( the carrier of [:S,T:]) : b₁ is_way_below [x,y] } is set
y is set
s9 is set
ST is set
[s9,ST] is V1() set
{s9,ST} is non empty set
{s9} is non empty set
{{s9,ST},{s9}} is non empty set
t1 is M2( the carrier of S)
t is M2( the carrier of T)
[t1,t] is V1() M2( the carrier of [:S,T:])
{t1,t} is non empty set
{t1} is non empty set
{{t1,t},{t1}} is non empty set
y is set
[: the carrier of S, the carrier of T:] is non empty V7() set
s9 is M2( the carrier of [:S,T:])
s9 `1 is M2( the carrier of S)
s9 `2 is M2( the carrier of T)
[(s9 `1),(s9 `2)] is V1() M2( the carrier of [:S,T:])
{(s9 `1),(s9 `2)} is non empty set
{(s9 `1)} is non empty set
{{(s9 `1),(s9 `2)},{(s9 `1)}} is non empty set
y `2 is set
y `1 is set
S is non empty reflexive antisymmetric up-complete non void RelStr
T is non empty reflexive antisymmetric up-complete non void RelStr
[:S,T:] is non empty strict reflexive antisymmetric up-complete non void RelStr
the carrier of [:S,T:] is non empty set
x is M2( the carrier of [:S,T:])
waybelow x is M2( bool the carrier of [:S,T:])
bool the carrier of [:S,T:] is non empty set
{ b₁ where b₁ is M2( the carrier of [:S,T:]) : b₁ is_way_below x } is set
proj1 (waybelow x) is M2( bool the carrier of S)
the carrier of S is non empty set
bool the carrier of S is non empty set
x `1 is M2( the carrier of S)
waybelow (x `1) is M2( bool the carrier of S)
{ b₁ where b₁ is M2( the carrier of S) : b₁ is_way_below x `1 } is set
proj2 (waybelow x) is M2( bool the carrier of T)
the carrier of T is non empty set
bool the carrier of T is non empty set
x `2 is M2( the carrier of T)
waybelow (x `2) is M2( bool the carrier of T)
{ b<sub>1</sub> where b<sub>1</sub> is M2( the carrier of T) : b<sub>1</sub> is_way_below x `2 } is set
[: the carrier of S, the carrier of T:] is non empty V7() set
[(x `1),(x `2)] is V1() M2( the carrier of [:S,T:])
{(x `1),(x `2)} is non empty set
{(x `1)} is non empty set
{{(x `1),(x `2)},{(x `1)}} is non empty set
y is set
y is set
[y,y] is V1() set
{y,y} is non empty set
{y} is non empty set
{{y,y},{y}} is non empty set
ST is M2( the carrier of S)
s9 is M2( the carrier of T)
[ST,s9] is V1() M2( the carrier of [:S,T:])
{ST,s9} is non empty set
{ST} is non empty set
{{ST,s9},{ST}} is non empty set
y is set
y is set
[y,y] is V1() set
{y,y} is non empty set
{y} is non empty set
{{y,y},{y}} is non empty set
s9 is M2( the carrier of S)
ST is M2( the carrier of T)
[s9,ST] is V1() M2( the carrier of [:S,T:])
{s9,ST} is non empty set
{s9} is non empty set
{{s9,ST},{s9}} is non empty set
S is non empty reflexive transitive antisymmetric up-complete non void RelStr
T is non empty reflexive transitive antisymmetric lower-bounded up-complete non void RelStr
[:S,T:] is non empty strict reflexive transitive antisymmetric up-complete non void RelStr
the carrier of [:S,T:] is non empty set
x is M2( the carrier of [:S,T:])
waybelow x is lower M2( bool the carrier of [:S,T:])
bool the carrier of [:S,T:] is non empty set
{ b₁ where b₁ is M2( the carrier of [:S,T:]) : b₁ is_way_below x } is set
proj1 (waybelow x) is M2( bool the carrier of S)
the carrier of S is non empty set
bool the carrier of S is non empty set
x `1 is M2( the carrier of S)
waybelow (x `1) is lower M2( bool the carrier of S)
{ b₁ where b₁ is M2( the carrier of S) : b₁ is_way_below x `1 } is set
Bottom T is M2( the carrier of T)
the carrier of T is non empty set
"\/" ({},T) is M2( the carrier of T)
x `2 is M2( the carrier of T)
y is set
y is M2( the carrier of S)
[y,(Bottom T)] is V1() M2( the carrier of [:S,T:])
{y,(Bottom T)} is non empty set
{y} is non empty set
{{y,(Bottom T)},{y}} is non empty set
[(x `1),(x `2)] is V1() M2( the carrier of [:S,T:])
{(x `1),(x `2)} is non empty set
{(x `1)} is non empty set
{{(x `1),(x `2)},{(x `1)}} is non empty set
waybelow [(x `1),(x `2)] is lower M2( bool the carrier of [:S,T:])
{ b₁ where b₁ is M2( the carrier of [:S,T:]) : b₁ is_way_below [(x `1),(x `2)] } is set
[: the carrier of S, the carrier of T:] is non empty V7() set
S is non empty reflexive transitive antisymmetric lower-bounded up-complete non void RelStr
T is non empty reflexive transitive antisymmetric up-complete non void RelStr
[:S,T:] is non empty strict reflexive transitive antisymmetric up-complete non void RelStr
the carrier of [:S,T:] is non empty set
x is M2( the carrier of [:S,T:])
waybelow x is lower M2( bool the carrier of [:S,T:])
bool the carrier of [:S,T:] is non empty set
{ b₁ where b₁ is M2( the carrier of [:S,T:]) : b₁ is_way_below x } is set
proj2 (waybelow x) is M2( bool the carrier of T)
the carrier of T is non empty set
bool the carrier of T is non empty set
x `2 is M2( the carrier of T)
waybelow (x `2) is lower M2( bool the carrier of T)
{ b₁ where b₁ is M2( the carrier of T) : b₁ is_way_below x `2 } is set
Bottom S is M2( the carrier of S)
the carrier of S is non empty set
"\/" ({},S) is M2( the carrier of S)
x `1 is M2( the carrier of S)
y is set
y is M2( the carrier of T)
[(Bottom S),y] is V1() M2( the carrier of [:S,T:])
{(Bottom S),y} is non empty set
{(Bottom S)} is non empty set
{{(Bottom S),y},{(Bottom S)}} is non empty set
[(x `1),(x `2)] is V1() M2( the carrier of [:S,T:])
{(x `1),(x `2)} is non empty set
{(x `1)} is non empty set
{{(x `1),(x `2)},{(x `1)}} is non empty set
waybelow [(x `1),(x `2)] is lower M2( bool the carrier of [:S,T:])
{ b₁ where b₁ is M2( the carrier of [:S,T:]) : b₁ is_way_below [(x `1),(x `2)] } is set
[: the carrier of S, the carrier of T:] is non empty V7() set
S is non empty reflexive transitive antisymmetric up-complete non void RelStr
the carrier of S is non empty set
T is non empty reflexive transitive antisymmetric up-complete non void RelStr
the carrier of T is non empty set
[:S,T:] is non empty strict reflexive transitive antisymmetric up-complete non void RelStr
x is M2( the carrier of S)
wayabove x is upper M2( bool the carrier of S)
bool the carrier of S is non empty set
{ b₁ where b₁ is M2( the carrier of S) : x is_way_below b₁ } is set
y is M2( the carrier of T)
wayabove y is upper M2( bool the carrier of T)
bool the carrier of T is non empty set
{ b₁ where b₁ is M2( the carrier of T) : y is_way_below b₁ } is set
[:(wayabove x),(wayabove y):] is V7() upper M2( bool the carrier of [:S,T:])
the carrier of [:S,T:] is non empty set
bool the carrier of [:S,T:] is non empty set
[x,y] is V1() M2( the carrier of [:S,T:])
{x,y} is non empty set
{x} is non empty set
{{x,y},{x}} is non empty set
wayabove [x,y] is upper M2( bool the carrier of [:S,T:])
{ b₁ where b₁ is M2( the carrier of [:S,T:]) : [x,y] is_way_below b₁ } is set
y is set
s9 is set
ST is set
[s9,ST] is V1() set
{s9,ST} is non empty set
{s9} is non empty set
{{s9,ST},{s9}} is non empty set
t1 is M2( the carrier of S)
t is M2( the carrier of T)
[t1,t] is V1() M2( the carrier of [:S,T:])
{t1,t} is non empty set
{t1} is non empty set
{{t1,t},{t1}} is non empty set
y is set
[: the carrier of S, the carrier of T:] is non empty V7() set
s9 is M2( the carrier of [:S,T:])
s9 `1 is M2( the carrier of S)
s9 `2 is M2( the carrier of T)
[(s9 `1),(s9 `2)] is V1() M2( the carrier of [:S,T:])
{(s9 `1),(s9 `2)} is non empty set
{(s9 `1)} is non empty set
{{(s9 `1),(s9 `2)},{(s9 `1)}} is non empty set
y `2 is set
y `1 is set
S is non empty reflexive antisymmetric up-complete non void RelStr
T is non empty reflexive antisymmetric up-complete non void RelStr
[:S,T:] is non empty strict reflexive antisymmetric up-complete non void RelStr
the carrier of [:S,T:] is non empty set
x is M2( the carrier of [:S,T:])
wayabove x is M2( bool the carrier of [:S,T:])
bool the carrier of [:S,T:] is non empty set
{ b₁ where b₁ is M2( the carrier of [:S,T:]) : x is_way_below b₁ } is set
proj1 (wayabove x) is M2( bool the carrier of S)
the carrier of S is non empty set
bool the carrier of S is non empty set
x `1 is M2( the carrier of S)
wayabove (x `1) is M2( bool the carrier of S)
{ b₁ where b₁ is M2( the carrier of S) : x `1 is_way_below b<sub>1</sub> } is set
proj2 (wayabove x) is M2( bool the carrier of T)
the carrier of T is non empty set
bool the carrier of T is non empty set
x `2 is M2( the carrier of T)
wayabove (x `2) is M2( bool the carrier of T)
{ b<sub>1</sub> where b<sub>1</sub> is M2( the carrier of T) : x `2 is_way_below b₁ } is set
[: the carrier of S, the carrier of T:] is non empty V7() set
[(x `1),(x `2)] is V1() M2( the carrier of [:S,T:])
{(x `1),(x `2)} is non empty set
{(x `1)} is non empty set
{{(x `1),(x `2)},{(x `1)}} is non empty set
y is set
y is set
[y,y] is V1() set
{y,y} is non empty set
{y} is non empty set
{{y,y},{y}} is non empty set
ST is M2( the carrier of S)
s9 is M2( the carrier of T)
[ST,s9] is V1() M2( the carrier of [:S,T:])
{ST,s9} is non empty set
{ST} is non empty set
{{ST,s9},{ST}} is non empty set
y is set
y is set
[y,y] is V1() set
{y,y} is non empty set
{y} is non empty set
{{y,y},{y}} is non empty set
s9 is M2( the carrier of S)
ST is M2( the carrier of T)
[s9,ST] is V1() M2( the carrier of [:S,T:])
{s9,ST} is non empty set
{s9} is non empty set
{{s9,ST},{s9}} is non empty set
S is non empty reflexive transitive antisymmetric up-complete non void RelStr
the carrier of S is non empty set
T is non empty reflexive transitive antisymmetric up-complete non void RelStr
the carrier of T is non empty set
[:S,T:] is non empty strict reflexive transitive antisymmetric up-complete non void RelStr
x is M2( the carrier of S)
compactbelow x is M2( bool the carrier of S)
bool the carrier of S is non empty set
{ b₁ where b₁ is M2( the carrier of S) : ( b₁ <= x & b₁ is compact ) } is set
y is M2( the carrier of T)
compactbelow y is M2( bool the carrier of T)
bool the carrier of T is non empty set
{ b₁ where b₁ is M2( the carrier of T) : ( b₁ <= y & b₁ is compact ) } is set
[:(compactbelow x),(compactbelow y):] is V7() M2( bool the carrier of [:S,T:])
the carrier of [:S,T:] is non empty set
bool the carrier of [:S,T:] is non empty set
[x,y] is V1() M2( the carrier of [:S,T:])
{x,y} is non empty set
{x} is non empty set
{{x,y},{x}} is non empty set
compactbelow [x,y] is M2( bool the carrier of [:S,T:])
{ b₁ where b₁ is M2( the carrier of [:S,T:]) : ( b₁ <= [x,y] & b₁ is compact ) } is set
y is set
s9 is set
ST is set
[s9,ST] is V1() set
{s9,ST} is non empty set
{s9} is non empty set
{{s9,ST},{s9}} is non empty set
t1 is M2( the carrier of S)
t is M2( the carrier of T)
[t1,t] is V1() M2( the carrier of [:S,T:])
{t1,t} is non empty set
{t1} is non empty set
{{t1,t},{t1}} is non empty set
[t1,t] `1 is M2( the carrier of S)
[t1,t] `2 is M2( the carrier of T)
y is set
s9 is M2( the carrier of [:S,T:])
s9 `1 is M2( the carrier of S)
s9 `2 is M2( the carrier of T)
[: the carrier of S, the carrier of T:] is non empty V7() set
[(s9 `1),(s9 `2)] is V1() M2( the carrier of [:S,T:])
{(s9 `1),(s9 `2)} is non empty set
{(s9 `1)} is non empty set
{{(s9 `1),(s9 `2)},{(s9 `1)}} is non empty set
y `2 is set
y `1 is set
S is non empty reflexive antisymmetric up-complete non void RelStr
T is non empty reflexive antisymmetric up-complete non void RelStr
[:S,T:] is non empty strict reflexive antisymmetric up-complete non void RelStr
the carrier of [:S,T:] is non empty set
x is M2( the carrier of [:S,T:])
compactbelow x is M2( bool the carrier of [:S,T:])
bool the carrier of [:S,T:] is non empty set
{ b₁ where b₁ is M2( the carrier of [:S,T:]) : ( b₁ <= x & b₁ is compact ) } is set
proj1 (compactbelow x) is M2( bool the carrier of S)
the carrier of S is non empty set
bool the carrier of S is non empty set
x `1 is M2( the carrier of S)
compactbelow (x `1) is M2( bool the carrier of S)
{ b₁ where b₁ is M2( the carrier of S) : ( b₁ <= x `1 & b<sub>1</sub> is compact ) } is set
proj2 (compactbelow x) is M2( bool the carrier of T)
the carrier of T is non empty set
bool the carrier of T is non empty set
x `2 is M2( the carrier of T)
compactbelow (x `2) is M2( bool the carrier of T)
{ b<sub>1</sub> where b<sub>1</sub> is M2( the carrier of T) : ( b<sub>1</sub> <= x `2 & b₁ is compact ) } is set
[: the carrier of S, the carrier of T:] is non empty V7() set
[(x `1),(x `2)] is V1() M2( the carrier of [:S,T:])
{(x `1),(x `2)} is non empty set
{(x `1)} is non empty set
{{(x `1),(x `2)},{(x `1)}} is non empty set
y is set
y is set
[y,y] is V1() set
{y,y} is non empty set
{y} is non empty set
{{y,y},{y}} is non empty set
ST is M2( the carrier of S)
s9 is M2( the carrier of T)
[ST,s9] is V1() M2( the carrier of [:S,T:])
{ST,s9} is non empty set
{ST} is non empty set
{{ST,s9},{ST}} is non empty set
[ST,s9] `1 is M2( the carrier of S)
y is set
y is set
[y,y] is V1() set
{y,y} is non empty set
{y} is non empty set
{{y,y},{y}} is non empty set
s9 is M2( the carrier of S)
ST is M2( the carrier of T)
[s9,ST] is V1() M2( the carrier of [:S,T:])
{s9,ST} is non empty set
{s9} is non empty set
{{s9,ST},{s9}} is non empty set
[s9,ST] `2 is M2( the carrier of T)
S is non empty reflexive transitive antisymmetric up-complete non void RelStr
T is non empty reflexive transitive antisymmetric lower-bounded up-complete non void RelStr
[:S,T:] is non empty strict reflexive transitive antisymmetric up-complete non void RelStr
the carrier of [:S,T:] is non empty set
x is M2( the carrier of [:S,T:])
compactbelow x is M2( bool the carrier of [:S,T:])
bool the carrier of [:S,T:] is non empty set
{ b₁ where b₁ is M2( the carrier of [:S,T:]) : ( b₁ <= x & b₁ is compact ) } is set
proj1 (compactbelow x) is M2( bool the carrier of S)
the carrier of S is non empty set
bool the carrier of S is non empty set
x `1 is M2( the carrier of S)
compactbelow (x `1) is M2( bool the carrier of S)
{ b₁ where b₁ is M2( the carrier of S) : ( b₁ <= x `1 & b<sub>1</sub> is compact ) } is set
Bottom T is M2( the carrier of T)
the carrier of T is non empty set
"\/" ({},T) is M2( the carrier of T)
x `2 is M2( the carrier of T)
y is set
y is M2( the carrier of S)
[y,(Bottom T)] is V1() M2( the carrier of [:S,T:])
{y,(Bottom T)} is non empty set
{y} is non empty set
{{y,(Bottom T)},{y}} is non empty set
[(x `1),(x `2)] is V1() M2( the carrier of [:S,T:])
{(x `1),(x `2)} is non empty set
{(x `1)} is non empty set
{{(x `1),(x `2)},{(x `1)}} is non empty set
[: the carrier of S, the carrier of T:] is non empty V7() set
[y,(Bottom T)] `1 is M2( the carrier of S)
[y,(Bottom T)] `2 is M2( the carrier of T)
compactbelow [(x `1),(x `2)] is M2( bool the carrier of [:S,T:])
{ b₁ where b₁ is M2( the carrier of [:S,T:]) : ( b₁ <= [(x `1),(x `2)] & b₁ is compact ) } is set
S is non empty reflexive transitive antisymmetric lower-bounded up-complete non void RelStr
T is non empty reflexive transitive antisymmetric up-complete non void RelStr
[:S,T:] is non empty strict reflexive transitive antisymmetric up-complete non void RelStr
the carrier of [:S,T:] is non empty set
x is M2( the carrier of [:S,T:])
compactbelow x is M2( bool the carrier of [:S,T:])
bool the carrier of [:S,T:] is non empty set
{ b₁ where b₁ is M2( the carrier of [:S,T:]) : ( b₁ <= x & b₁ is compact ) } is set
proj2 (compactbelow x) is M2( bool the carrier of T)
the carrier of T is non empty set
bool the carrier of T is non empty set
x `2 is M2( the carrier of T)
compactbelow (x `2) is M2( bool the carrier of T)
{ b₁ where b₁ is M2( the carrier of T) : ( b₁ <= x `2 & b<sub>1</sub> is compact ) } is set
Bottom S is M2( the carrier of S)
the carrier of S is non empty set
"\/" ({},S) is M2( the carrier of S)
x `1 is M2( the carrier of S)
y is set
y is M2( the carrier of T)
[(Bottom S),y] is V1() M2( the carrier of [:S,T:])
{(Bottom S),y} is non empty set
{(Bottom S)} is non empty set
{{(Bottom S),y},{(Bottom S)}} is non empty set
[(x `1),(x `2)] is V1() M2( the carrier of [:S,T:])
{(x `1),(x `2)} is non empty set
{(x `1)} is non empty set
{{(x `1),(x `2)},{(x `1)}} is non empty set
[: the carrier of S, the carrier of T:] is non empty V7() set
[(Bottom S),y] `1 is M2( the carrier of S)
[(Bottom S),y] `2 is M2( the carrier of T)
compactbelow [(x `1),(x `2)] is M2( bool the carrier of [:S,T:])
{ b₁ where b₁ is M2( the carrier of [:S,T:]) : ( b₁ <= [(x `1),(x `2)] & b₁ is compact ) } is set
S is non empty reflexive non void RelStr
the carrier of S is non empty set
bool the carrier of S is non empty set
T is M2( bool the carrier of S)
x is M2( the carrier of S)
S is non empty reflexive antisymmetric up-complete non void RelStr
T is non empty reflexive antisymmetric up-complete non void RelStr
[:S,T:] is non empty strict reflexive antisymmetric up-complete non void RelStr
the carrier of [:S,T:] is non empty set
bool the carrier of [:S,T:] is non empty set
x is M2( bool the carrier of [:S,T:])
proj1 x is M2( bool the carrier of S)
the carrier of S is non empty set
bool the carrier of S is non empty set
proj2 x is M2( bool the carrier of T)
the carrier of T is non empty set
bool the carrier of T is non empty set
[: the carrier of S, the carrier of T:] is non empty V7() set
y is M2( the carrier of S)
y is set
[y,y] is V1() set
{y,y} is non empty set
{y} is non empty set
{{y,y},{y}} is non empty set
s9 is M2( the carrier of T)
[y,s9] is V1() M2( the carrier of [:S,T:])
{y,s9} is non empty set
{{y,s9},{y}} is non empty set
ST is M2( the carrier of [:S,T:])
ST `1 is M2( the carrier of S)
ST `2 is M2( the carrier of T)
[(ST `1),(ST `2)] is V1() M2( the carrier of [:S,T:])
{(ST `1),(ST `2)} is non empty set
{(ST `1)} is non empty set
{{(ST `1),(ST `2)},{(ST `1)}} is non empty set
t is M2( the carrier of S)
y is M2( the carrier of T)
y is set
[y,y] is V1() set
{y,y} is non empty set
{y} is non empty set
{{y,y},{y}} is non empty set
s9 is M2( the carrier of S)
[s9,y] is V1() M2( the carrier of [:S,T:])
{s9,y} is non empty set
{s9} is non empty set
{{s9,y},{s9}} is non empty set
ST is M2( the carrier of [:S,T:])
ST `2 is M2( the carrier of T)
t is M2( the carrier of T)
ST `1 is M2( the carrier of S)
[(ST `1),(ST `2)] is V1() M2( the carrier of [:S,T:])
{(ST `1),(ST `2)} is non empty set
{(ST `1)} is non empty set
{{(ST `1),(ST `2)},{(ST `1)}} is non empty set
S is non empty reflexive transitive antisymmetric up-complete non void RelStr
the carrier of S is non empty set
bool the carrier of S is non empty set
T is non empty reflexive transitive antisymmetric up-complete non void RelStr
the carrier of T is non empty set
bool the carrier of T is non empty set
[:S,T:] is non empty strict reflexive transitive antisymmetric up-complete non void RelStr
x is M2( bool the carrier of S)
y is M2( bool the carrier of T)
[:x,y:] is V7() M2( bool the carrier of [:S,T:])
the carrier of [:S,T:] is non empty set
bool the carrier of [:S,T:] is non empty set
y is M2( the carrier of [:S,T:])
y `1 is M2( the carrier of S)
y `2 is M2( the carrier of T)
[(y `1),(y `2)] is V1() M2( the carrier of [:S,T:])
{(y `1),(y `2)} is non empty set
{(y `1)} is non empty set
{{(y `1),(y `2)},{(y `1)}} is non empty set
s9 is M2( the carrier of S)
ST is M2( the carrier of T)
t is M2( the carrier of T)
[s9,t] is V1() M2( the carrier of [:S,T:])
{s9,t} is non empty set
{s9} is non empty set
{{s9,t},{s9}} is non empty set
S is non empty reflexive antisymmetric up-complete non void RelStr
T is non empty reflexive antisymmetric up-complete non void RelStr
[:S,T:] is non empty strict reflexive antisymmetric up-complete non void RelStr
the carrier of [:S,T:] is non empty set
bool the carrier of [:S,T:] is non empty set
x is M2( bool the carrier of [:S,T:])
proj1 x is M2( bool the carrier of S)
the carrier of S is non empty set
bool the carrier of S is non empty set
proj2 x is M2( bool the carrier of T)
the carrier of T is non empty set
bool the carrier of T is non empty set
[: the carrier of S, the carrier of T:] is non empty V7() set
y is non empty directed M2( bool the carrier of S)
"\/" (y,S) is M2( the carrier of S)
y is set
[("\/" (y,S)),y] is V1() set
{("\/" (y,S)),y} is non empty set
{("\/" (y,S))} is non empty set
{{("\/" (y,S)),y},{("\/" (y,S))}} is non empty set
{y} is non empty set
s9 is non empty directed M2( bool the carrier of T)
[:y,s9:] is non empty V7() directed M2( bool the carrier of [:S,T:])
"\/" ([:y,s9:],[:S,T:]) is M2( the carrier of [:S,T:])
proj1 [:y,s9:] is non empty M2( bool the carrier of S)
"\/" ((proj1 [:y,s9:]),S) is M2( the carrier of S)
proj2 [:y,s9:] is non empty M2( bool the carrier of T)
"\/" ((proj2 [:y,s9:]),T) is M2( the carrier of T)
[("\/" ((proj1 [:y,s9:]),S)),("\/" ((proj2 [:y,s9:]),T))] is V1() M2( the carrier of [:S,T:])
{("\/" ((proj1 [:y,s9:]),S)),("\/" ((proj2 [:y,s9:]),T))} is non empty set
{("\/" ((proj1 [:y,s9:]),S))} is non empty set
{{("\/" ((proj1 [:y,s9:]),S)),("\/" ((proj2 [:y,s9:]),T))},{("\/" ((proj1 [:y,s9:]),S))}} is non empty set
[("\/" (y,S)),("\/" ((proj2 [:y,s9:]),T))] is V1() M2( the carrier of [:S,T:])
{("\/" (y,S)),("\/" ((proj2 [:y,s9:]),T))} is non empty set
{{("\/" (y,S)),("\/" ((proj2 [:y,s9:]),T))},{("\/" (y,S))}} is non empty set
"\/" (s9,T) is M2( the carrier of T)
[("\/" (y,S)),("\/" (s9,T))] is V1() M2( the carrier of [:S,T:])
{("\/" (y,S)),("\/" (s9,T))} is non empty set
{{("\/" (y,S)),("\/" (s9,T))},{("\/" (y,S))}} is non empty set
[:y,{y}:] is non empty V7() set
ST is set
ST `1 is set
t is set
ST `2 is set
[t,(ST `2)] is V1() set
{t,(ST `2)} is non empty set
{t} is non empty set
{{t,(ST `2)},{t}} is non empty set
t is set
y is non empty directed M2( bool the carrier of T)
"\/" (y,T) is M2( the carrier of T)
y is set
[y,("\/" (y,T))] is V1() set
{y,("\/" (y,T))} is non empty set
{y} is non empty set
{{y,("\/" (y,T))},{y}} is non empty set
s9 is non empty directed M2( bool the carrier of S)
[:s9,y:] is non empty V7() directed M2( bool the carrier of [:S,T:])
"\/" ([:s9,y:],[:S,T:]) is M2( the carrier of [:S,T:])
proj1 [:s9,y:] is non empty M2( bool the carrier of S)
"\/" ((proj1 [:s9,y:]),S) is M2( the carrier of S)
proj2 [:s9,y:] is non empty M2( bool the carrier of T)
"\/" ((proj2 [:s9,y:]),T) is M2( the carrier of T)
[("\/" ((proj1 [:s9,y:]),S)),("\/" ((proj2 [:s9,y:]),T))] is V1() M2( the carrier of [:S,T:])
{("\/" ((proj1 [:s9,y:]),S)),("\/" ((proj2 [:s9,y:]),T))} is non empty set
{("\/" ((proj1 [:s9,y:]),S))} is non empty set
{{("\/" ((proj1 [:s9,y:]),S)),("\/" ((proj2 [:s9,y:]),T))},{("\/" ((proj1 [:s9,y:]),S))}} is non empty set
"\/" (s9,S) is M2( the carrier of S)
[("\/" (s9,S)),("\/" ((proj2 [:s9,y:]),T))] is V1() M2( the carrier of [:S,T:])
{("\/" (s9,S)),("\/" ((proj2 [:s9,y:]),T))} is non empty set
{("\/" (s9,S))} is non empty set
{{("\/" (s9,S)),("\/" ((proj2 [:s9,y:]),T))},{("\/" (s9,S))}} is non empty set
[("\/" (s9,S)),("\/" (y,T))] is V1() M2( the carrier of [:S,T:])
{("\/" (s9,S)),("\/" (y,T))} is non empty set
{{("\/" (s9,S)),("\/" (y,T))},{("\/" (s9,S))}} is non empty set
[:{y},y:] is non empty V7() set
ST is set
ST `2 is set
ST `1 is set
t is set
[(ST `1),t] is V1() set
{(ST `1),t} is non empty set
{(ST `1)} is non empty set
{{(ST `1),t},{(ST `1)}} is non empty set
t is set
S is non empty reflexive antisymmetric up-complete non void RelStr
the carrier of S is non empty set
bool the carrier of S is non empty set
T is non empty reflexive antisymmetric up-complete non void RelStr
the carrier of T is non empty set
bool the carrier of T is non empty set
[:S,T:] is non empty strict reflexive antisymmetric up-complete non void RelStr
x is upper M2( bool the carrier of S)
y is upper M2( bool the carrier of T)
[:x,y:] is V7() upper M2( bool the carrier of [:S,T:])
the carrier of [:S,T:] is non empty set
bool the carrier of [:S,T:] is non empty set
y is non empty directed M2( bool the carrier of [:S,T:])
"\/" (y,[:S,T:]) is M2( the carrier of [:S,T:])
proj1 y is M2( bool the carrier of S)
"\/" ((proj1 y),S) is M2( the carrier of S)
proj2 y is M2( bool the carrier of T)
"\/" ((proj2 y),T) is M2( the carrier of T)
[("\/" ((proj1 y),S)),("\/" ((proj2 y),T))] is V1() M2( the carrier of [:S,T:])
{("\/" ((proj1 y),S)),("\/" ((proj2 y),T))} is non empty set
{("\/" ((proj1 y),S))} is non empty set
{{("\/" ((proj1 y),S)),("\/" ((proj2 y),T))},{("\/" ((proj1 y),S))}} is non empty set
s9 is set
ST is M2( the carrier of S)
t is set
[ST,t] is V1() set
{ST,t} is non empty set
{ST} is non empty set
{{ST,t},{ST}} is non empty set
t1 is set
s2 is M2( the carrier of T)
t1 is set
[t1,s2] is V1() set
{t1,s2} is non empty set
{t1} is non empty set
{{t1,s2},{t1}} is non empty set
[: the carrier of S, the carrier of T:] is non empty V7() set
z is M2( the carrier of T)
[ST,z] is V1() M2( the carrier of [:S,T:])
{ST,z} is non empty set
{{ST,z},{ST}} is non empty set
x is M2( the carrier of S)
[x,s2] is V1() M2( the carrier of [:S,T:])
{x,s2} is non empty set
{x} is non empty set
{{x,s2},{x}} is non empty set
z is M2( the carrier of [:S,T:])
z is M2( the carrier of [:S,T:])
z `1 is M2( the carrier of S)
z `2 is M2( the carrier of T)
[(z `1),(z `2)] is V1() M2( the carrier of [:S,T:])
{(z `1),(z `2)} is non empty set
{(z `1)} is non empty set
{{(z `1),(z `2)},{(z `1)}} is non empty set
z is M2( the carrier of [:S,T:])
S is non empty reflexive antisymmetric up-complete non void RelStr
the carrier of S is non empty set
bool the carrier of S is non empty set
T is non empty reflexive antisymmetric up-complete non void RelStr
the carrier of T is non empty set
bool the carrier of T is non empty set
[:S,T:] is non empty strict reflexive antisymmetric up-complete non void RelStr
x is M2( bool the carrier of S)
y is M2( bool the carrier of T)
[:x,y:] is V7() M2( bool the carrier of [:S,T:])
the carrier of [:S,T:] is non empty set
bool the carrier of [:S,T:] is non empty set
y is set
{y} is non empty set
s9 is non empty directed M2( bool the carrier of T)
ST is non empty directed M2( bool the carrier of S)
"\/" (ST,S) is M2( the carrier of S)
[:ST,s9:] is non empty V7() directed M2( bool the carrier of [:S,T:])
"\/" ([:ST,s9:],[:S,T:]) is M2( the carrier of [:S,T:])
proj1 [:ST,s9:] is non empty M2( bool the carrier of S)
"\/" ((proj1 [:ST,s9:]),S) is M2( the carrier of S)
proj2 [:ST,s9:] is non empty M2( bool the carrier of T)
"\/" ((proj2 [:ST,s9:]),T) is M2( the carrier of T)
[("\/" ((proj1 [:ST,s9:]),S)),("\/" ((proj2 [:ST,s9:]),T))] is V1() M2( the carrier of [:S,T:])
{("\/" ((proj1 [:ST,s9:]),S)),("\/" ((proj2 [:ST,s9:]),T))} is non empty set
{("\/" ((proj1 [:ST,s9:]),S))} is non empty set
{{("\/" ((proj1 [:ST,s9:]),S)),("\/" ((proj2 [:ST,s9:]),T))},{("\/" ((proj1 [:ST,s9:]),S))}} is non empty set
[("\/" (ST,S)),("\/" ((proj2 [:ST,s9:]),T))] is V1() M2( the carrier of [:S,T:])
{("\/" (ST,S)),("\/" ((proj2 [:ST,s9:]),T))} is non empty set
{("\/" (ST,S))} is non empty set
{{("\/" (ST,S)),("\/" ((proj2 [:ST,s9:]),T))},{("\/" (ST,S))}} is non empty set
"\/" (s9,T) is M2( the carrier of T)
[("\/" (ST,S)),("\/" (s9,T))] is V1() M2( the carrier of [:S,T:])
{("\/" (ST,S)),("\/" (s9,T))} is non empty set
{{("\/" (ST,S)),("\/" (s9,T))},{("\/" (ST,S))}} is non empty set
[("\/" (ST,S)),y] is V1() set
{("\/" (ST,S)),y} is non empty set
{{("\/" (ST,S)),y},{("\/" (ST,S))}} is non empty set
y is set
{y} is non empty set
ST is non empty directed M2( bool the carrier of T)
"\/" (ST,T) is M2( the carrier of T)
s9 is non empty directed M2( bool the carrier of S)
[:s9,ST:] is non empty V7() directed M2( bool the carrier of [:S,T:])
"\/" ([:s9,ST:],[:S,T:]) is M2( the carrier of [:S,T:])
proj1 [:s9,ST:] is non empty M2( bool the carrier of S)
"\/" ((proj1 [:s9,ST:]),S) is M2( the carrier of S)
proj2 [:s9,ST:] is non empty M2( bool the carrier of T)
"\/" ((proj2 [:s9,ST:]),T) is M2( the carrier of T)
[("\/" ((proj1 [:s9,ST:]),S)),("\/" ((proj2 [:s9,ST:]),T))] is V1() M2( the carrier of [:S,T:])
{("\/" ((proj1 [:s9,ST:]),S)),("\/" ((proj2 [:s9,ST:]),T))} is non empty set
{("\/" ((proj1 [:s9,ST:]),S))} is non empty set
{{("\/" ((proj1 [:s9,ST:]),S)),("\/" ((proj2 [:s9,ST:]),T))},{("\/" ((proj1 [:s9,ST:]),S))}} is non empty set
"\/" (s9,S) is M2( the carrier of S)
[("\/" (s9,S)),("\/" ((proj2 [:s9,ST:]),T))] is V1() M2( the carrier of [:S,T:])
{("\/" (s9,S)),("\/" ((proj2 [:s9,ST:]),T))} is non empty set
{("\/" (s9,S))} is non empty set
{{("\/" (s9,S)),("\/" ((proj2 [:s9,ST:]),T))},{("\/" (s9,S))}} is non empty set
[("\/" (s9,S)),("\/" (ST,T))] is V1() M2( the carrier of [:S,T:])
{("\/" (s9,S)),("\/" (ST,T))} is non empty set
{{("\/" (s9,S)),("\/" (ST,T))},{("\/" (s9,S))}} is non empty set
[y,("\/" (ST,T))] is V1() set
{y,("\/" (ST,T))} is non empty set
{{y,("\/" (ST,T))},{y}} is non empty set
S is non empty reflexive antisymmetric up-complete non void RelStr
the carrier of S is non empty set
bool the carrier of S is non empty set
T is non empty reflexive antisymmetric up-complete non void RelStr
the carrier of T is non empty set
bool the carrier of T is non empty set
[:S,T:] is non empty strict reflexive antisymmetric up-complete non void RelStr
x is M2( bool the carrier of S)
y is M2( bool the carrier of T)
[:x,y:] is V7() M2( bool the carrier of [:S,T:])
the carrier of [:S,T:] is non empty set
bool the carrier of [:S,T:] is non empty set
y is non empty directed M2( bool the carrier of [:S,T:])
"\/" (y,[:S,T:]) is M2( the carrier of [:S,T:])
proj2 y is M2( bool the carrier of T)
"\/" ((proj2 y),T) is M2( the carrier of T)
proj1 y is M2( bool the carrier of S)
"\/" ((proj1 y),S) is M2( the carrier of S)
[("\/" ((proj1 y),S)),("\/" ((proj2 y),T))] is V1() M2( the carrier of [:S,T:])
{("\/" ((proj1 y),S)),("\/" ((proj2 y),T))} is non empty set
{("\/" ((proj1 y),S))} is non empty set
{{("\/" ((proj1 y),S)),("\/" ((proj2 y),T))},{("\/" ((proj1 y),S))}} is non empty set
S is non empty reflexive antisymmetric up-complete non void RelStr
T is non empty reflexive antisymmetric up-complete non void RelStr
[:S,T:] is non empty strict reflexive antisymmetric up-complete non void RelStr
the carrier of [:S,T:] is non empty set
bool the carrier of [:S,T:] is non empty set
x is M2( bool the carrier of [:S,T:])
proj1 x is M2( bool the carrier of S)
the carrier of S is non empty set
bool the carrier of S is non empty set
proj2 x is M2( bool the carrier of T)
the carrier of T is non empty set
bool the carrier of T is non empty set
[: the carrier of S, the carrier of T:] is non empty V7() set
y is non empty directed M2( bool the carrier of S)
"\/" (y,S) is M2( the carrier of S)
y is set
[("\/" (y,S)),y] is V1() set
{("\/" (y,S)),y} is non empty set
{("\/" (y,S))} is non empty set
{{("\/" (y,S)),y},{("\/" (y,S))}} is non empty set
s9 is M2( the carrier of T)
{s9} is non empty M2( bool the carrier of T)
ST is non empty directed M2( bool the carrier of T)
[:y,ST:] is non empty V7() directed M2( bool the carrier of [:S,T:])
"\/" ([:y,ST:],[:S,T:]) is M2( the carrier of [:S,T:])
proj1 [:y,ST:] is non empty M2( bool the carrier of S)
"\/" ((proj1 [:y,ST:]),S) is M2( the carrier of S)
proj2 [:y,ST:] is non empty M2( bool the carrier of T)
"\/" ((proj2 [:y,ST:]),T) is M2( the carrier of T)
[("\/" ((proj1 [:y,ST:]),S)),("\/" ((proj2 [:y,ST:]),T))] is V1() M2( the carrier of [:S,T:])
{("\/" ((proj1 [:y,ST:]),S)),("\/" ((proj2 [:y,ST:]),T))} is non empty set
{("\/" ((proj1 [:y,ST:]),S))} is non empty set
{{("\/" ((proj1 [:y,ST:]),S)),("\/" ((proj2 [:y,ST:]),T))},{("\/" ((proj1 [:y,ST:]),S))}} is non empty set
[("\/" (y,S)),("\/" ((proj2 [:y,ST:]),T))] is V1() M2( the carrier of [:S,T:])
{("\/" (y,S)),("\/" ((proj2 [:y,ST:]),T))} is non empty set
{{("\/" (y,S)),("\/" ((proj2 [:y,ST:]),T))},{("\/" (y,S))}} is non empty set
"\/" (ST,T) is M2( the carrier of T)
[("\/" (y,S)),("\/" (ST,T))] is V1() M2( the carrier of [:S,T:])
{("\/" (y,S)),("\/" (ST,T))} is non empty set
{{("\/" (y,S)),("\/" (ST,T))},{("\/" (y,S))}} is non empty set
[("\/" (y,S)),s9] is V1() M2( the carrier of [:S,T:])
{("\/" (y,S)),s9} is non empty set
{{("\/" (y,S)),s9},{("\/" (y,S))}} is non empty set
t is M2( the carrier of [:S,T:])
t `1 is M2( the carrier of S)
t `2 is M2( the carrier of T)
[(t `1),(t `2)] is V1() M2( the carrier of [:S,T:])
{(t `1),(t `2)} is non empty set
{(t `1)} is non empty set
{{(t `1),(t `2)},{(t `1)}} is non empty set
t1 is M2( the carrier of S)
s2 is M2( the carrier of S)
[s2,s9] is V1() M2( the carrier of [:S,T:])
{s2,s9} is non empty set
{s2} is non empty set
{{s2,s9},{s2}} is non empty set
y is non empty directed M2( bool the carrier of T)
"\/" (y,T) is M2( the carrier of T)
y is set
[y,("\/" (y,T))] is V1() set
{y,("\/" (y,T))} is non empty set
{y} is non empty set
{{y,("\/" (y,T))},{y}} is non empty set
s9 is M2( the carrier of S)
{s9} is non empty M2( bool the carrier of S)
ST is non empty directed M2( bool the carrier of S)
[:ST,y:] is non empty V7() directed M2( bool the carrier of [:S,T:])
"\/" ([:ST,y:],[:S,T:]) is M2( the carrier of [:S,T:])
proj1 [:ST,y:] is non empty M2( bool the carrier of S)
"\/" ((proj1 [:ST,y:]),S) is M2( the carrier of S)
proj2 [:ST,y:] is non empty M2( bool the carrier of T)
"\/" ((proj2 [:ST,y:]),T) is M2( the carrier of T)
[("\/" ((proj1 [:ST,y:]),S)),("\/" ((proj2 [:ST,y:]),T))] is V1() M2( the carrier of [:S,T:])
{("\/" ((proj1 [:ST,y:]),S)),("\/" ((proj2 [:ST,y:]),T))} is non empty set
{("\/" ((proj1 [:ST,y:]),S))} is non empty set
{{("\/" ((proj1 [:ST,y:]),S)),("\/" ((proj2 [:ST,y:]),T))},{("\/" ((proj1 [:ST,y:]),S))}} is non empty set
"\/" (ST,S) is M2( the carrier of S)
[("\/" (ST,S)),("\/" ((proj2 [:ST,y:]),T))] is V1() M2( the carrier of [:S,T:])
{("\/" (ST,S)),("\/" ((proj2 [:ST,y:]),T))} is non empty set
{("\/" (ST,S))} is non empty set
{{("\/" (ST,S)),("\/" ((proj2 [:ST,y:]),T))},{("\/" (ST,S))}} is non empty set
[("\/" (ST,S)),("\/" (y,T))] is V1() M2( the carrier of [:S,T:])
{("\/" (ST,S)),("\/" (y,T))} is non empty set
{{("\/" (ST,S)),("\/" (y,T))},{("\/" (ST,S))}} is non empty set
[s9,("\/" (y,T))] is V1() M2( the carrier of [:S,T:])
{s9,("\/" (y,T))} is non empty set
{s9} is non empty set
{{s9,("\/" (y,T))},{s9}} is non empty set
t is M2( the carrier of [:S,T:])
t `2 is M2( the carrier of T)
t1 is M2( the carrier of T)
t `1 is M2( the carrier of S)
[(t `1),(t `2)] is V1() M2( the carrier of [:S,T:])
{(t `1),(t `2)} is non empty set
{(t `1)} is non empty set
{{(t `1),(t `2)},{(t `1)}} is non empty set
s2 is M2( the carrier of T)
[s9,s2] is V1() M2( the carrier of [:S,T:])
{s9,s2} is non empty set
{{s9,s2},{s9}} is non empty set
S is non empty reflexive transitive antisymmetric up-complete non void RelStr
the carrier of S is non empty set
bool the carrier of S is non empty set
T is non empty reflexive transitive antisymmetric up-complete non void RelStr
the carrier of T is non empty set
bool the carrier of T is non empty set
[:S,T:] is non empty strict reflexive transitive antisymmetric up-complete non void RelStr
x is M2( bool the carrier of S)
y is M2( bool the carrier of T)
[:x,y:] is V7() M2( bool the carrier of [:S,T:])
the carrier of [:S,T:] is non empty set
bool the carrier of [:S,T:] is non empty set
y is non empty directed M2( bool the carrier of [:S,T:])
"\/" (y,[:S,T:]) is M2( the carrier of [:S,T:])
proj1 y is M2( bool the carrier of S)
"\/" ((proj1 y),S) is M2( the carrier of S)
proj2 y is M2( bool the carrier of T)
"\/" ((proj2 y),T) is M2( the carrier of T)
[("\/" ((proj1 y),S)),("\/" ((proj2 y),T))] is V1() M2( the carrier of [:S,T:])
{("\/" ((proj1 y),S)),("\/" ((proj2 y),T))} is non empty set
{("\/" ((proj1 y),S))} is non empty set
{{("\/" ((proj1 y),S)),("\/" ((proj2 y),T))},{("\/" ((proj1 y),S))}} is non empty set
s9 is M2( the carrier of S)
ST is set
[s9,ST] is V1() set
{s9,ST} is non empty set
{s9} is non empty set
{{s9,ST},{s9}} is non empty set
t is M2( the carrier of T)
t1 is set
[t1,t] is V1() set
{t1,t} is non empty set
{t1} is non empty set
{{t1,t},{t1}} is non empty set
[: the carrier of S, the carrier of T:] is non empty V7() set
s2 is M2( the carrier of T)
[s9,s2] is V1() M2( the carrier of [:S,T:])
{s9,s2} is non empty set
{{s9,s2},{s9}} is non empty set
t1 is M2( the carrier of S)
[t1,t] is V1() M2( the carrier of [:S,T:])
{t1,t} is non empty set
{t1} is non empty set
{{t1,t},{t1}} is non empty set
z is M2( the carrier of [:S,T:])
z `1 is M2( the carrier of S)
z `2 is M2( the carrier of T)
[(z `1),(z `2)] is V1() M2( the carrier of [:S,T:])
{(z `1),(z `2)} is non empty set
{(z `1)} is non empty set
{{(z `1),(z `2)},{(z `1)}} is non empty set
x is M2( the carrier of [:S,T:])
x `2 is M2( the carrier of T)
x `1 is M2( the carrier of S)
[(x `1),(x `2)] is V1() M2( the carrier of [:S,T:])
{(x `1),(x `2)} is non empty set
{(x `1)} is non empty set
{{(x `1),(x `2)},{(x `1)}} is non empty set
S is non empty reflexive non void RelStr
the carrier of S is non empty set
the InternalRel of S is non empty V7() M2( bool [: the carrier of S, the carrier of S:])
[: the carrier of S, the carrier of S:] is non empty V7() set
bool [: the carrier of S, the carrier of S:] is non empty set
RelStr(# the carrier of S, the InternalRel of S #) is non empty strict reflexive non void RelStr
T is non empty reflexive non void RelStr
the carrier of T is non empty set
the InternalRel of T is non empty V7() M2( bool [: the carrier of T, the carrier of T:])
[: the carrier of T, the carrier of T:] is non empty V7() set
bool [: the carrier of T, the carrier of T:] is non empty set
RelStr(# the carrier of T, the InternalRel of T #) is non empty strict reflexive non void RelStr
bool the carrier of S is non empty set
bool the carrier of T is non empty set
x is non empty M2( bool the carrier of T)
y is M2( the carrier of S)
y is M2( the carrier of T)
s9 is M2( the carrier of T)
ST is M2( the carrier of S)
S is non empty reflexive lower-bounded /\-complete non void RelStr
the carrier of S is non empty set
the InternalRel of S is non empty V7() M2( bool [: the carrier of S, the carrier of S:])
[: the carrier of S, the carrier of S:] is non empty V7() set
bool [: the carrier of S, the carrier of S:] is non empty set
RelStr(# the carrier of S, the InternalRel of S #) is non empty strict reflexive non void RelStr
S is non empty reflexive lower-bounded /\-complete non void RelStr
T is non empty reflexive lower-bounded /\-complete non void RelStr
[:S,T:] is non empty strict reflexive lower-bounded non void RelStr
the carrier of [:S,T:] is non empty set
bool the carrier of [:S,T:] is non empty set
x is non empty M2( bool the carrier of [:S,T:])
proj1 x is M2( bool the carrier of S)
the carrier of S is non empty set
bool the carrier of S is non empty set
y is M2( the carrier of S)
proj2 x is M2( bool the carrier of T)
the carrier of T is non empty set
bool the carrier of T is non empty set
y is M2( the carrier of T)
[y,y] is V1() M2( the carrier of [:S,T:])
{y,y} is non empty set
{y} is non empty set
{{y,y},{y}} is non empty set
s9 is M2( the carrier of [:S,T:])
[: the carrier of S, the carrier of T:] is non empty V7() set
s9 `1 is M2( the carrier of S)
s9 `2 is M2( the carrier of T)
[(s9 `1),(s9 `2)] is V1() M2( the carrier of [:S,T:])
{(s9 `1),(s9 `2)} is non empty set
{(s9 `1)} is non empty set
{{(s9 `1),(s9 `2)},{(s9 `1)}} is non empty set
S is non empty reflexive non void RelStr
T is non empty reflexive non void RelStr
[:S,T:] is non empty strict reflexive non void RelStr
the carrier of [:S,T:] is non empty set
bool the carrier of [:S,T:] is non empty set
the carrier of S is non empty set
the carrier of T is non empty set
[: the carrier of S, the carrier of T:] is non empty V7() set
the M2( the carrier of T) is M2( the carrier of T)
bool the carrier of S is non empty set
y is non empty M2( bool the carrier of S)
{ the M2( the carrier of T)} is non empty M2( bool the carrier of T)
bool the carrier of T is non empty set
[:y,{ the M2( the carrier of T)}:] is non empty V7() M2( bool the carrier of [:S,T:])
y is M2( the carrier of [:S,T:])
y `1 is M2( the carrier of S)
y `2 is M2( the carrier of T)
[(y `1),(y `2)] is V1() M2( the carrier of [:S,T:])
{(y `1),(y `2)} is non empty set
{(y `1)} is non empty set
{{(y `1),(y `2)},{(y `1)}} is non empty set
s9 is M2( the carrier of S)
[s9, the M2( the carrier of T)] is V1() M2( the carrier of [:S,T:])
{s9, the M2( the carrier of T)} is non empty set
{s9} is non empty set
{{s9, the M2( the carrier of T)},{s9}} is non empty set
the M2( the carrier of S) is M2( the carrier of S)
bool the carrier of T is non empty set
y is non empty M2( bool the carrier of T)
{ the M2( the carrier of S)} is non empty M2( bool the carrier of S)
bool the carrier of S is non empty set
[:{ the M2( the carrier of S)},y:] is non empty V7() M2( bool the carrier of [:S,T:])
y is M2( the carrier of [:S,T:])
y `2 is M2( the carrier of T)
y `1 is M2( the carrier of S)
[(y `1),(y `2)] is V1() M2( the carrier of [:S,T:])
{(y `1),(y `2)} is non empty set
{(y `1)} is non empty set
{{(y `1),(y `2)},{(y `1)}} is non empty set
s9 is M2( the carrier of T)
[ the M2( the carrier of S),s9] is V1() M2( the carrier of [:S,T:])
{ the M2( the carrier of S),s9} is non empty set
{ the M2( the carrier of S)} is non empty set
{{ the M2( the carrier of S),s9},{ the M2( the carrier of S)}} is non empty set
S is non empty antisymmetric lower-bounded upper-bounded bounded complemented with_suprema with_infima RelStr
T is non empty antisymmetric lower-bounded upper-bounded bounded complemented with_suprema with_infima RelStr
[:S,T:] is non empty strict antisymmetric lower-bounded upper-bounded bounded with_suprema with_infima RelStr
the carrier of [:S,T:] is non empty set
x is M2( the carrier of [:S,T:])
the carrier of S is non empty set
x `1 is M2( the carrier of S)
y is M2( the carrier of S)
the carrier of T is non empty set
x `2 is M2( the carrier of T)
y is M2( the carrier of T)
[y,y] is V1() M2( the carrier of [:S,T:])
{y,y} is non empty set
{y} is non empty set
{{y,y},{y}} is non empty set
[y,y] `1 is M2( the carrier of S)
[y,y] `2 is M2( the carrier of T)
S is non empty antisymmetric lower-bounded upper-bounded bounded with_suprema with_infima RelStr
T is non empty antisymmetric lower-bounded upper-bounded bounded with_suprema with_infima RelStr
[:S,T:] is non empty strict antisymmetric lower-bounded upper-bounded bounded with_suprema with_infima RelStr
the carrier of S is non empty set
the M2( the carrier of S) is M2( the carrier of S)
the carrier of [:S,T:] is non empty set
the carrier of T is non empty set
the M2( the carrier of T) is M2( the carrier of T)
y is M2( the carrier of S)
[y, the M2( the carrier of T)] is V1() M2( the carrier of [:S,T:])
{y, the M2( the carrier of T)} is non empty set
{y} is non empty set
{{y, the M2( the carrier of T)},{y}} is non empty set
s9 is M2( the carrier of [:S,T:])
s9 `1 is M2( the carrier of S)
[y, the M2( the carrier of T)] `1 is M2( the carrier of S)
the carrier of T is non empty set
y is M2( the carrier of T)
[ the M2( the carrier of S),y] is V1() M2( the carrier of [:S,T:])
{ the M2( the carrier of S),y} is non empty set
{ the M2( the carrier of S)} is non empty set
{{ the M2( the carrier of S),y},{ the M2( the carrier of S)}} is non empty set
y is M2( the carrier of [:S,T:])
y `2 is M2( the carrier of T)
[ the M2( the carrier of S),y] `2 is M2( the carrier of T)
S is non empty antisymmetric distributive with_suprema with_infima RelStr
T is non empty antisymmetric distributive with_suprema with_infima RelStr
[:S,T:] is non empty strict antisymmetric with_suprema with_infima RelStr
the carrier of [:S,T:] is non empty set
x is M2( the carrier of [:S,T:])
y is M2( the carrier of [:S,T:])
y is M2( the carrier of [:S,T:])
y "\/" y is M2( the carrier of [:S,T:])
x "/\" (y "\/" y) is M2( the carrier of [:S,T:])
x "/\" y is M2( the carrier of [:S,T:])
x "/\" y is M2( the carrier of [:S,T:])
(x "/\" y) "\/" (x "/\" y) is M2( the carrier of [:S,T:])
the carrier of S is non empty set
the carrier of T is non empty set
[: the carrier of S, the carrier of T:] is non empty V7() set
y "\/" y is M2( the carrier of [:S,T:])
x "/\" (y "\/" y) is M2( the carrier of [:S,T:])
(x "/\" (y "\/" y)) `2 is M2( the carrier of T)
x `2 is M2( the carrier of T)
(y "\/" y) `2 is M2( the carrier of T)
(x `2) "/\" ((y "\/" y) `2) is M2( the carrier of T)
y `2 is M2( the carrier of T)
y `2 is M2( the carrier of T)
(y `2) "\/" (y `2) is M2( the carrier of T)
(x `2) "/\" ((y `2) "\/" (y `2)) is M2( the carrier of T)
(x `2) "/\" (y `2) is M2( the carrier of T)
(x `2) "/\" (y `2) is M2( the carrier of T)
((x `2) "/\" (y `2)) "\/" ((x `2) "/\" (y `2)) is M2( the carrier of T)
x "/\" y is M2( the carrier of [:S,T:])
(x "/\" y) `2 is M2( the carrier of T)
((x "/\" y) `2) "\/" ((x `2) "/\" (y `2)) is M2( the carrier of T)
x "/\" y is M2( the carrier of [:S,T:])
(x "/\" y) `2 is M2( the carrier of T)
((x "/\" y) `2) "\/" ((x "/\" y) `2) is M2( the carrier of T)
(x "/\" y) "\/" (x "/\" y) is M2( the carrier of [:S,T:])
((x "/\" y) "\/" (x "/\" y)) `2 is M2( the carrier of T)
(x "/\" (y "\/" y)) `1 is M2( the carrier of S)
x `1 is M2( the carrier of S)
(y "\/" y) `1 is M2( the carrier of S)
(x `1) "/\" ((y "\/" y) `1) is M2( the carrier of S)
y `1 is M2( the carrier of S)
y `1 is M2( the carrier of S)
(y `1) "\/" (y `1) is M2( the carrier of S)
(x `1) "/\" ((y `1) "\/" (y `1)) is M2( the carrier of S)
(x `1) "/\" (y `1) is M2( the carrier of S)
(x `1) "/\" (y `1) is M2( the carrier of S)
((x `1) "/\" (y `1)) "\/" ((x `1) "/\" (y `1)) is M2( the carrier of S)
(x "/\" y) `1 is M2( the carrier of S)
((x "/\" y) `1) "\/" ((x `1) "/\" (y `1)) is M2( the carrier of S)
(x "/\" y) `1 is M2( the carrier of S)
((x "/\" y) `1) "\/" ((x "/\" y) `1) is M2( the carrier of S)
((x "/\" y) "\/" (x "/\" y)) `1 is M2( the carrier of S)
S is non empty antisymmetric with_suprema with_infima RelStr
T is non empty reflexive antisymmetric with_suprema with_infima non void RelStr
[:S,T:] is non empty strict antisymmetric with_suprema with_infima RelStr
the carrier of [:S,T:] is non empty set
the carrier of T is non empty set
the M2( the carrier of T) is M2( the carrier of T)
the carrier of S is non empty set
y is M2( the carrier of S)
y is M2( the carrier of S)
s9 is M2( the carrier of S)
y "\/" s9 is M2( the carrier of S)
y "/\" (y "\/" s9) is M2( the carrier of S)
y "/\" y is M2( the carrier of S)
y "/\" s9 is M2( the carrier of S)
(y "/\" y) "\/" (y "/\" s9) is M2( the carrier of S)
the M2( the carrier of T) "/\" the M2( the carrier of T) is M2( the carrier of T)
the M2( the carrier of T) "\/" the M2( the carrier of T) is M2( the carrier of T)
y "\/" s9 is M2( the carrier of S)
y "/\" (y "\/" s9) is M2( the carrier of S)
[(y "/\" (y "\/" s9)), the M2( the carrier of T)] is V1() M2( the carrier of [:S,T:])
{(y "/\" (y "\/" s9)), the M2( the carrier of T)} is non empty set
{(y "/\" (y "\/" s9))} is non empty set
{{(y "/\" (y "\/" s9)), the M2( the carrier of T)},{(y "/\" (y "\/" s9))}} is non empty set
[(y "/\" (y "\/" s9)), the M2( the carrier of T)] `1 is M2( the carrier of S)
[y, the M2( the carrier of T)] is V1() M2( the carrier of [:S,T:])
{y, the M2( the carrier of T)} is non empty set
{y} is non empty set
{{y, the M2( the carrier of T)},{y}} is non empty set
[(y "\/" s9), the M2( the carrier of T)] is V1() M2( the carrier of [:S,T:])
{(y "\/" s9), the M2( the carrier of T)} is non empty set
{(y "\/" s9)} is non empty set
{{(y "\/" s9), the M2( the carrier of T)},{(y "\/" s9)}} is non empty set
[y, the M2( the carrier of T)] "/\" [(y "\/" s9), the M2( the carrier of T)] is M2( the carrier of [:S,T:])
([y, the M2( the carrier of T)] "/\" [(y "\/" s9), the M2( the carrier of T)]) `1 is M2( the carrier of S)
[y, the M2( the carrier of T)] is V1() M2( the carrier of [:S,T:])
{y, the M2( the carrier of T)} is non empty set
{y} is non empty set
{{y, the M2( the carrier of T)},{y}} is non empty set
[s9, the M2( the carrier of T)] is V1() M2( the carrier of [:S,T:])
{s9, the M2( the carrier of T)} is non empty set
{s9} is non empty set
{{s9, the M2( the carrier of T)},{s9}} is non empty set
[y, the M2( the carrier of T)] "\/" [s9, the M2( the carrier of T)] is M2( the carrier of [:S,T:])
[y, the M2( the carrier of T)] "/\" ([y, the M2( the carrier of T)] "\/" [s9, the M2( the carrier of T)]) is M2( the carrier of [:S,T:])
([y, the M2( the carrier of T)] "/\" ([y, the M2( the carrier of T)] "\/" [s9, the M2( the carrier of T)])) `1 is M2( the carrier of S)
[y, the M2( the carrier of T)] "/\" [y, the M2( the carrier of T)] is M2( the carrier of [:S,T:])
[y, the M2( the carrier of T)] "/\" [s9, the M2( the carrier of T)] is M2( the carrier of [:S,T:])
([y, the M2( the carrier of T)] "/\" [y, the M2( the carrier of T)]) "\/" ([y, the M2( the carrier of T)] "/\" [s9, the M2( the carrier of T)]) is M2( the carrier of [:S,T:])
(([y, the M2( the carrier of T)] "/\" [y, the M2( the carrier of T)]) "\/" ([y, the M2( the carrier of T)] "/\" [s9, the M2( the carrier of T)])) `1 is M2( the carrier of S)
y "/\" y is M2( the carrier of S)
[(y "/\" y), the M2( the carrier of T)] is V1() M2( the carrier of [:S,T:])
{(y "/\" y), the M2( the carrier of T)} is non empty set
{(y "/\" y)} is non empty set
{{(y "/\" y), the M2( the carrier of T)},{(y "/\" y)}} is non empty set
[(y "/\" y), the M2( the carrier of T)] "\/" ([y, the M2( the carrier of T)] "/\" [s9, the M2( the carrier of T)]) is M2( the carrier of [:S,T:])
([(y "/\" y), the M2( the carrier of T)] "\/" ([y, the M2( the carrier of T)] "/\" [s9, the M2( the carrier of T)])) `1 is M2( the carrier of S)
y "/\" s9 is M2( the carrier of S)
[(y "/\" s9), the M2( the carrier of T)] is V1() M2( the carrier of [:S,T:])
{(y "/\" s9), the M2( the carrier of T)} is non empty set
{(y "/\" s9)} is non empty set
{{(y "/\" s9), the M2( the carrier of T)},{(y "/\" s9)}} is non empty set
[(y "/\" y), the M2( the carrier of T)] "\/" [(y "/\" s9), the M2( the carrier of T)] is M2( the carrier of [:S,T:])
([(y "/\" y), the M2( the carrier of T)] "\/" [(y "/\" s9), the M2( the carrier of T)]) `1 is M2( the carrier of S)
(y "/\" y) "\/" (y "/\" s9) is M2( the carrier of S)
[((y "/\" y) "\/" (y "/\" s9)), the M2( the carrier of T)] is V1() M2( the carrier of [:S,T:])
{((y "/\" y) "\/" (y "/\" s9)), the M2( the carrier of T)} is non empty set
{((y "/\" y) "\/" (y "/\" s9))} is non empty set
{{((y "/\" y) "\/" (y "/\" s9)), the M2( the carrier of T)},{((y "/\" y) "\/" (y "/\" s9))}} is non empty set
[((y "/\" y) "\/" (y "/\" s9)), the M2( the carrier of T)] `1 is M2( the carrier of S)
S is non empty reflexive antisymmetric with_suprema with_infima non void RelStr
T is non empty antisymmetric with_suprema with_infima RelStr
[:S,T:] is non empty strict antisymmetric with_suprema with_infima RelStr
the carrier of [:S,T:] is non empty set
the carrier of S is non empty set
the M2( the carrier of S) is M2( the carrier of S)
the carrier of T is non empty set
y is M2( the carrier of T)
y is M2( the carrier of T)
s9 is M2( the carrier of T)
y "\/" s9 is M2( the carrier of T)
y "/\" (y "\/" s9) is M2( the carrier of T)
y "/\" y is M2( the carrier of T)
y "/\" s9 is M2( the carrier of T)
(y "/\" y) "\/" (y "/\" s9) is M2( the carrier of T)
the M2( the carrier of S) "/\" the M2( the carrier of S) is M2( the carrier of S)
the M2( the carrier of S) "\/" the M2( the carrier of S) is M2( the carrier of S)
y "\/" s9 is M2( the carrier of T)
y "/\" (y "\/" s9) is M2( the carrier of T)
[ the M2( the carrier of S),(y "/\" (y "\/" s9))] is V1() M2( the carrier of [:S,T:])
{ the M2( the carrier of S),(y "/\" (y "\/" s9))} is non empty set
{ the M2( the carrier of S)} is non empty set
{{ the M2( the carrier of S),(y "/\" (y "\/" s9))},{ the M2( the carrier of S)}} is non empty set
[ the M2( the carrier of S),(y "/\" (y "\/" s9))] `2 is M2( the carrier of T)
[ the M2( the carrier of S),y] is V1() M2( the carrier of [:S,T:])
{ the M2( the carrier of S),y} is non empty set
{{ the M2( the carrier of S),y},{ the M2( the carrier of S)}} is non empty set
[ the M2( the carrier of S),(y "\/" s9)] is V1() M2( the carrier of [:S,T:])
{ the M2( the carrier of S),(y "\/" s9)} is non empty set
{{ the M2( the carrier of S),(y "\/" s9)},{ the M2( the carrier of S)}} is non empty set
[ the M2( the carrier of S),y] "/\" [ the M2( the carrier of S),(y "\/" s9)] is M2( the carrier of [:S,T:])
([ the M2( the carrier of S),y] "/\" [ the M2( the carrier of S),(y "\/" s9)]) `2 is M2( the carrier of T)
[ the M2( the carrier of S),y] is V1() M2( the carrier of [:S,T:])
{ the M2( the carrier of S),y} is non empty set
{{ the M2( the carrier of S),y},{ the M2( the carrier of S)}} is non empty set
[ the M2( the carrier of S),s9] is V1() M2( the carrier of [:S,T:])
{ the M2( the carrier of S),s9} is non empty set
{{ the M2( the carrier of S),s9},{ the M2( the carrier of S)}} is non empty set
[ the M2( the carrier of S),y] "\/" [ the M2( the carrier of S),s9] is M2( the carrier of [:S,T:])
[ the M2( the carrier of S),y] "/\" ([ the M2( the carrier of S),y] "\/" [ the M2( the carrier of S),s9]) is M2( the carrier of [:S,T:])
([ the M2( the carrier of S),y] "/\" ([ the M2( the carrier of S),y] "\/" [ the M2( the carrier of S),s9])) `2 is M2( the carrier of T)
[ the M2( the carrier of S),y] "/\" [ the M2( the carrier of S),y] is M2( the carrier of [:S,T:])
[ the M2( the carrier of S),y] "/\" [ the M2( the carrier of S),s9] is M2( the carrier of [:S,T:])
([ the M2( the carrier of S),y] "/\" [ the M2( the carrier of S),y]) "\/" ([ the M2( the carrier of S),y] "/\" [ the M2( the carrier of S),s9]) is M2( the carrier of [:S,T:])
(([ the M2( the carrier of S),y] "/\" [ the M2( the carrier of S),y]) "\/" ([ the M2( the carrier of S),y] "/\" [ the M2( the carrier of S),s9])) `2 is M2( the carrier of T)
y "/\" y is M2( the carrier of T)
[ the M2( the carrier of S),(y "/\" y)] is V1() M2( the carrier of [:S,T:])
{ the M2( the carrier of S),(y "/\" y)} is non empty set
{{ the M2( the carrier of S),(y "/\" y)},{ the M2( the carrier of S)}} is non empty set
[ the M2( the carrier of S),(y "/\" y)] "\/" ([ the M2( the carrier of S),y] "/\" [ the M2( the carrier of S),s9]) is M2( the carrier of [:S,T:])
([ the M2( the carrier of S),(y "/\" y)] "\/" ([ the M2( the carrier of S),y] "/\" [ the M2( the carrier of S),s9])) `2 is M2( the carrier of T)
y "/\" s9 is M2( the carrier of T)
[ the M2( the carrier of S),(y "/\" s9)] is V1() M2( the carrier of [:S,T:])
{ the M2( the carrier of S),(y "/\" s9)} is non empty set
{{ the M2( the carrier of S),(y "/\" s9)},{ the M2( the carrier of S)}} is non empty set
[ the M2( the carrier of S),(y "/\" y)] "\/" [ the M2( the carrier of S),(y "/\" s9)] is M2( the carrier of [:S,T:])
([ the M2( the carrier of S),(y "/\" y)] "\/" [ the M2( the carrier of S),(y "/\" s9)]) `2 is M2( the carrier of T)
(y "/\" y) "\/" (y "/\" s9) is M2( the carrier of T)
[ the M2( the carrier of S),((y "/\" y) "\/" (y "/\" s9))] is V1() M2( the carrier of [:S,T:])
{ the M2( the carrier of S),((y "/\" y) "\/" (y "/\" s9))} is non empty set
{{ the M2( the carrier of S),((y "/\" y) "\/" (y "/\" s9))},{ the M2( the carrier of S)}} is non empty set
[ the M2( the carrier of S),((y "/\" y) "\/" (y "/\" s9))] `2 is M2( the carrier of T)
S is non empty reflexive transitive antisymmetric up-complete with_infima non void satisfying_MC meet-continuous RelStr
T is non empty reflexive transitive antisymmetric up-complete with_infima non void satisfying_MC meet-continuous RelStr
[:S,T:] is non empty strict reflexive transitive antisymmetric up-complete with_infima non void RelStr
the carrier of [:S,T:] is non empty set
bool the carrier of [:S,T:] is non empty set
x is M2( the carrier of [:S,T:])
{x} is non empty M2( bool the carrier of [:S,T:])
y is non empty directed M2( bool the carrier of [:S,T:])
"\/" (y,[:S,T:]) is M2( the carrier of [:S,T:])
x "/\" ("\/" (y,[:S,T:])) is M2( the carrier of [:S,T:])
{x} "/\" y is non empty M2( bool the carrier of [:S,T:])
"\/" (({x} "/\" y),[:S,T:]) is M2( the carrier of [:S,T:])
proj1 y is M2( bool the carrier of S)
the carrier of S is non empty set
bool the carrier of S is non empty set
proj2 y is M2( bool the carrier of T)
the carrier of T is non empty set
bool the carrier of T is non empty set
[: the carrier of S, the carrier of T:] is non empty V7() set
x `1 is M2( the carrier of S)
x `2 is M2( the carrier of T)
[(x `1),(x `2)] is V1() M2( the carrier of [:S,T:])
{(x `1),(x `2)} is non empty set
{(x `1)} is non empty set
{{(x `1),(x `2)},{(x `1)}} is non empty set
y is non empty directed M2( bool the carrier of [:S,T:])
y "/\" y is non empty directed M2( bool the carrier of [:S,T:])
{x} "/\" y is non empty M2( bool the carrier of [:S,T:])
"\/" (({x} "/\" y),[:S,T:]) is M2( the carrier of [:S,T:])
proj1 ({x} "/\" y) is M2( bool the carrier of S)
"\/" ((proj1 ({x} "/\" y)),S) is M2( the carrier of S)
proj2 ({x} "/\" y) is M2( bool the carrier of T)
"\/" ((proj2 ({x} "/\" y)),T) is M2( the carrier of T)
[("\/" ((proj1 ({x} "/\" y)),S)),("\/" ((proj2 ({x} "/\" y)),T))] is V1() M2( the carrier of [:S,T:])
{("\/" ((proj1 ({x} "/\" y)),S)),("\/" ((proj2 ({x} "/\" y)),T))} is non empty set
{("\/" ((proj1 ({x} "/\" y)),S))} is non empty set
{{("\/" ((proj1 ({x} "/\" y)),S)),("\/" ((proj2 ({x} "/\" y)),T))},{("\/" ((proj1 ({x} "/\" y)),S))}} is non empty set
"\/" ((proj1 y),S) is M2( the carrier of S)
"\/" ((proj2 y),T) is M2( the carrier of T)
[("\/" ((proj1 y),S)),("\/" ((proj2 y),T))] is V1() M2( the carrier of [:S,T:])
{("\/" ((proj1 y),S)),("\/" ((proj2 y),T))} is non empty set
{("\/" ((proj1 y),S))} is non empty set
{{("\/" ((proj1 y),S)),("\/" ((proj2 y),T))},{("\/" ((proj1 y),S))}} is non empty set
x "/\" ("\/" (y,[:S,T:])) is M2( the carrier of [:S,T:])
(x "/\" ("\/" (y,[:S,T:]))) `2 is M2( the carrier of T)
("\/" (y,[:S,T:])) `2 is M2( the carrier of T)
(x `2) "/\" (("\/" (y,[:S,T:])) `2) is M2( the carrier of T)
(x `2) "/\" ("\/" ((proj2 y),T)) is M2( the carrier of T)
{(x `2)} is non empty M2( bool the carrier of T)
{(x `2)} "/\" (proj2 y) is M2( bool the carrier of T)
"\/" (({(x `2)} "/\" (proj2 y)),T) is M2( the carrier of T)
proj2 {x} is M2( bool the carrier of T)
(proj2 {x}) "/\" (proj2 y) is M2( bool the carrier of T)
"\/" (((proj2 {x}) "/\" (proj2 y)),T) is M2( the carrier of T)
("\/" (({x} "/\" y),[:S,T:])) `2 is M2( the carrier of T)
(x "/\" ("\/" (y,[:S,T:]))) `1 is M2( the carrier of S)
("\/" (y,[:S,T:])) `1 is M2( the carrier of S)
(x `1) "/\" (("\/" (y,[:S,T:])) `1) is M2( the carrier of S)
(x `1) "/\" ("\/" ((proj1 y),S)) is M2( the carrier of S)
{(x `1)} is non empty M2( bool the carrier of S)
{(x `1)} "/\" (proj1 y) is M2( bool the carrier of S)
"\/" (({(x `1)} "/\" (proj1 y)),S) is M2( the carrier of S)
proj1 {x} is M2( bool the carrier of S)
(proj1 {x}) "/\" (proj1 y) is M2( bool the carrier of S)
"\/" (((proj1 {x}) "/\" (proj1 y)),S) is M2( the carrier of S)
("\/" (({x} "/\" y),[:S,T:])) `1 is M2( the carrier of S)
S is non empty reflexive transitive antisymmetric with_infima non void RelStr
T is non empty reflexive transitive antisymmetric with_infima non void RelStr
[:S,T:] is non empty strict reflexive transitive antisymmetric with_infima non void RelStr
the carrier of [:S,T:] is non empty set
bool the carrier of [:S,T:] is non empty set
the carrier of T is non empty set
the M2( the carrier of T) is M2( the carrier of T)
the carrier of S is non empty set
bool the carrier of S is non empty set
bool the carrier of T is non empty set
{ the M2( the carrier of T)} is non empty M2( bool the carrier of T)
y is M2( the carrier of S)
[y, the M2( the carrier of T)] is V1() M2( the carrier of [:S,T:])
{y, the M2( the carrier of T)} is non empty set
{y} is non empty set
{{y, the M2( the carrier of T)},{y}} is non empty set
{[y, the M2( the carrier of T)]} is non empty V7() M2( bool the carrier of [:S,T:])
y is non empty directed M2( bool the carrier of S)
s9 is non empty directed M2( bool the carrier of T)
[:y,s9:] is non empty V7() directed M2( bool the carrier of [:S,T:])
"\/" ([:y,s9:],[:S,T:]) is M2( the carrier of [:S,T:])
proj1 [:y,s9:] is non empty M2( bool the carrier of S)
"\/" ((proj1 [:y,s9:]),S) is M2( the carrier of S)
proj2 [:y,s9:] is non empty M2( bool the carrier of T)
"\/" ((proj2 [:y,s9:]),T) is M2( the carrier of T)
[("\/" ((proj1 [:y,s9:]),S)),("\/" ((proj2 [:y,s9:]),T))] is V1() M2( the carrier of [:S,T:])
{("\/" ((proj1 [:y,s9:]),S)),("\/" ((proj2 [:y,s9:]),T))} is non empty set
{("\/" ((proj1 [:y,s9:]),S))} is non empty set
{{("\/" ((proj1 [:y,s9:]),S)),("\/" ((proj2 [:y,s9:]),T))},{("\/" ((proj1 [:y,s9:]),S))}} is non empty set
ST is non empty directed M2( bool the carrier of [:S,T:])
ST "/\" [:y,s9:] is non empty directed M2( bool the carrier of [:S,T:])
{[y, the M2( the carrier of T)]} "/\" [:y,s9:] is non empty M2( bool the carrier of [:S,T:])
"\/" (({[y, the M2( the carrier of T)]} "/\" [:y,s9:]),[:S,T:]) is M2( the carrier of [:S,T:])
proj1 ({[y, the M2( the carrier of T)]} "/\" [:y,s9:]) is M2( bool the carrier of S)
"\/" ((proj1 ({[y, the M2( the carrier of T)]} "/\" [:y,s9:])),S) is M2( the carrier of S)
proj2 ({[y, the M2( the carrier of T)]} "/\" [:y,s9:]) is M2( bool the carrier of T)
"\/" ((proj2 ({[y, the M2( the carrier of T)]} "/\" [:y,s9:])),T) is M2( the carrier of T)
[("\/" ((proj1 ({[y, the M2( the carrier of T)]} "/\" [:y,s9:])),S)),("\/" ((proj2 ({[y, the M2( the carrier of T)]} "/\" [:y,s9:])),T))] is V1() M2( the carrier of [:S,T:])
{("\/" ((proj1 ({[y, the M2( the carrier of T)]} "/\" [:y,s9:])),S)),("\/" ((proj2 ({[y, the M2( the carrier of T)]} "/\" [:y,s9:])),T))} is non empty set
{("\/" ((proj1 ({[y, the M2( the carrier of T)]} "/\" [:y,s9:])),S))} is non empty set
{{("\/" ((proj1 ({[y, the M2( the carrier of T)]} "/\" [:y,s9:])),S)),("\/" ((proj2 ({[y, the M2( the carrier of T)]} "/\" [:y,s9:])),T))},{("\/" ((proj1 ({[y, the M2( the carrier of T)]} "/\" [:y,s9:])),S))}} is non empty set
{y} is non empty M2( bool the carrier of S)
{y} "/\" y is non empty M2( bool the carrier of S)
"\/" (({y} "/\" y),S) is M2( the carrier of S)
proj1 {[y, the M2( the carrier of T)]} is non empty M2( bool the carrier of S)
(proj1 {[y, the M2( the carrier of T)]}) "/\" y is non empty M2( bool the carrier of S)
"\/" (((proj1 {[y, the M2( the carrier of T)]}) "/\" y),S) is M2( the carrier of S)
(proj1 {[y, the M2( the carrier of T)]}) "/\" (proj1 [:y,s9:]) is non empty M2( bool the carrier of S)
"\/" (((proj1 {[y, the M2( the carrier of T)]}) "/\" (proj1 [:y,s9:])),S) is M2( the carrier of S)
("\/" (({[y, the M2( the carrier of T)]} "/\" [:y,s9:]),[:S,T:])) `1 is M2( the carrier of S)
[y, the M2( the carrier of T)] "/\" ("\/" ([:y,s9:],[:S,T:])) is M2( the carrier of [:S,T:])
([y, the M2( the carrier of T)] "/\" ("\/" ([:y,s9:],[:S,T:]))) `1 is M2( the carrier of S)
[y, the M2( the carrier of T)] `1 is M2( the carrier of S)
("\/" ([:y,s9:],[:S,T:])) `1 is M2( the carrier of S)
([y, the M2( the carrier of T)] `1) "/\" (("\/" ([:y,s9:],[:S,T:])) `1) is M2( the carrier of S)
y "/\" (("\/" ([:y,s9:],[:S,T:])) `1) is M2( the carrier of S)
y "/\" ("\/" ((proj1 [:y,s9:]),S)) is M2( the carrier of S)
"\/" (y,S) is M2( the carrier of S)
y "/\" ("\/" (y,S)) is M2( the carrier of S)
the M2( the carrier of S) is M2( the carrier of S)
y is M2( the carrier of T)
{y} is non empty M2( bool the carrier of T)
y is non empty directed M2( bool the carrier of T)
"\/" (y,T) is M2( the carrier of T)
y "/\" ("\/" (y,T)) is M2( the carrier of T)
{y} "/\" y is non empty M2( bool the carrier of T)
"\/" (({y} "/\" y),T) is M2( the carrier of T)
{ the M2( the carrier of S)} is non empty M2( bool the carrier of S)
s9 is non empty directed M2( bool the carrier of S)
[:s9,y:] is non empty V7() directed M2( bool the carrier of [:S,T:])
"\/" ([:s9,y:],[:S,T:]) is M2( the carrier of [:S,T:])
proj1 [:s9,y:] is non empty M2( bool the carrier of S)
"\/" ((proj1 [:s9,y:]),S) is M2( the carrier of S)
proj2 [:s9,y:] is non empty M2( bool the carrier of T)
"\/" ((proj2 [:s9,y:]),T) is M2( the carrier of T)
[("\/" ((proj1 [:s9,y:]),S)),("\/" ((proj2 [:s9,y:]),T))] is V1() M2( the carrier of [:S,T:])
{("\/" ((proj1 [:s9,y:]),S)),("\/" ((proj2 [:s9,y:]),T))} is non empty set
{("\/" ((proj1 [:s9,y:]),S))} is non empty set
{{("\/" ((proj1 [:s9,y:]),S)),("\/" ((proj2 [:s9,y:]),T))},{("\/" ((proj1 [:s9,y:]),S))}} is non empty set
[ the M2( the carrier of S),y] is V1() M2( the carrier of [:S,T:])
{ the M2( the carrier of S),y} is non empty set
{ the M2( the carrier of S)} is non empty set
{{ the M2( the carrier of S),y},{ the M2( the carrier of S)}} is non empty set
{[ the M2( the carrier of S),y]} is non empty V7() M2( bool the carrier of [:S,T:])
ST is non empty directed M2( bool the carrier of [:S,T:])
ST "/\" [:s9,y:] is non empty directed M2( bool the carrier of [:S,T:])
{[ the M2( the carrier of S),y]} "/\" [:s9,y:] is non empty M2( bool the carrier of [:S,T:])
"\/" (({[ the M2( the carrier of S),y]} "/\" [:s9,y:]),[:S,T:]) is M2( the carrier of [:S,T:])
proj1 ({[ the M2( the carrier of S),y]} "/\" [:s9,y:]) is M2( bool the carrier of S)
"\/" ((proj1 ({[ the M2( the carrier of S),y]} "/\" [:s9,y:])),S) is M2( the carrier of S)
proj2 ({[ the M2( the carrier of S),y]} "/\" [:s9,y:]) is M2( bool the carrier of T)
"\/" ((proj2 ({[ the M2( the carrier of S),y]} "/\" [:s9,y:])),T) is M2( the carrier of T)
[("\/" ((proj1 ({[ the M2( the carrier of S),y]} "/\" [:s9,y:])),S)),("\/" ((proj2 ({[ the M2( the carrier of S),y]} "/\" [:s9,y:])),T))] is V1() M2( the carrier of [:S,T:])
{("\/" ((proj1 ({[ the M2( the carrier of S),y]} "/\" [:s9,y:])),S)),("\/" ((proj2 ({[ the M2( the carrier of S),y]} "/\" [:s9,y:])),T))} is non empty set
{("\/" ((proj1 ({[ the M2( the carrier of S),y]} "/\" [:s9,y:])),S))} is non empty set
{{("\/" ((proj1 ({[ the M2( the carrier of S),y]} "/\" [:s9,y:])),S)),("\/" ((proj2 ({[ the M2( the carrier of S),y]} "/\" [:s9,y:])),T))},{("\/" ((proj1 ({[ the M2( the carrier of S),y]} "/\" [:s9,y:])),S))}} is non empty set
{y} "/\" y is non empty M2( bool the carrier of T)
"\/" (({y} "/\" y),T) is M2( the carrier of T)
proj2 {[ the M2( the carrier of S),y]} is non empty M2( bool the carrier of T)
(proj2 {[ the M2( the carrier of S),y]}) "/\" y is non empty M2( bool the carrier of T)
"\/" (((proj2 {[ the M2( the carrier of S),y]}) "/\" y),T) is M2( the carrier of T)
(proj2 {[ the M2( the carrier of S),y]}) "/\" (proj2 [:s9,y:]) is non empty M2( bool the carrier of T)
"\/" (((proj2 {[ the M2( the carrier of S),y]}) "/\" (proj2 [:s9,y:])),T) is M2( the carrier of T)
("\/" (({[ the M2( the carrier of S),y]} "/\" [:s9,y:]),[:S,T:])) `2 is M2( the carrier of T)
[ the M2( the carrier of S),y] "/\" ("\/" ([:s9,y:],[:S,T:])) is M2( the carrier of [:S,T:])
([ the M2( the carrier of S),y] "/\" ("\/" ([:s9,y:],[:S,T:]))) `2 is M2( the carrier of T)
[ the M2( the carrier of S),y] `2 is M2( the carrier of T)
("\/" ([:s9,y:],[:S,T:])) `2 is M2( the carrier of T)
([ the M2( the carrier of S),y] `2) "/\" (("\/" ([:s9,y:],[:S,T:])) `2) is M2( the carrier of T)
y "/\" (("\/" ([:s9,y:],[:S,T:])) `2) is M2( the carrier of T)
y "/\" ("\/" ((proj2 [:s9,y:]),T)) is M2( the carrier of T)
y "/\" ("\/" (y,T)) is M2( the carrier of T)
S is non empty reflexive transitive antisymmetric lower-bounded up-complete /\-complete with_infima satisfying_axiom_of_approximation non void RelStr
T is non empty reflexive transitive antisymmetric lower-bounded up-complete /\-complete with_infima satisfying_axiom_of_approximation non void RelStr
[:S,T:] is non empty strict reflexive transitive antisymmetric lower-bounded up-complete /\-complete with_infima non void RelStr
the carrier of [:S,T:] is non empty set
x is M2( the carrier of [:S,T:])
waybelow x is non empty directed lower M2( bool the carrier of [:S,T:])
bool the carrier of [:S,T:] is non empty set
{ b₁ where b₁ is M2( the carrier of [:S,T:]) : b₁ is_way_below x } is set
"\/" ((waybelow x),[:S,T:]) is M2( the carrier of [:S,T:])
the carrier of S is non empty set
the carrier of T is non empty set
[: the carrier of S, the carrier of T:] is non empty V7() set
proj1 (waybelow x) is M2( bool the carrier of S)
bool the carrier of S is non empty set
"\/" ((proj1 (waybelow x)),S) is M2( the carrier of S)
proj2 (waybelow x) is M2( bool the carrier of T)
bool the carrier of T is non empty set
"\/" ((proj2 (waybelow x)),T) is M2( the carrier of T)
[("\/" ((proj1 (waybelow x)),S)),("\/" ((proj2 (waybelow x)),T))] is V1() M2( the carrier of [:S,T:])
{("\/" ((proj1 (waybelow x)),S)),("\/" ((proj2 (waybelow x)),T))} is non empty set
{("\/" ((proj1 (waybelow x)),S))} is non empty set
{{("\/" ((proj1 (waybelow x)),S)),("\/" ((proj2 (waybelow x)),T))},{("\/" ((proj1 (waybelow x)),S))}} is non empty set
("\/" ((waybelow x),[:S,T:])) `2 is M2( the carrier of T)
x `2 is M2( the carrier of T)
waybelow (x `2) is non empty directed lower M2( bool the carrier of T)
{ b<sub>1</sub> where b<sub>1</sub> is M2( the carrier of T) : b<sub>1</sub> is_way_below x `2 } is set
"\/" ((waybelow (x `2)),T) is M2( the carrier of T)
("\/" ((waybelow x),[:S,T:])) `1 is M2( the carrier of S)
x `1 is M2( the carrier of S)
waybelow (x `1) is non empty directed lower M2( bool the carrier of S)
{ b₁ where b₁ is M2( the carrier of S) : b₁ is_way_below x `1 } is set
"\/" ((waybelow (x `1)),S) is M2( the carrier of S)
S is non empty reflexive transitive antisymmetric lower-bounded up-complete /\-complete with_infima satisfying_axiom_of_approximation continuous non void RelStr
T is non empty reflexive transitive antisymmetric lower-bounded up-complete /\-complete with_infima satisfying_axiom_of_approximation continuous non void RelStr
[:S,T:] is non empty strict reflexive transitive antisymmetric lower-bounded up-complete /\-complete with_infima satisfying_axiom_of_approximation non void RelStr
the carrier of [:S,T:] is non empty set
x is M2( the carrier of [:S,T:])
waybelow x is non empty directed lower M2( bool the carrier of [:S,T:])
bool the carrier of [:S,T:] is non empty set
{ b₁ where b₁ is M2( the carrier of [:S,T:]) : b₁ is_way_below x } is set
y is M2( the carrier of [:S,T:])
waybelow y is non empty directed lower M2( bool the carrier of [:S,T:])
{ b₁ where b₁ is M2( the carrier of [:S,T:]) : b₁ is_way_below y } is set
S is non empty reflexive transitive antisymmetric lower-bounded up-complete non void RelStr
T is non empty reflexive transitive antisymmetric lower-bounded up-complete non void RelStr
[:S,T:] is non empty strict reflexive transitive antisymmetric lower-bounded up-complete non void RelStr
the carrier of [:S,T:] is non empty set
the carrier of T is non empty set
the M2( the carrier of T) is M2( the carrier of T)
the carrier of S is non empty set
y is M2( the carrier of S)
[y, the M2( the carrier of T)] is V1() M2( the carrier of [:S,T:])
{y, the M2( the carrier of T)} is non empty set
{y} is non empty set
{{y, the M2( the carrier of T)},{y}} is non empty set
waybelow [y, the M2( the carrier of T)] is non empty lower M2( bool the carrier of [:S,T:])
bool the carrier of [:S,T:] is non empty set
{ b₁ where b₁ is M2( the carrier of [:S,T:]) : b₁ is_way_below [y, the M2( the carrier of T)] } is set
waybelow y is non empty lower M2( bool the carrier of S)
bool the carrier of S is non empty set
{ b₁ where b₁ is M2( the carrier of S) : b₁ is_way_below y } is set
waybelow the M2( the carrier of T) is non empty lower M2( bool the carrier of T)
bool the carrier of T is non empty set
{ b₁ where b₁ is M2( the carrier of T) : b₁ is_way_below the M2( the carrier of T) } is set
[:(waybelow y),(waybelow the M2( the carrier of T)):] is non empty V7() lower M2( bool the carrier of [:S,T:])
proj1 [:(waybelow y),(waybelow the M2( the carrier of T)):] is non empty M2( bool the carrier of S)
y is M2( the carrier of S)
waybelow y is non empty lower M2( bool the carrier of S)
{ b₁ where b₁ is M2( the carrier of S) : b₁ is_way_below y } is set
"\/" ((waybelow y),S) is M2( the carrier of S)
[y, the M2( the carrier of T)] is V1() M2( the carrier of [:S,T:])
{y, the M2( the carrier of T)} is non empty set
{y} is non empty set
{{y, the M2( the carrier of T)},{y}} is non empty set
waybelow [y, the M2( the carrier of T)] is non empty lower M2( bool the carrier of [:S,T:])
{ b₁ where b₁ is M2( the carrier of [:S,T:]) : b₁ is_way_below [y, the M2( the carrier of T)] } is set
"\/" ((waybelow [y, the M2( the carrier of T)]),[:S,T:]) is M2( the carrier of [:S,T:])
proj1 (waybelow [y, the M2( the carrier of T)]) is M2( bool the carrier of S)
"\/" ((proj1 (waybelow [y, the M2( the carrier of T)])),S) is M2( the carrier of S)
proj2 (waybelow [y, the M2( the carrier of T)]) is M2( bool the carrier of T)
"\/" ((proj2 (waybelow [y, the M2( the carrier of T)])),T) is M2( the carrier of T)
[("\/" ((proj1 (waybelow [y, the M2( the carrier of T)])),S)),("\/" ((proj2 (waybelow [y, the M2( the carrier of T)])),T))] is V1() M2( the carrier of [:S,T:])
{("\/" ((proj1 (waybelow [y, the M2( the carrier of T)])),S)),("\/" ((proj2 (waybelow [y, the M2( the carrier of T)])),T))} is non empty set
{("\/" ((proj1 (waybelow [y, the M2( the carrier of T)])),S))} is non empty set
{{("\/" ((proj1 (waybelow [y, the M2( the carrier of T)])),S)),("\/" ((proj2 (waybelow [y, the M2( the carrier of T)])),T))},{("\/" ((proj1 (waybelow [y, the M2( the carrier of T)])),S))}} is non empty set
[y, the M2( the carrier of T)] `1 is M2( the carrier of S)
("\/" ((waybelow [y, the M2( the carrier of T)]),[:S,T:])) `1 is M2( the carrier of S)
waybelow ([y, the M2( the carrier of T)] `1) is non empty lower M2( bool the carrier of S)
{ b<sub>1</sub> where b<sub>1</sub> is M2( the carrier of S) : b<sub>1</sub> is_way_below [y, the M2( the carrier of T)] `1 } is set
"\/" ((waybelow ([y, the M2( the carrier of T)] `1)),S) is M2( the carrier of S)
the M2( the carrier of S) is M2( the carrier of S)
y is M2( the carrier of T)
[ the M2( the carrier of S),y] is V1() M2( the carrier of [:S,T:])
{ the M2( the carrier of S),y} is non empty set
{ the M2( the carrier of S)} is non empty set
{{ the M2( the carrier of S),y},{ the M2( the carrier of S)}} is non empty set
waybelow [ the M2( the carrier of S),y] is non empty lower M2( bool the carrier of [:S,T:])
{ b<sub>1</sub> where b<sub>1</sub> is M2( the carrier of [:S,T:]) : b<sub>1</sub> is_way_below [ the M2( the carrier of S),y] } is set
waybelow the M2( the carrier of S) is non empty lower M2( bool the carrier of S)
{ b<sub>1</sub> where b<sub>1</sub> is M2( the carrier of S) : b<sub>1</sub> is_way_below the M2( the carrier of S) } is set
waybelow y is non empty lower M2( bool the carrier of T)
{ b<sub>1</sub> where b<sub>1</sub> is M2( the carrier of T) : b<sub>1</sub> is_way_below y } is set
[:(waybelow the M2( the carrier of S)),(waybelow y):] is non empty V7() lower M2( bool the carrier of [:S,T:])
proj2 [:(waybelow the M2( the carrier of S)),(waybelow y):] is non empty M2( bool the carrier of T)
y is M2( the carrier of T)
waybelow y is non empty lower M2( bool the carrier of T)
{ b<sub>1</sub> where b<sub>1</sub> is M2( the carrier of T) : b<sub>1</sub> is_way_below y } is set
"\/" ((waybelow y),T) is M2( the carrier of T)
y is M2( the carrier of [:S,T:])
waybelow y is non empty lower M2( bool the carrier of [:S,T:])
{ b<sub>1</sub> where b<sub>1</sub> is M2( the carrier of [:S,T:]) : b<sub>1</sub> is_way_below y } is set
[ the M2( the carrier of S),y] is V1() M2( the carrier of [:S,T:])
{ the M2( the carrier of S),y} is non empty set
{{ the M2( the carrier of S),y},{ the M2( the carrier of S)}} is non empty set
waybelow [ the M2( the carrier of S),y] is non empty lower M2( bool the carrier of [:S,T:])
{ b<sub>1</sub> where b<sub>1</sub> is M2( the carrier of [:S,T:]) : b<sub>1</sub> is_way_below [ the M2( the carrier of S),y] } is set
"\/" ((waybelow [ the M2( the carrier of S),y]),[:S,T:]) is M2( the carrier of [:S,T:])
proj1 (waybelow [ the M2( the carrier of S),y]) is M2( bool the carrier of S)
"\/" ((proj1 (waybelow [ the M2( the carrier of S),y])),S) is M2( the carrier of S)
proj2 (waybelow [ the M2( the carrier of S),y]) is M2( bool the carrier of T)
"\/" ((proj2 (waybelow [ the M2( the carrier of S),y])),T) is M2( the carrier of T)
[("\/" ((proj1 (waybelow [ the M2( the carrier of S),y])),S)),("\/" ((proj2 (waybelow [ the M2( the carrier of S),y])),T))] is V1() M2( the carrier of [:S,T:])
{("\/" ((proj1 (waybelow [ the M2( the carrier of S),y])),S)),("\/" ((proj2 (waybelow [ the M2( the carrier of S),y])),T))} is non empty set
{("\/" ((proj1 (waybelow [ the M2( the carrier of S),y])),S))} is non empty set
{{("\/" ((proj1 (waybelow [ the M2( the carrier of S),y])),S)),("\/" ((proj2 (waybelow [ the M2( the carrier of S),y])),T))},{("\/" ((proj1 (waybelow [ the M2( the carrier of S),y])),S))}} is non empty set
[ the M2( the carrier of S),y] `2 is M2( the carrier of T)
("\/" ((waybelow [ the M2( the carrier of S),y]),[:S,T:])) `2 is M2( the carrier of T)
waybelow ([ the M2( the carrier of S),y] `2) is non empty lower M2( bool the carrier of T)
{ b₁ where b₁ is M2( the carrier of T) : b₁ is_way_below [ the M2( the carrier of S),y] `2 } is set
"\/" ((waybelow ([ the M2( the carrier of S),y] `2)),T) is M2( the carrier of T)
S is non empty reflexive transitive antisymmetric lower-bounded upper-bounded bounded up-complete /\-complete with_suprema with_infima complete satisfying_axiom_K non void RelStr
T is non empty reflexive transitive antisymmetric lower-bounded upper-bounded bounded up-complete /\-complete with_suprema with_infima complete satisfying_axiom_K non void RelStr
[:S,T:] is non empty strict reflexive transitive antisymmetric lower-bounded upper-bounded bounded up-complete /\-complete with_suprema with_infima complete non void RelStr
the carrier of [:S,T:] is non empty set
x is M2( the carrier of [:S,T:])
compactbelow x is non empty directed M2( bool the carrier of [:S,T:])
bool the carrier of [:S,T:] is non empty set
{ b₁ where b₁ is M2( the carrier of [:S,T:]) : ( b₁ <= x & b₁ is compact ) } is set
"\/" ((compactbelow x),[:S,T:]) is M2( the carrier of [:S,T:])
the carrier of S is non empty set
the carrier of T is non empty set
[: the carrier of S, the carrier of T:] is non empty V7() set
proj1 (compactbelow x) is M2( bool the carrier of S)
bool the carrier of S is non empty set
"\/" ((proj1 (compactbelow x)),S) is M2( the carrier of S)
proj2 (compactbelow x) is M2( bool the carrier of T)
bool the carrier of T is non empty set
"\/" ((proj2 (compactbelow x)),T) is M2( the carrier of T)
[("\/" ((proj1 (compactbelow x)),S)),("\/" ((proj2 (compactbelow x)),T))] is V1() M2( the carrier of [:S,T:])
{("\/" ((proj1 (compactbelow x)),S)),("\/" ((proj2 (compactbelow x)),T))} is non empty set
{("\/" ((proj1 (compactbelow x)),S))} is non empty set
{{("\/" ((proj1 (compactbelow x)),S)),("\/" ((proj2 (compactbelow x)),T))},{("\/" ((proj1 (compactbelow x)),S))}} is non empty set
("\/" ((compactbelow x),[:S,T:])) `2 is M2( the carrier of T)
x `2 is M2( the carrier of T)
compactbelow (x `2) is non empty directed M2( bool the carrier of T)
{ b<sub>1</sub> where b<sub>1</sub> is M2( the carrier of T) : ( b<sub>1</sub> <= x `2 & b₁ is compact ) } is set
"\/" ((compactbelow (x `2)),T) is M2( the carrier of T)
("\/" ((compactbelow x),[:S,T:])) `1 is M2( the carrier of S)
x `1 is M2( the carrier of S)
compactbelow (x `1) is non empty directed M2( bool the carrier of S)
{ b₁ where b₁ is M2( the carrier of S) : ( b₁ <= x `1 & b<sub>1</sub> is compact ) } is set
"\/" ((compactbelow (x `1)),S) is M2( the carrier of S)
S is non empty reflexive transitive antisymmetric lower-bounded upper-bounded bounded up-complete /\-complete with_suprema with_infima complete satisfying_axiom_of_approximation continuous satisfying_axiom_K algebraic non void RelStr
T is non empty reflexive transitive antisymmetric lower-bounded upper-bounded bounded up-complete /\-complete with_suprema with_infima complete satisfying_axiom_of_approximation continuous satisfying_axiom_K algebraic non void RelStr
[:S,T:] is non empty strict reflexive transitive antisymmetric lower-bounded upper-bounded bounded up-complete /\-complete with_suprema with_infima complete satisfying_axiom_of_approximation continuous satisfying_axiom_K non void RelStr
the carrier of [:S,T:] is non empty set
x is M2( the carrier of [:S,T:])
compactbelow x is non empty directed M2( bool the carrier of [:S,T:])
bool the carrier of [:S,T:] is non empty set
{ b₁ where b₁ is M2( the carrier of [:S,T:]) : ( b₁ <= x & b₁ is compact ) } is set
y is M2( the carrier of [:S,T:])
compactbelow y is non empty directed M2( bool the carrier of [:S,T:])
{ b₁ where b₁ is M2( the carrier of [:S,T:]) : ( b₁ <= y & b₁ is compact ) } is set
S is non empty reflexive transitive antisymmetric lower-bounded non void RelStr
T is non empty reflexive transitive antisymmetric lower-bounded non void RelStr
[:S,T:] is non empty strict reflexive transitive antisymmetric lower-bounded non void RelStr
the carrier of [:S,T:] is non empty set
the carrier of T is non empty set
the M2( the carrier of T) is M2( the carrier of T)
the carrier of S is non empty set
y is M2( the carrier of S)
[y, the M2( the carrier of T)] is V1() M2( the carrier of [:S,T:])
{y, the M2( the carrier of T)} is non empty set
{y} is non empty set
{{y, the M2( the carrier of T)},{y}} is non empty set
compactbelow [y, the M2( the carrier of T)] is non empty M2( bool the carrier of [:S,T:])
bool the carrier of [:S,T:] is non empty set
{ b₁ where b₁ is M2( the carrier of [:S,T:]) : ( b₁ <= [y, the M2( the carrier of T)] & b₁ is compact ) } is set
compactbelow y is non empty M2( bool the carrier of S)
bool the carrier of S is non empty set
{ b₁ where b₁ is M2( the carrier of S) : ( b₁ <= y & b₁ is compact ) } is set
compactbelow the M2( the carrier of T) is non empty M2( bool the carrier of T)
bool the carrier of T is non empty set
{ b₁ where b₁ is M2( the carrier of T) : ( b₁ <= the M2( the carrier of T) & b₁ is compact ) } is set
[:(compactbelow y),(compactbelow the M2( the carrier of T)):] is non empty V7() M2( bool the carrier of [:S,T:])
proj1 [:(compactbelow y),(compactbelow the M2( the carrier of T)):] is non empty M2( bool the carrier of S)
y is M2( the carrier of S)
compactbelow y is non empty M2( bool the carrier of S)
{ b₁ where b₁ is M2( the carrier of S) : ( b₁ <= y & b₁ is compact ) } is set
"\/" ((compactbelow y),S) is M2( the carrier of S)
[y, the M2( the carrier of T)] is V1() M2( the carrier of [:S,T:])
{y, the M2( the carrier of T)} is non empty set
{y} is non empty set
{{y, the M2( the carrier of T)},{y}} is non empty set
compactbelow [y, the M2( the carrier of T)] is non empty M2( bool the carrier of [:S,T:])
{ b₁ where b₁ is M2( the carrier of [:S,T:]) : ( b₁ <= [y, the M2( the carrier of T)] & b₁ is compact ) } is set
"\/" ((compactbelow [y, the M2( the carrier of T)]),[:S,T:]) is M2( the carrier of [:S,T:])
proj1 (compactbelow [y, the M2( the carrier of T)]) is M2( bool the carrier of S)
"\/" ((proj1 (compactbelow [y, the M2( the carrier of T)])),S) is M2( the carrier of S)
proj2 (compactbelow [y, the M2( the carrier of T)]) is M2( bool the carrier of T)
"\/" ((proj2 (compactbelow [y, the M2( the carrier of T)])),T) is M2( the carrier of T)
[("\/" ((proj1 (compactbelow [y, the M2( the carrier of T)])),S)),("\/" ((proj2 (compactbelow [y, the M2( the carrier of T)])),T))] is V1() M2( the carrier of [:S,T:])
{("\/" ((proj1 (compactbelow [y, the M2( the carrier of T)])),S)),("\/" ((proj2 (compactbelow [y, the M2( the carrier of T)])),T))} is non empty set
{("\/" ((proj1 (compactbelow [y, the M2( the carrier of T)])),S))} is non empty set
{{("\/" ((proj1 (compactbelow [y, the M2( the carrier of T)])),S)),("\/" ((proj2 (compactbelow [y, the M2( the carrier of T)])),T))},{("\/" ((proj1 (compactbelow [y, the M2( the carrier of T)])),S))}} is non empty set
[y, the M2( the carrier of T)] `1 is M2( the carrier of S)
("\/" ((compactbelow [y, the M2( the carrier of T)]),[:S,T:])) `1 is M2( the carrier of S)
compactbelow ([y, the M2( the carrier of T)] `1) is non empty M2( bool the carrier of S)
{ b<sub>1</sub> where b<sub>1</sub> is M2( the carrier of S) : ( b<sub>1</sub> <= [y, the M2( the carrier of T)] `1 & b₁ is compact ) } is set
"\/" ((compactbelow ([y, the M2( the carrier of T)] `1)),S) is M2( the carrier of S)
the M2( the carrier of S) is M2( the carrier of S)
y is M2( the carrier of T)
[ the M2( the carrier of S),y] is V1() M2( the carrier of [:S,T:])
{ the M2( the carrier of S),y} is non empty set
{ the M2( the carrier of S)} is non empty set
{{ the M2( the carrier of S),y},{ the M2( the carrier of S)}} is non empty set
compactbelow [ the M2( the carrier of S),y] is non empty M2( bool the carrier of [:S,T:])
{ b<sub>1</sub> where b<sub>1</sub> is M2( the carrier of [:S,T:]) : ( b<sub>1</sub> <= [ the M2( the carrier of S),y] & b<sub>1</sub> is compact ) } is set
compactbelow the M2( the carrier of S) is non empty M2( bool the carrier of S)
{ b<sub>1</sub> where b<sub>1</sub> is M2( the carrier of S) : ( b<sub>1</sub> <= the M2( the carrier of S) & b<sub>1</sub> is compact ) } is set
compactbelow y is non empty M2( bool the carrier of T)
{ b<sub>1</sub> where b<sub>1</sub> is M2( the carrier of T) : ( b<sub>1</sub> <= y & b<sub>1</sub> is compact ) } is set
[:(compactbelow the M2( the carrier of S)),(compactbelow y):] is non empty V7() M2( bool the carrier of [:S,T:])
proj2 [:(compactbelow the M2( the carrier of S)),(compactbelow y):] is non empty M2( bool the carrier of T)
y is M2( the carrier of T)
compactbelow y is non empty M2( bool the carrier of T)
{ b<sub>1</sub> where b<sub>1</sub> is M2( the carrier of T) : ( b<sub>1</sub> <= y & b<sub>1</sub> is compact ) } is set
"\/" ((compactbelow y),T) is M2( the carrier of T)
[ the M2( the carrier of S),y] is V1() M2( the carrier of [:S,T:])
{ the M2( the carrier of S),y} is non empty set
{{ the M2( the carrier of S),y},{ the M2( the carrier of S)}} is non empty set
compactbelow [ the M2( the carrier of S),y] is non empty M2( bool the carrier of [:S,T:])
{ b<sub>1</sub> where b<sub>1</sub> is M2( the carrier of [:S,T:]) : ( b<sub>1</sub> <= [ the M2( the carrier of S),y] & b<sub>1</sub> is compact ) } is set
"\/" ((compactbelow [ the M2( the carrier of S),y]),[:S,T:]) is M2( the carrier of [:S,T:])
proj1 (compactbelow [ the M2( the carrier of S),y]) is M2( bool the carrier of S)
"\/" ((proj1 (compactbelow [ the M2( the carrier of S),y])),S) is M2( the carrier of S)
proj2 (compactbelow [ the M2( the carrier of S),y]) is M2( bool the carrier of T)
"\/" ((proj2 (compactbelow [ the M2( the carrier of S),y])),T) is M2( the carrier of T)
[("\/" ((proj1 (compactbelow [ the M2( the carrier of S),y])),S)),("\/" ((proj2 (compactbelow [ the M2( the carrier of S),y])),T))] is V1() M2( the carrier of [:S,T:])
{("\/" ((proj1 (compactbelow [ the M2( the carrier of S),y])),S)),("\/" ((proj2 (compactbelow [ the M2( the carrier of S),y])),T))} is non empty set
{("\/" ((proj1 (compactbelow [ the M2( the carrier of S),y])),S))} is non empty set
{{("\/" ((proj1 (compactbelow [ the M2( the carrier of S),y])),S)),("\/" ((proj2 (compactbelow [ the M2( the carrier of S),y])),T))},{("\/" ((proj1 (compactbelow [ the M2( the carrier of S),y])),S))}} is non empty set
[ the M2( the carrier of S),y] `2 is M2( the carrier of T)
("\/" ((compactbelow [ the M2( the carrier of S),y]),[:S,T:])) `2 is M2( the carrier of T)
compactbelow ([ the M2( the carrier of S),y] `2) is non empty M2( bool the carrier of T)
{ b₁ where b₁ is M2( the carrier of T) : ( b₁ <= [ the M2( the carrier of S),y] `2 & b<sub>1</sub> is compact ) } is set
"\/" ((compactbelow ([ the M2( the carrier of S),y] `2)),T) is M2( the carrier of T)
S is non empty reflexive transitive antisymmetric lower-bounded upper-bounded bounded up-complete /\-complete with_suprema with_infima complete satisfying_axiom_of_approximation continuous satisfying_axiom_K algebraic arithmetic non void RelStr
T is non empty reflexive transitive antisymmetric lower-bounded upper-bounded bounded up-complete /\-complete with_suprema with_infima complete satisfying_axiom_of_approximation continuous satisfying_axiom_K algebraic arithmetic non void RelStr
[:S,T:] is non empty strict reflexive transitive antisymmetric lower-bounded upper-bounded bounded up-complete /\-complete with_suprema with_infima complete satisfying_axiom_of_approximation continuous satisfying_axiom_K algebraic non void RelStr
CompactSublatt [:S,T:] is non empty strict reflexive transitive antisymmetric V71([:S,T:]) join-inheriting with_suprema non void SubRelStr of [:S,T:]
the carrier of [:S,T:] is non empty set
y is M2( the carrier of [:S,T:])
the carrier of (CompactSublatt [:S,T:]) is non empty set
y is M2( the carrier of [:S,T:])
{y,y} is non empty M2( bool the carrier of [:S,T:])
bool the carrier of [:S,T:] is non empty set
"/\" ({y,y},[:S,T:]) is M2( the carrier of [:S,T:])
y `1 is M2( the carrier of S)
the carrier of S is non empty set
CompactSublatt S is non empty strict reflexive transitive antisymmetric V71(S) join-inheriting with_suprema non void SubRelStr of S
the carrier of (CompactSublatt S) is non empty set
y `1 is M2( the carrier of S)
y `2 is M2( the carrier of T)
the carrier of T is non empty set
CompactSublatt T is non empty strict reflexive transitive antisymmetric V71(T) join-inheriting with_suprema non void SubRelStr of T
the carrier of (CompactSublatt T) is non empty set
y `2 is M2( the carrier of T)
{(y `2),(y `2)} is non empty M2( bool the carrier of T)
bool the carrier of T is non empty set
"/\" ({(y `2),(y `2)},T) is M2( the carrier of T)
(y `2) "/\" (y `2) is M2( the carrier of T)
y "/\" y is M2( the carrier of [:S,T:])
(y "/\" y) `2 is M2( the carrier of T)
{(y `1),(y `1)} is non empty M2( bool the carrier of S)
bool the carrier of S is non empty set
"/\" ({(y `1),(y `1)},S) is M2( the carrier of S)
(y `1) "/\" (y `1) is M2( the carrier of S)
(y "/\" y) `1 is M2( the carrier of S)
S is non empty reflexive transitive antisymmetric lower-bounded with_suprema with_infima non void RelStr
T is non empty reflexive transitive antisymmetric lower-bounded with_suprema with_infima non void RelStr
[:S,T:] is non empty strict reflexive transitive antisymmetric lower-bounded with_suprema with_infima non void RelStr
CompactSublatt [:S,T:] is non empty strict reflexive transitive antisymmetric V71([:S,T:]) join-inheriting with_suprema non void SubRelStr of [:S,T:]
the carrier of S is non empty set
x is M2( the carrier of S)
CompactSublatt S is non empty strict reflexive transitive antisymmetric V71(S) join-inheriting with_suprema non void SubRelStr of S
the carrier of (CompactSublatt S) is non empty set
y is M2( the carrier of S)
{x,y} is non empty M2( bool the carrier of S)
bool the carrier of S is non empty set
Bottom T is M2( the carrier of T)
the carrier of T is non empty set
"\/" ({},T) is M2( the carrier of T)
[y,(Bottom T)] is V1() M2( the carrier of [:S,T:])
the carrier of [:S,T:] is non empty set
{y,(Bottom T)} is non empty set
{y} is non empty set
{{y,(Bottom T)},{y}} is non empty set
[y,(Bottom T)] `1 is M2( the carrier of S)
[y,(Bottom T)] `2 is M2( the carrier of T)
the carrier of (CompactSublatt [:S,T:]) is non empty set
[x,(Bottom T)] is V1() M2( the carrier of [:S,T:])
{x,(Bottom T)} is non empty set
{x} is non empty set
{{x,(Bottom T)},{x}} is non empty set
[x,(Bottom T)] `1 is M2( the carrier of S)
[x,(Bottom T)] `2 is M2( the carrier of T)
{[x,(Bottom T)],[y,(Bottom T)]} is non empty V7() M2( bool the carrier of [:S,T:])
bool the carrier of [:S,T:] is non empty set
"/\" ({[x,(Bottom T)],[y,(Bottom T)]},[:S,T:]) is M2( the carrier of [:S,T:])
("/\" ({[x,(Bottom T)],[y,(Bottom T)]},[:S,T:])) `1 is M2( the carrier of S)
[x,(Bottom T)] "/\" [y,(Bottom T)] is M2( the carrier of [:S,T:])
([x,(Bottom T)] "/\" [y,(Bottom T)]) `1 is M2( the carrier of S)
([x,(Bottom T)] `1) "/\" ([y,(Bottom T)] `1) is M2( the carrier of S)
x "/\" ([y,(Bottom T)] `1) is M2( the carrier of S)
x "/\" y is M2( the carrier of S)
"/\" ({x,y},S) is M2( the carrier of S)
CompactSublatt T is non empty strict reflexive transitive antisymmetric V71(T) join-inheriting with_suprema non void SubRelStr of T
x is M2( the carrier of T)
the carrier of (CompactSublatt T) is non empty set
y is M2( the carrier of T)
{x,y} is non empty M2( bool the carrier of T)
bool the carrier of T is non empty set
"/\" ({x,y},T) is M2( the carrier of T)
Bottom S is M2( the carrier of S)
"\/" ({},S) is M2( the carrier of S)
[(Bottom S),y] is V1() M2( the carrier of [:S,T:])
{(Bottom S),y} is non empty set
{(Bottom S)} is non empty set
{{(Bottom S),y},{(Bottom S)}} is non empty set
[(Bottom S),y] `2 is M2( the carrier of T)
[(Bottom S),y] `1 is M2( the carrier of S)
[(Bottom S),x] is V1() M2( the carrier of [:S,T:])
{(Bottom S),x} is non empty set
{{(Bottom S),x},{(Bottom S)}} is non empty set
[(Bottom S),x] `2 is M2( the carrier of T)
[(Bottom S),x] `1 is M2( the carrier of S)
{[(Bottom S),x],[(Bottom S),y]} is non empty V7() M2( bool the carrier of [:S,T:])
"/\" ({[(Bottom S),x],[(Bottom S),y]},[:S,T:]) is M2( the carrier of [:S,T:])
("/\" ({[(Bottom S),x],[(Bottom S),y]},[:S,T:])) `2 is M2( the carrier of T)
[(Bottom S),x] "/\" [(Bottom S),y] is M2( the carrier of [:S,T:])
([(Bottom S),x] "/\" [(Bottom S),y]) `2 is M2( the carrier of T)
([(Bottom S),x] `2) "/\" ([(Bottom S),y] `2) is M2( the carrier of T)
x "/\" ([(Bottom S),y] `2) is M2( the carrier of T)
x "/\" y is M2( the carrier of T)