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

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

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

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

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