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
{ (b1 "/\" b2) where b1, b2 is M2( the carrier of [:S,T:]) : ( b1 in x & b2 in y ) } is set
{ (b1 "/\" b2) where b1, b2 is M2( the carrier of S) : ( b1 in proj1 x & b2 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
{ (b1 "/\" b2) where b1, b2 is M2( the carrier of T) : ( b1 in proj2 x & b2 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
{ (b1 "\/" b2) where b1, b2 is M2( the carrier of [:S,T:]) : ( b1 in x & b2 in y ) } is set
{ (b1 "\/" b2) where b1, b2 is M2( the carrier of S) : ( b1 in proj1 x & b2 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
{ (b1 "\/" b2) where b1, b2 is M2( the carrier of T) : ( b1 in proj2 x & b2 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