:: ROBBINS2 semantic presentation
begin
definition
let
L
be ( ( non
empty
) ( non
empty
)
ComplLLattStr
) ;
attr
L
is
satisfying_DN_1
means
:: ROBBINS2:def 1
for
x
,
y
,
z
,
u
being ( ( ) ( )
Element
of ( ( ) ( )
set
) ) holds
(
(
(
(
(
x
: ( ( ) ( )
Element
of ( ( ) (
V11
() )
set
) )
+
y
: ( ( ) ( )
Element
of ( ( ) (
V11
() )
set
) )
)
: ( ( ) ( )
M2
( the
U1
of
L
: ( ( ) ( )
OrthoLattStr
) : ( ( ) ( )
set
) ))
`
)
: ( ( ) ( )
M2
( the
U1
of
L
: ( ( ) ( )
OrthoLattStr
) : ( ( ) ( )
set
) ))
+
z
: ( ( ) ( )
Element
of ( ( ) (
V11
() )
set
) )
)
: ( ( ) ( )
M2
( the
U1
of
L
: ( ( ) ( )
OrthoLattStr
) : ( ( ) ( )
set
) ))
`
)
: ( ( ) ( )
M2
( the
U1
of
L
: ( ( ) ( )
OrthoLattStr
) : ( ( ) ( )
set
) ))
+
(
(
x
: ( ( ) ( )
Element
of ( ( ) (
V11
() )
set
) )
+
(
(
(
z
: ( ( ) ( )
Element
of ( ( ) (
V11
() )
set
) )
`
)
: ( ( ) ( )
M2
( the
U1
of
L
: ( ( ) ( )
OrthoLattStr
) : ( ( ) ( )
set
) ))
+
(
(
z
: ( ( ) ( )
Element
of ( ( ) (
V11
() )
set
) )
+
u
: ( ( ) ( )
Element
of ( ( ) (
V11
() )
set
) )
)
: ( ( ) ( )
M2
( the
U1
of
L
: ( ( ) ( )
OrthoLattStr
) : ( ( ) ( )
set
) ))
`
)
: ( ( ) ( )
M2
( the
U1
of
L
: ( ( ) ( )
OrthoLattStr
) : ( ( ) ( )
set
) ))
)
: ( ( ) ( )
M2
( the
U1
of
L
: ( ( ) ( )
OrthoLattStr
) : ( ( ) ( )
set
) ))
`
)
: ( ( ) ( )
M2
( the
U1
of
L
: ( ( ) ( )
OrthoLattStr
) : ( ( ) ( )
set
) ))
)
: ( ( ) ( )
M2
( the
U1
of
L
: ( ( ) ( )
OrthoLattStr
) : ( ( ) ( )
set
) ))
`
)
: ( ( ) ( )
M2
( the
U1
of
L
: ( ( ) ( )
OrthoLattStr
) : ( ( ) ( )
set
) ))
)
: ( ( ) ( )
M2
( the
U1
of
L
: ( ( ) ( )
OrthoLattStr
) : ( ( ) ( )
set
) ))
`
: ( ( ) ( )
M2
( the
U1
of
L
: ( ( ) ( )
OrthoLattStr
) : ( ( ) ( )
set
) ))
=
z
: ( ( ) ( )
Element
of ( ( ) (
V11
() )
set
) ) ;
end;
registration
cluster
TrivComplLat
: ( (
strict
) ( non
empty
V42
()
V43
()
V48
(1 : ( ( ) ( )
set
) )
join-commutative
join-associative
upper-bounded
strict
Robbins
Huntington
join-idempotent
with_idempotent_element
)
ComplLLattStr
)
->
strict
satisfying_DN_1
;
cluster
TrivOrtLat
: ( (
strict
) ( non
empty
V42
()
V43
()
V48
(1 : ( ( ) ( )
set
) )
join-commutative
join-associative
meet-commutative
meet-associative
meet-absorbing
join-absorbing
Lattice-like
distributive
modular
lower-bounded
upper-bounded
V65
()
complemented
Boolean
strict
Robbins
Huntington
join-idempotent
well-complemented
de_Morgan
)
OrthoLattStr
)
->
strict
satisfying_DN_1
;
end;
registration
cluster
non
empty
join-commutative
join-associative
satisfying_DN_1
for ( ( ) ( )
ComplLLattStr
) ;
end;
theorem
:: ROBBINS2:1
for
L
being ( ( non
empty
satisfying_DN_1
) ( non
empty
satisfying_DN_1
)
ComplLLattStr
)
for
x
,
y
,
z
,
u
,
v
being ( ( ) ( )
Element
of ( ( ) (
V11
() )
set
) ) holds
(
(
(
x
: ( ( ) ( )
Element
of ( ( ) (
V11
() )
set
) )
+
y
: ( ( ) ( )
Element
of ( ( ) (
V11
() )
set
) )
)
: ( ( ) ( )
M2
( the
U1
of
b
1
: ( ( non
empty
satisfying_DN_1
) ( non
empty
satisfying_DN_1
)
ComplLLattStr
) : ( ( ) (
V11
() )
set
) ))
`
)
: ( ( ) ( )
M2
( the
U1
of
b
1
: ( ( non
empty
satisfying_DN_1
) ( non
empty
satisfying_DN_1
)
ComplLLattStr
) : ( ( ) (
V11
() )
set
) ))
+
(
(
(
(
(
(
z
: ( ( ) ( )
Element
of ( ( ) (
V11
() )
set
) )
+
u
: ( ( ) ( )
Element
of ( ( ) (
V11
() )
set
) )
)
: ( ( ) ( )
M2
( the
U1
of
b
1
: ( ( non
empty
satisfying_DN_1
) ( non
empty
satisfying_DN_1
)
ComplLLattStr
) : ( ( ) (
V11
() )
set
) ))
`
)
: ( ( ) ( )
M2
( the
U1
of
b
1
: ( ( non
empty
satisfying_DN_1
) ( non
empty
satisfying_DN_1
)
ComplLLattStr
) : ( ( ) (
V11
() )
set
) ))
+
x
: ( ( ) ( )
Element
of ( ( ) (
V11
() )
set
) )
)
: ( ( ) ( )
M2
( the
U1
of
b
1
: ( ( non
empty
satisfying_DN_1
) ( non
empty
satisfying_DN_1
)
ComplLLattStr
) : ( ( ) (
V11
() )
set
) ))
`
)
: ( ( ) ( )
M2
( the
U1
of
b
1
: ( ( non
empty
satisfying_DN_1
) ( non
empty
satisfying_DN_1
)
ComplLLattStr
) : ( ( ) (
V11
() )
set
) ))
+
(
(
(
y
: ( ( ) ( )
Element
of ( ( ) (
V11
() )
set
) )
`
)
: ( ( ) ( )
M2
( the
U1
of
b
1
: ( ( non
empty
satisfying_DN_1
) ( non
empty
satisfying_DN_1
)
ComplLLattStr
) : ( ( ) (
V11
() )
set
) ))
+
(
(
y
: ( ( ) ( )
Element
of ( ( ) (
V11
() )
set
) )
+
v
: ( ( ) ( )
Element
of ( ( ) (
V11
() )
set
) )
)
: ( ( ) ( )
M2
( the
U1
of
b
1
: ( ( non
empty
satisfying_DN_1
) ( non
empty
satisfying_DN_1
)
ComplLLattStr
) : ( ( ) (
V11
() )
set
) ))
`
)
: ( ( ) ( )
M2
( the
U1
of
b
1
: ( ( non
empty
satisfying_DN_1
) ( non
empty
satisfying_DN_1
)
ComplLLattStr
) : ( ( ) (
V11
() )
set
) ))
)
: ( ( ) ( )
M2
( the
U1
of
b
1
: ( ( non
empty
satisfying_DN_1
) ( non
empty
satisfying_DN_1
)
ComplLLattStr
) : ( ( ) (
V11
() )
set
) ))
`
)
: ( ( ) ( )
M2
( the
U1
of
b
1
: ( ( non
empty
satisfying_DN_1
) ( non
empty
satisfying_DN_1
)
ComplLLattStr
) : ( ( ) (
V11
() )
set
) ))
)
: ( ( ) ( )
M2
( the
U1
of
b
1
: ( ( non
empty
satisfying_DN_1
) ( non
empty
satisfying_DN_1
)
ComplLLattStr
) : ( ( ) (
V11
() )
set
) ))
`
)
: ( ( ) ( )
M2
( the
U1
of
b
1
: ( ( non
empty
satisfying_DN_1
) ( non
empty
satisfying_DN_1
)
ComplLLattStr
) : ( ( ) (
V11
() )
set
) ))
)
: ( ( ) ( )
M2
( the
U1
of
b
1
: ( ( non
empty
satisfying_DN_1
) ( non
empty
satisfying_DN_1
)
ComplLLattStr
) : ( ( ) (
V11
() )
set
) ))
`
: ( ( ) ( )
M2
( the
U1
of
b
1
: ( ( non
empty
satisfying_DN_1
) ( non
empty
satisfying_DN_1
)
ComplLLattStr
) : ( ( ) (
V11
() )
set
) ))
=
y
: ( ( ) ( )
Element
of ( ( ) (
V11
() )
set
) ) ;
theorem
:: ROBBINS2:2
for
L
being ( ( non
empty
satisfying_DN_1
) ( non
empty
satisfying_DN_1
)
ComplLLattStr
)
for
x
,
y
,
z
,
u
being ( ( ) ( )
Element
of ( ( ) (
V11
() )
set
) ) holds
(
(
(
x
: ( ( ) ( )
Element
of ( ( ) (
V11
() )
set
) )
+
y
: ( ( ) ( )
Element
of ( ( ) (
V11
() )
set
) )
)
: ( ( ) ( )
M2
( the
U1
of
b
1
: ( ( non
empty
satisfying_DN_1
) ( non
empty
satisfying_DN_1
)
ComplLLattStr
) : ( ( ) (
V11
() )
set
) ))
`
)
: ( ( ) ( )
M2
( the
U1
of
b
1
: ( ( non
empty
satisfying_DN_1
) ( non
empty
satisfying_DN_1
)
ComplLLattStr
) : ( ( ) (
V11
() )
set
) ))
+
(
(
(
(
z
: ( ( ) ( )
Element
of ( ( ) (
V11
() )
set
) )
+
x
: ( ( ) ( )
Element
of ( ( ) (
V11
() )
set
) )
)
: ( ( ) ( )
M2
( the
U1
of
b
1
: ( ( non
empty
satisfying_DN_1
) ( non
empty
satisfying_DN_1
)
ComplLLattStr
) : ( ( ) (
V11
() )
set
) ))
`
)
: ( ( ) ( )
M2
( the
U1
of
b
1
: ( ( non
empty
satisfying_DN_1
) ( non
empty
satisfying_DN_1
)
ComplLLattStr
) : ( ( ) (
V11
() )
set
) ))
+
(
(
(
y
: ( ( ) ( )
Element
of ( ( ) (
V11
() )
set
) )
`
)
: ( ( ) ( )
M2
( the
U1
of
b
1
: ( ( non
empty
satisfying_DN_1
) ( non
empty
satisfying_DN_1
)
ComplLLattStr
) : ( ( ) (
V11
() )
set
) ))
+
(
(
y
: ( ( ) ( )
Element
of ( ( ) (
V11
() )
set
) )
+
u
: ( ( ) ( )
Element
of ( ( ) (
V11
() )
set
) )
)
: ( ( ) ( )
M2
( the
U1
of
b
1
: ( ( non
empty
satisfying_DN_1
) ( non
empty
satisfying_DN_1
)
ComplLLattStr
) : ( ( ) (
V11
() )
set
) ))
`
)
: ( ( ) ( )
M2
( the
U1
of
b
1
: ( ( non
empty
satisfying_DN_1
) ( non
empty
satisfying_DN_1
)
ComplLLattStr
) : ( ( ) (
V11
() )
set
) ))
)
: ( ( ) ( )
M2
( the
U1
of
b
1
: ( ( non
empty
satisfying_DN_1
) ( non
empty
satisfying_DN_1
)
ComplLLattStr
) : ( ( ) (
V11
() )
set
) ))
`
)
: ( ( ) ( )
M2
( the
U1
of
b
1
: ( ( non
empty
satisfying_DN_1
) ( non
empty
satisfying_DN_1
)
ComplLLattStr
) : ( ( ) (
V11
() )
set
) ))
)
: ( ( ) ( )
M2
( the
U1
of
b
1
: ( ( non
empty
satisfying_DN_1
) ( non
empty
satisfying_DN_1
)
ComplLLattStr
) : ( ( ) (
V11
() )
set
) ))
`
)
: ( ( ) ( )
M2
( the
U1
of
b
1
: ( ( non
empty
satisfying_DN_1
) ( non
empty
satisfying_DN_1
)
ComplLLattStr
) : ( ( ) (
V11
() )
set
) ))
)
: ( ( ) ( )
M2
( the
U1
of
b
1
: ( ( non
empty
satisfying_DN_1
) ( non
empty
satisfying_DN_1
)
ComplLLattStr
) : ( ( ) (
V11
() )
set
) ))
`
: ( ( ) ( )
M2
( the
U1
of
b
1
: ( ( non
empty
satisfying_DN_1
) ( non
empty
satisfying_DN_1
)
ComplLLattStr
) : ( ( ) (
V11
() )
set
) ))
=
y
: ( ( ) ( )
Element
of ( ( ) (
V11
() )
set
) ) ;
theorem
:: ROBBINS2:3
for
L
being ( ( non
empty
satisfying_DN_1
) ( non
empty
satisfying_DN_1
)
ComplLLattStr
)
for
x
being ( ( ) ( )
Element
of ( ( ) (
V11
() )
set
) ) holds
(
(
(
x
: ( ( ) ( )
Element
of ( ( ) (
V11
() )
set
) )
+
(
x
: ( ( ) ( )
Element
of ( ( ) (
V11
() )
set
) )
`
)
: ( ( ) ( )
M2
( the
U1
of
b
1
: ( ( non
empty
satisfying_DN_1
) ( non
empty
satisfying_DN_1
)
ComplLLattStr
) : ( ( ) (
V11
() )
set
) ))
)
: ( ( ) ( )
M2
( the
U1
of
b
1
: ( ( non
empty
satisfying_DN_1
) ( non
empty
satisfying_DN_1
)
ComplLLattStr
) : ( ( ) (
V11
() )
set
) ))
`
)
: ( ( ) ( )
M2
( the
U1
of
b
1
: ( ( non
empty
satisfying_DN_1
) ( non
empty
satisfying_DN_1
)
ComplLLattStr
) : ( ( ) (
V11
() )
set
) ))
+
x
: ( ( ) ( )
Element
of ( ( ) (
V11
() )
set
) )
)
: ( ( ) ( )
M2
( the
U1
of
b
1
: ( ( non
empty
satisfying_DN_1
) ( non
empty
satisfying_DN_1
)
ComplLLattStr
) : ( ( ) (
V11
() )
set
) ))
`
: ( ( ) ( )
M2
( the
U1
of
b
1
: ( ( non
empty
satisfying_DN_1
) ( non
empty
satisfying_DN_1
)
ComplLLattStr
) : ( ( ) (
V11
() )
set
) ))
=
x
: ( ( ) ( )
Element
of ( ( ) (
V11
() )
set
) )
`
: ( ( ) ( )
M2
( the
U1
of
b
1
: ( ( non
empty
satisfying_DN_1
) ( non
empty
satisfying_DN_1
)
ComplLLattStr
) : ( ( ) (
V11
() )
set
) )) ;
theorem
:: ROBBINS2:4
for
L
being ( ( non
empty
satisfying_DN_1
) ( non
empty
satisfying_DN_1
)
ComplLLattStr
)
for
x
,
y
,
z
,
u
being ( ( ) ( )
Element
of ( ( ) (
V11
() )
set
) ) holds
(
(
(
x
: ( ( ) ( )
Element
of ( ( ) (
V11
() )
set
) )
+
y
: ( ( ) ( )
Element
of ( ( ) (
V11
() )
set
) )
)
: ( ( ) ( )
M2
( the
U1
of
b
1
: ( ( non
empty
satisfying_DN_1
) ( non
empty
satisfying_DN_1
)
ComplLLattStr
) : ( ( ) (
V11
() )
set
) ))
`
)
: ( ( ) ( )
M2
( the
U1
of
b
1
: ( ( non
empty
satisfying_DN_1
) ( non
empty
satisfying_DN_1
)
ComplLLattStr
) : ( ( ) (
V11
() )
set
) ))
+
(
(
(
(
z
: ( ( ) ( )
Element
of ( ( ) (
V11
() )
set
) )
+
x
: ( ( ) ( )
Element
of ( ( ) (
V11
() )
set
) )
)
: ( ( ) ( )
M2
( the
U1
of
b
1
: ( ( non
empty
satisfying_DN_1
) ( non
empty
satisfying_DN_1
)
ComplLLattStr
) : ( ( ) (
V11
() )
set
) ))
`
)
: ( ( ) ( )
M2
( the
U1
of
b
1
: ( ( non
empty
satisfying_DN_1
) ( non
empty
satisfying_DN_1
)
ComplLLattStr
) : ( ( ) (
V11
() )
set
) ))
+
(
(
(
(
(
(
y
: ( ( ) ( )
Element
of ( ( ) (
V11
() )
set
) )
+
(
y
: ( ( ) ( )
Element
of ( ( ) (
V11
() )
set
) )
`
)
: ( ( ) ( )
M2
( the
U1
of
b
1
: ( ( non
empty
satisfying_DN_1
) ( non
empty
satisfying_DN_1
)
ComplLLattStr
) : ( ( ) (
V11
() )
set
) ))
)
: ( ( ) ( )
M2
( the
U1
of
b
1
: ( ( non
empty
satisfying_DN_1
) ( non
empty
satisfying_DN_1
)
ComplLLattStr
) : ( ( ) (
V11
() )
set
) ))
`
)
: ( ( ) ( )
M2
( the
U1
of
b
1
: ( ( non
empty
satisfying_DN_1
) ( non
empty
satisfying_DN_1
)
ComplLLattStr
) : ( ( ) (
V11
() )
set
) ))
+
y
: ( ( ) ( )
Element
of ( ( ) (
V11
() )
set
) )
)
: ( ( ) ( )
M2
( the
U1
of
b
1
: ( ( non
empty
satisfying_DN_1
) ( non
empty
satisfying_DN_1
)
ComplLLattStr
) : ( ( ) (
V11
() )
set
) ))
`
)
: ( ( ) ( )
M2
( the
U1
of
b
1
: ( ( non
empty
satisfying_DN_1
) ( non
empty
satisfying_DN_1
)
ComplLLattStr
) : ( ( ) (
V11
() )
set
) ))
+
(
(
y
: ( ( ) ( )
Element
of ( ( ) (
V11
() )
set
) )
+
u
: ( ( ) ( )
Element
of ( ( ) (
V11
() )
set
) )
)
: ( ( ) ( )
M2
( the
U1
of
b
1
: ( ( non
empty
satisfying_DN_1
) ( non
empty
satisfying_DN_1
)
ComplLLattStr
) : ( ( ) (
V11
() )
set
) ))
`
)
: ( ( ) ( )
M2
( the
U1
of
b
1
: ( ( non
empty
satisfying_DN_1
) ( non
empty
satisfying_DN_1
)
ComplLLattStr
) : ( ( ) (
V11
() )
set
) ))
)
: ( ( ) ( )
M2
( the
U1
of
b
1
: ( ( non
empty
satisfying_DN_1
) ( non
empty
satisfying_DN_1
)
ComplLLattStr
) : ( ( ) (
V11
() )
set
) ))
`
)
: ( ( ) ( )
M2
( the
U1
of
b
1
: ( ( non
empty
satisfying_DN_1
) ( non
empty
satisfying_DN_1
)
ComplLLattStr
) : ( ( ) (
V11
() )
set
) ))
)
: ( ( ) ( )
M2
( the
U1
of
b
1
: ( ( non
empty
satisfying_DN_1
) ( non
empty
satisfying_DN_1
)
ComplLLattStr
) : ( ( ) (
V11
() )
set
) ))
`
)
: ( ( ) ( )
M2
( the
U1
of
b
1
: ( ( non
empty
satisfying_DN_1
) ( non
empty
satisfying_DN_1
)
ComplLLattStr
) : ( ( ) (
V11
() )
set
) ))
)
: ( ( ) ( )
M2
( the
U1
of
b
1
: ( ( non
empty
satisfying_DN_1
) ( non
empty
satisfying_DN_1
)
ComplLLattStr
) : ( ( ) (
V11
() )
set
) ))
`
: ( ( ) ( )
M2
( the
U1
of
b
1
: ( ( non
empty
satisfying_DN_1
) ( non
empty
satisfying_DN_1
)
ComplLLattStr
) : ( ( ) (
V11
() )
set
) ))
=
y
: ( ( ) ( )
Element
of ( ( ) (
V11
() )
set
) ) ;
theorem
:: ROBBINS2:5
for
L
being ( ( non
empty
satisfying_DN_1
) ( non
empty
satisfying_DN_1
)
ComplLLattStr
)
for
x
,
y
,
z
being ( ( ) ( )
Element
of ( ( ) (
V11
() )
set
) ) holds
(
(
(
x
: ( ( ) ( )
Element
of ( ( ) (
V11
() )
set
) )
+
y
: ( ( ) ( )
Element
of ( ( ) (
V11
() )
set
) )
)
: ( ( ) ( )
M2
( the
U1
of
b
1
: ( ( non
empty
satisfying_DN_1
) ( non
empty
satisfying_DN_1
)
ComplLLattStr
) : ( ( ) (
V11
() )
set
) ))
`
)
: ( ( ) ( )
M2
( the
U1
of
b
1
: ( ( non
empty
satisfying_DN_1
) ( non
empty
satisfying_DN_1
)
ComplLLattStr
) : ( ( ) (
V11
() )
set
) ))
+
(
(
(
(
z
: ( ( ) ( )
Element
of ( ( ) (
V11
() )
set
) )
+
x
: ( ( ) ( )
Element
of ( ( ) (
V11
() )
set
) )
)
: ( ( ) ( )
M2
( the
U1
of
b
1
: ( ( non
empty
satisfying_DN_1
) ( non
empty
satisfying_DN_1
)
ComplLLattStr
) : ( ( ) (
V11
() )
set
) ))
`
)
: ( ( ) ( )
M2
( the
U1
of
b
1
: ( ( non
empty
satisfying_DN_1
) ( non
empty
satisfying_DN_1
)
ComplLLattStr
) : ( ( ) (
V11
() )
set
) ))
+
y
: ( ( ) ( )
Element
of ( ( ) (
V11
() )
set
) )
)
: ( ( ) ( )
M2
( the
U1
of
b
1
: ( ( non
empty
satisfying_DN_1
) ( non
empty
satisfying_DN_1
)
ComplLLattStr
) : ( ( ) (
V11
() )
set
) ))
`
)
: ( ( ) ( )
M2
( the
U1
of
b
1
: ( ( non
empty
satisfying_DN_1
) ( non
empty
satisfying_DN_1
)
ComplLLattStr
) : ( ( ) (
V11
() )
set
) ))
)
: ( ( ) ( )
M2
( the
U1
of
b
1
: ( ( non
empty
satisfying_DN_1
) ( non
empty
satisfying_DN_1
)
ComplLLattStr
) : ( ( ) (
V11
() )
set
) ))
`
: ( ( ) ( )
M2
( the
U1
of
b
1
: ( ( non
empty
satisfying_DN_1
) ( non
empty
satisfying_DN_1
)
ComplLLattStr
) : ( ( ) (
V11
() )
set
) ))
=
y
: ( ( ) ( )
Element
of ( ( ) (
V11
() )
set
) ) ;
theorem
:: ROBBINS2:6
for
L
being ( ( non
empty
satisfying_DN_1
) ( non
empty
satisfying_DN_1
)
ComplLLattStr
)
for
x
,
y
being ( ( ) ( )
Element
of ( ( ) (
V11
() )
set
) ) holds
(
(
(
x
: ( ( ) ( )
Element
of ( ( ) (
V11
() )
set
) )
+
y
: ( ( ) ( )
Element
of ( ( ) (
V11
() )
set
) )
)
: ( ( ) ( )
M2
( the
U1
of
b
1
: ( ( non
empty
satisfying_DN_1
) ( non
empty
satisfying_DN_1
)
ComplLLattStr
) : ( ( ) (
V11
() )
set
) ))
`
)
: ( ( ) ( )
M2
( the
U1
of
b
1
: ( ( non
empty
satisfying_DN_1
) ( non
empty
satisfying_DN_1
)
ComplLLattStr
) : ( ( ) (
V11
() )
set
) ))
+
(
(
(
x
: ( ( ) ( )
Element
of ( ( ) (
V11
() )
set
) )
`
)
: ( ( ) ( )
M2
( the
U1
of
b
1
: ( ( non
empty
satisfying_DN_1
) ( non
empty
satisfying_DN_1
)
ComplLLattStr
) : ( ( ) (
V11
() )
set
) ))
+
y
: ( ( ) ( )
Element
of ( ( ) (
V11
() )
set
) )
)
: ( ( ) ( )
M2
( the
U1
of
b
1
: ( ( non
empty
satisfying_DN_1
) ( non
empty
satisfying_DN_1
)
ComplLLattStr
) : ( ( ) (
V11
() )
set
) ))
`
)
: ( ( ) ( )
M2
( the
U1
of
b
1
: ( ( non
empty
satisfying_DN_1
) ( non
empty
satisfying_DN_1
)
ComplLLattStr
) : ( ( ) (
V11
() )
set
) ))
)
: ( ( ) ( )
M2
( the
U1
of
b
1
: ( ( non
empty
satisfying_DN_1
) ( non
empty
satisfying_DN_1
)
ComplLLattStr
) : ( ( ) (
V11
() )
set
) ))
`
: ( ( ) ( )
M2
( the
U1
of
b
1
: ( ( non
empty
satisfying_DN_1
) ( non
empty
satisfying_DN_1
)
ComplLLattStr
) : ( ( ) (
V11
() )
set
) ))
=
y
: ( ( ) ( )
Element
of ( ( ) (
V11
() )
set
) ) ;
theorem
:: ROBBINS2:7
for
L
being ( ( non
empty
satisfying_DN_1
) ( non
empty
satisfying_DN_1
)
ComplLLattStr
)
for
x
,
y
being ( ( ) ( )
Element
of ( ( ) (
V11
() )
set
) ) holds
(
(
(
(
(
x
: ( ( ) ( )
Element
of ( ( ) (
V11
() )
set
) )
+
y
: ( ( ) ( )
Element
of ( ( ) (
V11
() )
set
) )
)
: ( ( ) ( )
M2
( the
U1
of
b
1
: ( ( non
empty
satisfying_DN_1
) ( non
empty
satisfying_DN_1
)
ComplLLattStr
) : ( ( ) (
V11
() )
set
) ))
`
)
: ( ( ) ( )
M2
( the
U1
of
b
1
: ( ( non
empty
satisfying_DN_1
) ( non
empty
satisfying_DN_1
)
ComplLLattStr
) : ( ( ) (
V11
() )
set
) ))
+
x
: ( ( ) ( )
Element
of ( ( ) (
V11
() )
set
) )
)
: ( ( ) ( )
M2
( the
U1
of
b
1
: ( ( non
empty
satisfying_DN_1
) ( non
empty
satisfying_DN_1
)
ComplLLattStr
) : ( ( ) (
V11
() )
set
) ))
`
)
: ( ( ) ( )
M2
( the
U1
of
b
1
: ( ( non
empty
satisfying_DN_1
) ( non
empty
satisfying_DN_1
)
ComplLLattStr
) : ( ( ) (
V11
() )
set
) ))
+
(
(
x
: ( ( ) ( )
Element
of ( ( ) (
V11
() )
set
) )
+
y
: ( ( ) ( )
Element
of ( ( ) (
V11
() )
set
) )
)
: ( ( ) ( )
M2
( the
U1
of
b
1
: ( ( non
empty
satisfying_DN_1
) ( non
empty
satisfying_DN_1
)
ComplLLattStr
) : ( ( ) (
V11
() )
set
) ))
`
)
: ( ( ) ( )
M2
( the
U1
of
b
1
: ( ( non
empty
satisfying_DN_1
) ( non
empty
satisfying_DN_1
)
ComplLLattStr
) : ( ( ) (
V11
() )
set
) ))
)
: ( ( ) ( )
M2
( the
U1
of
b
1
: ( ( non
empty
satisfying_DN_1
) ( non
empty
satisfying_DN_1
)
ComplLLattStr
) : ( ( ) (
V11
() )
set
) ))
`
: ( ( ) ( )
M2
( the
U1
of
b
1
: ( ( non
empty
satisfying_DN_1
) ( non
empty
satisfying_DN_1
)
ComplLLattStr
) : ( ( ) (
V11
() )
set
) ))
=
x
: ( ( ) ( )
Element
of ( ( ) (
V11
() )
set
) ) ;
theorem
:: ROBBINS2:8
for
L
being ( ( non
empty
satisfying_DN_1
) ( non
empty
satisfying_DN_1
)
ComplLLattStr
)
for
x
,
y
being ( ( ) ( )
Element
of ( ( ) (
V11
() )
set
) ) holds
(
x
: ( ( ) ( )
Element
of ( ( ) (
V11
() )
set
) )
+
(
(
(
(
x
: ( ( ) ( )
Element
of ( ( ) (
V11
() )
set
) )
+
y
: ( ( ) ( )
Element
of ( ( ) (
V11
() )
set
) )
)
: ( ( ) ( )
M2
( the
U1
of
b
1
: ( ( non
empty
satisfying_DN_1
) ( non
empty
satisfying_DN_1
)
ComplLLattStr
) : ( ( ) (
V11
() )
set
) ))
`
)
: ( ( ) ( )
M2
( the
U1
of
b
1
: ( ( non
empty
satisfying_DN_1
) ( non
empty
satisfying_DN_1
)
ComplLLattStr
) : ( ( ) (
V11
() )
set
) ))
+
x
: ( ( ) ( )
Element
of ( ( ) (
V11
() )
set
) )
)
: ( ( ) ( )
M2
( the
U1
of
b
1
: ( ( non
empty
satisfying_DN_1
) ( non
empty
satisfying_DN_1
)
ComplLLattStr
) : ( ( ) (
V11
() )
set
) ))
`
)
: ( ( ) ( )
M2
( the
U1
of
b
1
: ( ( non
empty
satisfying_DN_1
) ( non
empty
satisfying_DN_1
)
ComplLLattStr
) : ( ( ) (
V11
() )
set
) ))
)
: ( ( ) ( )
M2
( the
U1
of
b
1
: ( ( non
empty
satisfying_DN_1
) ( non
empty
satisfying_DN_1
)
ComplLLattStr
) : ( ( ) (
V11
() )
set
) ))
`
: ( ( ) ( )
M2
( the
U1
of
b
1
: ( ( non
empty
satisfying_DN_1
) ( non
empty
satisfying_DN_1
)
ComplLLattStr
) : ( ( ) (
V11
() )
set
) ))
=
(
x
: ( ( ) ( )
Element
of ( ( ) (
V11
() )
set
) )
+
y
: ( ( ) ( )
Element
of ( ( ) (
V11
() )
set
) )
)
: ( ( ) ( )
M2
( the
U1
of
b
1
: ( ( non
empty
satisfying_DN_1
) ( non
empty
satisfying_DN_1
)
ComplLLattStr
) : ( ( ) (
V11
() )
set
) ))
`
: ( ( ) ( )
M2
( the
U1
of
b
1
: ( ( non
empty
satisfying_DN_1
) ( non
empty
satisfying_DN_1
)
ComplLLattStr
) : ( ( ) (
V11
() )
set
) )) ;
theorem
:: ROBBINS2:9
for
L
being ( ( non
empty
satisfying_DN_1
) ( non
empty
satisfying_DN_1
)
ComplLLattStr
)
for
x
,
y
,
z
being ( ( ) ( )
Element
of ( ( ) (
V11
() )
set
) ) holds
(
(
(
(
(
x
: ( ( ) ( )
Element
of ( ( ) (
V11
() )
set
) )
+
y
: ( ( ) ( )
Element
of ( ( ) (
V11
() )
set
) )
)
: ( ( ) ( )
M2
( the
U1
of
b
1
: ( ( non
empty
satisfying_DN_1
) ( non
empty
satisfying_DN_1
)
ComplLLattStr
) : ( ( ) (
V11
() )
set
) ))
`
)
: ( ( ) ( )
M2
( the
U1
of
b
1
: ( ( non
empty
satisfying_DN_1
) ( non
empty
satisfying_DN_1
)
ComplLLattStr
) : ( ( ) (
V11
() )
set
) ))
+
z
: ( ( ) ( )
Element
of ( ( ) (
V11
() )
set
) )
)
: ( ( ) ( )
M2
( the
U1
of
b
1
: ( ( non
empty
satisfying_DN_1
) ( non
empty
satisfying_DN_1
)
ComplLLattStr
) : ( ( ) (
V11
() )
set
) ))
`
)
: ( ( ) ( )
M2
( the
U1
of
b
1
: ( ( non
empty
satisfying_DN_1
) ( non
empty
satisfying_DN_1
)
ComplLLattStr
) : ( ( ) (
V11
() )
set
) ))
+
(
(
x
: ( ( ) ( )
Element
of ( ( ) (
V11
() )
set
) )
+
z
: ( ( ) ( )
Element
of ( ( ) (
V11
() )
set
) )
)
: ( ( ) ( )
M2
( the
U1
of
b
1
: ( ( non
empty
satisfying_DN_1
) ( non
empty
satisfying_DN_1
)
ComplLLattStr
) : ( ( ) (
V11
() )
set
) ))
`
)
: ( ( ) ( )
M2
( the
U1
of
b
1
: ( ( non
empty
satisfying_DN_1
) ( non
empty
satisfying_DN_1
)
ComplLLattStr
) : ( ( ) (
V11
() )
set
) ))
)
: ( ( ) ( )
M2
( the
U1
of
b
1
: ( ( non
empty
satisfying_DN_1
) ( non
empty
satisfying_DN_1
)
ComplLLattStr
) : ( ( ) (
V11
() )
set
) ))
`
: ( ( ) ( )
M2
( the
U1
of
b
1
: ( ( non
empty
satisfying_DN_1
) ( non
empty
satisfying_DN_1
)
ComplLLattStr
) : ( ( ) (
V11
() )
set
) ))
=
z
: ( ( ) ( )
Element
of ( ( ) (
V11
() )
set
) ) ;
theorem
:: ROBBINS2:10
for
L
being ( ( non
empty
satisfying_DN_1
) ( non
empty
satisfying_DN_1
)
ComplLLattStr
)
for
x
,
y
,
z
being ( ( ) ( )
Element
of ( ( ) (
V11
() )
set
) ) holds
(
x
: ( ( ) ( )
Element
of ( ( ) (
V11
() )
set
) )
+
(
(
(
(
y
: ( ( ) ( )
Element
of ( ( ) (
V11
() )
set
) )
+
z
: ( ( ) ( )
Element
of ( ( ) (
V11
() )
set
) )
)
: ( ( ) ( )
M2
( the
U1
of
b
1
: ( ( non
empty
satisfying_DN_1
) ( non
empty
satisfying_DN_1
)
ComplLLattStr
) : ( ( ) (
V11
() )
set
) ))
`
)
: ( ( ) ( )
M2
( the
U1
of
b
1
: ( ( non
empty
satisfying_DN_1
) ( non
empty
satisfying_DN_1
)
ComplLLattStr
) : ( ( ) (
V11
() )
set
) ))
+
(
(
y
: ( ( ) ( )
Element
of ( ( ) (
V11
() )
set
) )
+
x
: ( ( ) ( )
Element
of ( ( ) (
V11
() )
set
) )
)
: ( ( ) ( )
M2
( the
U1
of
b
1
: ( ( non
empty
satisfying_DN_1
) ( non
empty
satisfying_DN_1
)
ComplLLattStr
) : ( ( ) (
V11
() )
set
) ))
`
)
: ( ( ) ( )
M2
( the
U1
of
b
1
: ( ( non
empty
satisfying_DN_1
) ( non
empty
satisfying_DN_1
)
ComplLLattStr
) : ( ( ) (
V11
() )
set
) ))
)
: ( ( ) ( )
M2
( the
U1
of
b
1
: ( ( non
empty
satisfying_DN_1
) ( non
empty
satisfying_DN_1
)
ComplLLattStr
) : ( ( ) (
V11
() )
set
) ))
`
)
: ( ( ) ( )
M2
( the
U1
of
b
1
: ( ( non
empty
satisfying_DN_1
) ( non
empty
satisfying_DN_1
)
ComplLLattStr
) : ( ( ) (
V11
() )
set
) ))
)
: ( ( ) ( )
M2
( the
U1
of
b
1
: ( ( non
empty
satisfying_DN_1
) ( non
empty
satisfying_DN_1
)
ComplLLattStr
) : ( ( ) (
V11
() )
set
) ))
`
: ( ( ) ( )
M2
( the
U1
of
b
1
: ( ( non
empty
satisfying_DN_1
) ( non
empty
satisfying_DN_1
)
ComplLLattStr
) : ( ( ) (
V11
() )
set
) ))
=
(
y
: ( ( ) ( )
Element
of ( ( ) (
V11
() )
set
) )
+
x
: ( ( ) ( )
Element
of ( ( ) (
V11
() )
set
) )
)
: ( ( ) ( )
M2
( the
U1
of
b
1
: ( ( non
empty
satisfying_DN_1
) ( non
empty
satisfying_DN_1
)
ComplLLattStr
) : ( ( ) (
V11
() )
set
) ))
`
: ( ( ) ( )
M2
( the
U1
of
b
1
: ( ( non
empty
satisfying_DN_1
) ( non
empty
satisfying_DN_1
)
ComplLLattStr
) : ( ( ) (
V11
() )
set
) )) ;
theorem
:: ROBBINS2:11
for
L
being ( ( non
empty
satisfying_DN_1
) ( non
empty
satisfying_DN_1
)
ComplLLattStr
)
for
x
,
y
,
z
being ( ( ) ( )
Element
of ( ( ) (
V11
() )
set
) ) holds
(
(
(
(
(
(
(
x
: ( ( ) ( )
Element
of ( ( ) (
V11
() )
set
) )
+
y
: ( ( ) ( )
Element
of ( ( ) (
V11
() )
set
) )
)
: ( ( ) ( )
M2
( the
U1
of
b
1
: ( ( non
empty
satisfying_DN_1
) ( non
empty
satisfying_DN_1
)
ComplLLattStr
) : ( ( ) (
V11
() )
set
) ))
`
)
: ( ( ) ( )
M2
( the
U1
of
b
1
: ( ( non
empty
satisfying_DN_1
) ( non
empty
satisfying_DN_1
)
ComplLLattStr
) : ( ( ) (
V11
() )
set
) ))
+
z
: ( ( ) ( )
Element
of ( ( ) (
V11
() )
set
) )
)
: ( ( ) ( )
M2
( the
U1
of
b
1
: ( ( non
empty
satisfying_DN_1
) ( non
empty
satisfying_DN_1
)
ComplLLattStr
) : ( ( ) (
V11
() )
set
) ))
`
)
: ( ( ) ( )
M2
( the
U1
of
b
1
: ( ( non
empty
satisfying_DN_1
) ( non
empty
satisfying_DN_1
)
ComplLLattStr
) : ( ( ) (
V11
() )
set
) ))
+
(
(
(
x
: ( ( ) ( )
Element
of ( ( ) (
V11
() )
set
) )
`
)
: ( ( ) ( )
M2
( the
U1
of
b
1
: ( ( non
empty
satisfying_DN_1
) ( non
empty
satisfying_DN_1
)
ComplLLattStr
) : ( ( ) (
V11
() )
set
) ))
+
y
: ( ( ) ( )
Element
of ( ( ) (
V11
() )
set
) )
)
: ( ( ) ( )
M2
( the
U1
of
b
1
: ( ( non
empty
satisfying_DN_1
) ( non
empty
satisfying_DN_1
)
ComplLLattStr
) : ( ( ) (
V11
() )
set
) ))
`
)
: ( ( ) ( )
M2
( the
U1
of
b
1
: ( ( non
empty
satisfying_DN_1
) ( non
empty
satisfying_DN_1
)
ComplLLattStr
) : ( ( ) (
V11
() )
set
) ))
)
: ( ( ) ( )
M2
( the
U1
of
b
1
: ( ( non
empty
satisfying_DN_1
) ( non
empty
satisfying_DN_1
)
ComplLLattStr
) : ( ( ) (
V11
() )
set
) ))
`
)
: ( ( ) ( )
M2
( the
U1
of
b
1
: ( ( non
empty
satisfying_DN_1
) ( non
empty
satisfying_DN_1
)
ComplLLattStr
) : ( ( ) (
V11
() )
set
) ))
+
y
: ( ( ) ( )
Element
of ( ( ) (
V11
() )
set
) )
)
: ( ( ) ( )
M2
( the
U1
of
b
1
: ( ( non
empty
satisfying_DN_1
) ( non
empty
satisfying_DN_1
)
ComplLLattStr
) : ( ( ) (
V11
() )
set
) ))
`
: ( ( ) ( )
M2
( the
U1
of
b
1
: ( ( non
empty
satisfying_DN_1
) ( non
empty
satisfying_DN_1
)
ComplLLattStr
) : ( ( ) (
V11
() )
set
) ))
=
(
(
x
: ( ( ) ( )
Element
of ( ( ) (
V11
() )
set
) )
`
)
: ( ( ) ( )
M2
( the
U1
of
b
1
: ( ( non
empty
satisfying_DN_1
) ( non
empty
satisfying_DN_1
)
ComplLLattStr
) : ( ( ) (
V11
() )
set
) ))
+
y
: ( ( ) ( )
Element
of ( ( ) (
V11
() )
set
) )
)
: ( ( ) ( )
M2
( the
U1
of
b
1
: ( ( non
empty
satisfying_DN_1
) ( non
empty
satisfying_DN_1
)
ComplLLattStr
) : ( ( ) (
V11
() )
set
) ))
`
: ( ( ) ( )
M2
( the
U1
of
b
1
: ( ( non
empty
satisfying_DN_1
) ( non
empty
satisfying_DN_1
)
ComplLLattStr
) : ( ( ) (
V11
() )
set
) )) ;
theorem
:: ROBBINS2:12
for
L
being ( ( non
empty
satisfying_DN_1
) ( non
empty
satisfying_DN_1
)
ComplLLattStr
)
for
x
,
y
,
z
being ( ( ) ( )
Element
of ( ( ) (
V11
() )
set
) ) holds
(
x
: ( ( ) ( )
Element
of ( ( ) (
V11
() )
set
) )
+
(
(
(
(
y
: ( ( ) ( )
Element
of ( ( ) (
V11
() )
set
) )
+
z
: ( ( ) ( )
Element
of ( ( ) (
V11
() )
set
) )
)
: ( ( ) ( )
M2
( the
U1
of
b
1
: ( ( non
empty
satisfying_DN_1
) ( non
empty
satisfying_DN_1
)
ComplLLattStr
) : ( ( ) (
V11
() )
set
) ))
`
)
: ( ( ) ( )
M2
( the
U1
of
b
1
: ( ( non
empty
satisfying_DN_1
) ( non
empty
satisfying_DN_1
)
ComplLLattStr
) : ( ( ) (
V11
() )
set
) ))
+
(
(
z
: ( ( ) ( )
Element
of ( ( ) (
V11
() )
set
) )
+
x
: ( ( ) ( )
Element
of ( ( ) (
V11
() )
set
) )
)
: ( ( ) ( )
M2
( the
U1
of
b
1
: ( ( non
empty
satisfying_DN_1
) ( non
empty
satisfying_DN_1
)
ComplLLattStr
) : ( ( ) (
V11
() )
set
) ))
`
)
: ( ( ) ( )
M2
( the
U1
of
b
1
: ( ( non
empty
satisfying_DN_1
) ( non
empty
satisfying_DN_1
)
ComplLLattStr
) : ( ( ) (
V11
() )
set
) ))
)
: ( ( ) ( )
M2
( the
U1
of
b
1
: ( ( non
empty
satisfying_DN_1
) ( non
empty
satisfying_DN_1
)
ComplLLattStr
) : ( ( ) (
V11
() )
set
) ))
`
)
: ( ( ) ( )
M2
( the
U1
of
b
1
: ( ( non
empty
satisfying_DN_1
) ( non
empty
satisfying_DN_1
)
ComplLLattStr
) : ( ( ) (
V11
() )
set
) ))
)
: ( ( ) ( )
M2
( the
U1
of
b
1
: ( ( non
empty
satisfying_DN_1
) ( non
empty
satisfying_DN_1
)
ComplLLattStr
) : ( ( ) (
V11
() )
set
) ))
`
: ( ( ) ( )
M2
( the
U1
of
b
1
: ( ( non
empty
satisfying_DN_1
) ( non
empty
satisfying_DN_1
)
ComplLLattStr
) : ( ( ) (
V11
() )
set
) ))
=
(
z
: ( ( ) ( )
Element
of ( ( ) (
V11
() )
set
) )
+
x
: ( ( ) ( )
Element
of ( ( ) (
V11
() )
set
) )
)
: ( ( ) ( )
M2
( the
U1
of
b
1
: ( ( non
empty
satisfying_DN_1
) ( non
empty
satisfying_DN_1
)
ComplLLattStr
) : ( ( ) (
V11
() )
set
) ))
`
: ( ( ) ( )
M2
( the
U1
of
b
1
: ( ( non
empty
satisfying_DN_1
) ( non
empty
satisfying_DN_1
)
ComplLLattStr
) : ( ( ) (
V11
() )
set
) )) ;
theorem
:: ROBBINS2:13
for
L
being ( ( non
empty
satisfying_DN_1
) ( non
empty
satisfying_DN_1
)
ComplLLattStr
)
for
x
,
y
,
z
,
u
being ( ( ) ( )
Element
of ( ( ) (
V11
() )
set
) ) holds
(
(
(
x
: ( ( ) ( )
Element
of ( ( ) (
V11
() )
set
) )
+
y
: ( ( ) ( )
Element
of ( ( ) (
V11
() )
set
) )
)
: ( ( ) ( )
M2
( the
U1
of
b
1
: ( ( non
empty
satisfying_DN_1
) ( non
empty
satisfying_DN_1
)
ComplLLattStr
) : ( ( ) (
V11
() )
set
) ))
`
)
: ( ( ) ( )
M2
( the
U1
of
b
1
: ( ( non
empty
satisfying_DN_1
) ( non
empty
satisfying_DN_1
)
ComplLLattStr
) : ( ( ) (
V11
() )
set
) ))
+
(
(
(
(
z
: ( ( ) ( )
Element
of ( ( ) (
V11
() )
set
) )
+
x
: ( ( ) ( )
Element
of ( ( ) (
V11
() )
set
) )
)
: ( ( ) ( )
M2
( the
U1
of
b
1
: ( ( non
empty
satisfying_DN_1
) ( non
empty
satisfying_DN_1
)
ComplLLattStr
) : ( ( ) (
V11
() )
set
) ))
`
)
: ( ( ) ( )
M2
( the
U1
of
b
1
: ( ( non
empty
satisfying_DN_1
) ( non
empty
satisfying_DN_1
)
ComplLLattStr
) : ( ( ) (
V11
() )
set
) ))
+
(
(
(
y
: ( ( ) ( )
Element
of ( ( ) (
V11
() )
set
) )
`
)
: ( ( ) ( )
M2
( the
U1
of
b
1
: ( ( non
empty
satisfying_DN_1
) ( non
empty
satisfying_DN_1
)
ComplLLattStr
) : ( ( ) (
V11
() )
set
) ))
+
(
(
u
: ( ( ) ( )
Element
of ( ( ) (
V11
() )
set
) )
+
y
: ( ( ) ( )
Element
of ( ( ) (
V11
() )
set
) )
)
: ( ( ) ( )
M2
( the
U1
of
b
1
: ( ( non
empty
satisfying_DN_1
) ( non
empty
satisfying_DN_1
)
ComplLLattStr
) : ( ( ) (
V11
() )
set
) ))
`
)
: ( ( ) ( )
M2
( the
U1
of
b
1
: ( ( non
empty
satisfying_DN_1
) ( non
empty
satisfying_DN_1
)
ComplLLattStr
) : ( ( ) (
V11
() )
set
) ))
)
: ( ( ) ( )
M2
( the
U1
of
b
1
: ( ( non
empty
satisfying_DN_1
) ( non
empty
satisfying_DN_1
)
ComplLLattStr
) : ( ( ) (
V11
() )
set
) ))
`
)
: ( ( ) ( )
M2
( the
U1
of
b
1
: ( ( non
empty
satisfying_DN_1
) ( non
empty
satisfying_DN_1
)
ComplLLattStr
) : ( ( ) (
V11
() )
set
) ))
)
: ( ( ) ( )
M2
( the
U1
of
b
1
: ( ( non
empty
satisfying_DN_1
) ( non
empty
satisfying_DN_1
)
ComplLLattStr
) : ( ( ) (
V11
() )
set
) ))
`
)
: ( ( ) ( )
M2
( the
U1
of
b
1
: ( ( non
empty
satisfying_DN_1
) ( non
empty
satisfying_DN_1
)
ComplLLattStr
) : ( ( ) (
V11
() )
set
) ))
)
: ( ( ) ( )
M2
( the
U1
of
b
1
: ( ( non
empty
satisfying_DN_1
) ( non
empty
satisfying_DN_1
)
ComplLLattStr
) : ( ( ) (
V11
() )
set
) ))
`
: ( ( ) ( )
M2
( the
U1
of
b
1
: ( ( non
empty
satisfying_DN_1
) ( non
empty
satisfying_DN_1
)
ComplLLattStr
) : ( ( ) (
V11
() )
set
) ))
=
y
: ( ( ) ( )
Element
of ( ( ) (
V11
() )
set
) ) ;
theorem
:: ROBBINS2:14
for
L
being ( ( non
empty
satisfying_DN_1
) ( non
empty
satisfying_DN_1
)
ComplLLattStr
)
for
x
,
y
being ( ( ) ( )
Element
of ( ( ) (
V11
() )
set
) ) holds
(
x
: ( ( ) ( )
Element
of ( ( ) (
V11
() )
set
) )
+
y
: ( ( ) ( )
Element
of ( ( ) (
V11
() )
set
) )
)
: ( ( ) ( )
M2
( the
U1
of
b
1
: ( ( non
empty
satisfying_DN_1
) ( non
empty
satisfying_DN_1
)
ComplLLattStr
) : ( ( ) (
V11
() )
set
) ))
`
: ( ( ) ( )
M2
( the
U1
of
b
1
: ( ( non
empty
satisfying_DN_1
) ( non
empty
satisfying_DN_1
)
ComplLLattStr
) : ( ( ) (
V11
() )
set
) ))
=
(
y
: ( ( ) ( )
Element
of ( ( ) (
V11
() )
set
) )
+
x
: ( ( ) ( )
Element
of ( ( ) (
V11
() )
set
) )
)
: ( ( ) ( )
M2
( the
U1
of
b
1
: ( ( non
empty
satisfying_DN_1
) ( non
empty
satisfying_DN_1
)
ComplLLattStr
) : ( ( ) (
V11
() )
set
) ))
`
: ( ( ) ( )
M2
( the
U1
of
b
1
: ( ( non
empty
satisfying_DN_1
) ( non
empty
satisfying_DN_1
)
ComplLLattStr
) : ( ( ) (
V11
() )
set
) )) ;
theorem
:: ROBBINS2:15
for
L
being ( ( non
empty
satisfying_DN_1
) ( non
empty
satisfying_DN_1
)
ComplLLattStr
)
for
x
,
y
,
z
being ( ( ) ( )
Element
of ( ( ) (
V11
() )
set
) ) holds
(
(
(
(
(
x
: ( ( ) ( )
Element
of ( ( ) (
V11
() )
set
) )
+
y
: ( ( ) ( )
Element
of ( ( ) (
V11
() )
set
) )
)
: ( ( ) ( )
M2
( the
U1
of
b
1
: ( ( non
empty
satisfying_DN_1
) ( non
empty
satisfying_DN_1
)
ComplLLattStr
) : ( ( ) (
V11
() )
set
) ))
`
)
: ( ( ) ( )
M2
( the
U1
of
b
1
: ( ( non
empty
satisfying_DN_1
) ( non
empty
satisfying_DN_1
)
ComplLLattStr
) : ( ( ) (
V11
() )
set
) ))
+
(
(
y
: ( ( ) ( )
Element
of ( ( ) (
V11
() )
set
) )
+
z
: ( ( ) ( )
Element
of ( ( ) (
V11
() )
set
) )
)
: ( ( ) ( )
M2
( the
U1
of
b
1
: ( ( non
empty
satisfying_DN_1
) ( non
empty
satisfying_DN_1
)
ComplLLattStr
) : ( ( ) (
V11
() )
set
) ))
`
)
: ( ( ) ( )
M2
( the
U1
of
b
1
: ( ( non
empty
satisfying_DN_1
) ( non
empty
satisfying_DN_1
)
ComplLLattStr
) : ( ( ) (
V11
() )
set
) ))
)
: ( ( ) ( )
M2
( the
U1
of
b
1
: ( ( non
empty
satisfying_DN_1
) ( non
empty
satisfying_DN_1
)
ComplLLattStr
) : ( ( ) (
V11
() )
set
) ))
`
)
: ( ( ) ( )
M2
( the
U1
of
b
1
: ( ( non
empty
satisfying_DN_1
) ( non
empty
satisfying_DN_1
)
ComplLLattStr
) : ( ( ) (
V11
() )
set
) ))
+
z
: ( ( ) ( )
Element
of ( ( ) (
V11
() )
set
) )
)
: ( ( ) ( )
M2
( the
U1
of
b
1
: ( ( non
empty
satisfying_DN_1
) ( non
empty
satisfying_DN_1
)
ComplLLattStr
) : ( ( ) (
V11
() )
set
) ))
`
: ( ( ) ( )
M2
( the
U1
of
b
1
: ( ( non
empty
satisfying_DN_1
) ( non
empty
satisfying_DN_1
)
ComplLLattStr
) : ( ( ) (
V11
() )
set
) ))
=
(
y
: ( ( ) ( )
Element
of ( ( ) (
V11
() )
set
) )
+
z
: ( ( ) ( )
Element
of ( ( ) (
V11
() )
set
) )
)
: ( ( ) ( )
M2
( the
U1
of
b
1
: ( ( non
empty
satisfying_DN_1
) ( non
empty
satisfying_DN_1
)
ComplLLattStr
) : ( ( ) (
V11
() )
set
) ))
`
: ( ( ) ( )
M2
( the
U1
of
b
1
: ( ( non
empty
satisfying_DN_1
) ( non
empty
satisfying_DN_1
)
ComplLLattStr
) : ( ( ) (
V11
() )
set
) )) ;
theorem
:: ROBBINS2:16
for
L
being ( ( non
empty
satisfying_DN_1
) ( non
empty
satisfying_DN_1
)
ComplLLattStr
)
for
x
,
y
,
z
being ( ( ) ( )
Element
of ( ( ) (
V11
() )
set
) ) holds
(
(
(
x
: ( ( ) ( )
Element
of ( ( ) (
V11
() )
set
) )
+
(
(
(
(
x
: ( ( ) ( )
Element
of ( ( ) (
V11
() )
set
) )
+
y
: ( ( ) ( )
Element
of ( ( ) (
V11
() )
set
) )
)
: ( ( ) ( )
M2
( the
U1
of
b
1
: ( ( non
empty
satisfying_DN_1
) ( non
empty
satisfying_DN_1
)
ComplLLattStr
) : ( ( ) (
V11
() )
set
) ))
`
)
: ( ( ) ( )
M2
( the
U1
of
b
1
: ( ( non
empty
satisfying_DN_1
) ( non
empty
satisfying_DN_1
)
ComplLLattStr
) : ( ( ) (
V11
() )
set
) ))
+
z
: ( ( ) ( )
Element
of ( ( ) (
V11
() )
set
) )
)
: ( ( ) ( )
M2
( the
U1
of
b
1
: ( ( non
empty
satisfying_DN_1
) ( non
empty
satisfying_DN_1
)
ComplLLattStr
) : ( ( ) (
V11
() )
set
) ))
`
)
: ( ( ) ( )
M2
( the
U1
of
b
1
: ( ( non
empty
satisfying_DN_1
) ( non
empty
satisfying_DN_1
)
ComplLLattStr
) : ( ( ) (
V11
() )
set
) ))
)
: ( ( ) ( )
M2
( the
U1
of
b
1
: ( ( non
empty
satisfying_DN_1
) ( non
empty
satisfying_DN_1
)
ComplLLattStr
) : ( ( ) (
V11
() )
set
) ))
`
)
: ( ( ) ( )
M2
( the
U1
of
b
1
: ( ( non
empty
satisfying_DN_1
) ( non
empty
satisfying_DN_1
)
ComplLLattStr
) : ( ( ) (
V11
() )
set
) ))
+
z
: ( ( ) ( )
Element
of ( ( ) (
V11
() )
set
) )
)
: ( ( ) ( )
M2
( the
U1
of
b
1
: ( ( non
empty
satisfying_DN_1
) ( non
empty
satisfying_DN_1
)
ComplLLattStr
) : ( ( ) (
V11
() )
set
) ))
`
: ( ( ) ( )
M2
( the
U1
of
b
1
: ( ( non
empty
satisfying_DN_1
) ( non
empty
satisfying_DN_1
)
ComplLLattStr
) : ( ( ) (
V11
() )
set
) ))
=
(
(
(
x
: ( ( ) ( )
Element
of ( ( ) (
V11
() )
set
) )
+
y
: ( ( ) ( )
Element
of ( ( ) (
V11
() )
set
) )
)
: ( ( ) ( )
M2
( the
U1
of
b
1
: ( ( non
empty
satisfying_DN_1
) ( non
empty
satisfying_DN_1
)
ComplLLattStr
) : ( ( ) (
V11
() )
set
) ))
`
)
: ( ( ) ( )
M2
( the
U1
of
b
1
: ( ( non
empty
satisfying_DN_1
) ( non
empty
satisfying_DN_1
)
ComplLLattStr
) : ( ( ) (
V11
() )
set
) ))
+
z
: ( ( ) ( )
Element
of ( ( ) (
V11
() )
set
) )
)
: ( ( ) ( )
M2
( the
U1
of
b
1
: ( ( non
empty
satisfying_DN_1
) ( non
empty
satisfying_DN_1
)
ComplLLattStr
) : ( ( ) (
V11
() )
set
) ))
`
: ( ( ) ( )
M2
( the
U1
of
b
1
: ( ( non
empty
satisfying_DN_1
) ( non
empty
satisfying_DN_1
)
ComplLLattStr
) : ( ( ) (
V11
() )
set
) )) ;
theorem
:: ROBBINS2:17
for
L
being ( ( non
empty
satisfying_DN_1
) ( non
empty
satisfying_DN_1
)
ComplLLattStr
)
for
x
,
y
being ( ( ) ( )
Element
of ( ( ) (
V11
() )
set
) ) holds
(
(
(
(
(
x
: ( ( ) ( )
Element
of ( ( ) (
V11
() )
set
) )
+
y
: ( ( ) ( )
Element
of ( ( ) (
V11
() )
set
) )
)
: ( ( ) ( )
M2
( the
U1
of
b
1
: ( ( non
empty
satisfying_DN_1
) ( non
empty
satisfying_DN_1
)
ComplLLattStr
) : ( ( ) (
V11
() )
set
) ))
`
)
: ( ( ) ( )
M2
( the
U1
of
b
1
: ( ( non
empty
satisfying_DN_1
) ( non
empty
satisfying_DN_1
)
ComplLLattStr
) : ( ( ) (
V11
() )
set
) ))
+
x
: ( ( ) ( )
Element
of ( ( ) (
V11
() )
set
) )
)
: ( ( ) ( )
M2
( the
U1
of
b
1
: ( ( non
empty
satisfying_DN_1
) ( non
empty
satisfying_DN_1
)
ComplLLattStr
) : ( ( ) (
V11
() )
set
) ))
`
)
: ( ( ) ( )
M2
( the
U1
of
b
1
: ( ( non
empty
satisfying_DN_1
) ( non
empty
satisfying_DN_1
)
ComplLLattStr
) : ( ( ) (
V11
() )
set
) ))
+
y
: ( ( ) ( )
Element
of ( ( ) (
V11
() )
set
) )
)
: ( ( ) ( )
M2
( the
U1
of
b
1
: ( ( non
empty
satisfying_DN_1
) ( non
empty
satisfying_DN_1
)
ComplLLattStr
) : ( ( ) (
V11
() )
set
) ))
`
: ( ( ) ( )
M2
( the
U1
of
b
1
: ( ( non
empty
satisfying_DN_1
) ( non
empty
satisfying_DN_1
)
ComplLLattStr
) : ( ( ) (
V11
() )
set
) ))
=
(
y
: ( ( ) ( )
Element
of ( ( ) (
V11
() )
set
) )
+
y
: ( ( ) ( )
Element
of ( ( ) (
V11
() )
set
) )
)
: ( ( ) ( )
M2
( the
U1
of
b
1
: ( ( non
empty
satisfying_DN_1
) ( non
empty
satisfying_DN_1
)
ComplLLattStr
) : ( ( ) (
V11
() )
set
) ))
`
: ( ( ) ( )
M2
( the
U1
of
b
1
: ( ( non
empty
satisfying_DN_1
) ( non
empty
satisfying_DN_1
)
ComplLLattStr
) : ( ( ) (
V11
() )
set
) )) ;
theorem
:: ROBBINS2:18
for
L
being ( ( non
empty
satisfying_DN_1
) ( non
empty
satisfying_DN_1
)
ComplLLattStr
)
for
x
,
y
being ( ( ) ( )
Element
of ( ( ) (
V11
() )
set
) ) holds
(
(
x
: ( ( ) ( )
Element
of ( ( ) (
V11
() )
set
) )
`
)
: ( ( ) ( )
M2
( the
U1
of
b
1
: ( ( non
empty
satisfying_DN_1
) ( non
empty
satisfying_DN_1
)
ComplLLattStr
) : ( ( ) (
V11
() )
set
) ))
+
(
(
y
: ( ( ) ( )
Element
of ( ( ) (
V11
() )
set
) )
+
x
: ( ( ) ( )
Element
of ( ( ) (
V11
() )
set
) )
)
: ( ( ) ( )
M2
( the
U1
of
b
1
: ( ( non
empty
satisfying_DN_1
) ( non
empty
satisfying_DN_1
)
ComplLLattStr
) : ( ( ) (
V11
() )
set
) ))
`
)
: ( ( ) ( )
M2
( the
U1
of
b
1
: ( ( non
empty
satisfying_DN_1
) ( non
empty
satisfying_DN_1
)
ComplLLattStr
) : ( ( ) (
V11
() )
set
) ))
)
: ( ( ) ( )
M2
( the
U1
of
b
1
: ( ( non
empty
satisfying_DN_1
) ( non
empty
satisfying_DN_1
)
ComplLLattStr
) : ( ( ) (
V11
() )
set
) ))
`
: ( ( ) ( )
M2
( the
U1
of
b
1
: ( ( non
empty
satisfying_DN_1
) ( non
empty
satisfying_DN_1
)
ComplLLattStr
) : ( ( ) (
V11
() )
set
) ))
=
x
: ( ( ) ( )
Element
of ( ( ) (
V11
() )
set
) ) ;
theorem
:: ROBBINS2:19
for
L
being ( ( non
empty
satisfying_DN_1
) ( non
empty
satisfying_DN_1
)
ComplLLattStr
)
for
x
,
y
being ( ( ) ( )
Element
of ( ( ) (
V11
() )
set
) ) holds
(
(
(
x
: ( ( ) ( )
Element
of ( ( ) (
V11
() )
set
) )
+
y
: ( ( ) ( )
Element
of ( ( ) (
V11
() )
set
) )
)
: ( ( ) ( )
M2
( the
U1
of
b
1
: ( ( non
empty
satisfying_DN_1
) ( non
empty
satisfying_DN_1
)
ComplLLattStr
) : ( ( ) (
V11
() )
set
) ))
`
)
: ( ( ) ( )
M2
( the
U1
of
b
1
: ( ( non
empty
satisfying_DN_1
) ( non
empty
satisfying_DN_1
)
ComplLLattStr
) : ( ( ) (
V11
() )
set
) ))
+
(
y
: ( ( ) ( )
Element
of ( ( ) (
V11
() )
set
) )
`
)
: ( ( ) ( )
M2
( the
U1
of
b
1
: ( ( non
empty
satisfying_DN_1
) ( non
empty
satisfying_DN_1
)
ComplLLattStr
) : ( ( ) (
V11
() )
set
) ))
)
: ( ( ) ( )
M2
( the
U1
of
b
1
: ( ( non
empty
satisfying_DN_1
) ( non
empty
satisfying_DN_1
)
ComplLLattStr
) : ( ( ) (
V11
() )
set
) ))
`
: ( ( ) ( )
M2
( the
U1
of
b
1
: ( ( non
empty
satisfying_DN_1
) ( non
empty
satisfying_DN_1
)
ComplLLattStr
) : ( ( ) (
V11
() )
set
) ))
=
y
: ( ( ) ( )
Element
of ( ( ) (
V11
() )
set
) ) ;
theorem
:: ROBBINS2:20
for
L
being ( ( non
empty
satisfying_DN_1
) ( non
empty
satisfying_DN_1
)
ComplLLattStr
)
for
x
,
y
being ( ( ) ( )
Element
of ( ( ) (
V11
() )
set
) ) holds
(
x
: ( ( ) ( )
Element
of ( ( ) (
V11
() )
set
) )
+
(
(
y
: ( ( ) ( )
Element
of ( ( ) (
V11
() )
set
) )
+
(
x
: ( ( ) ( )
Element
of ( ( ) (
V11
() )
set
) )
`
)
: ( ( ) ( )
M2
( the
U1
of
b
1
: ( ( non
empty
satisfying_DN_1
) ( non
empty
satisfying_DN_1
)
ComplLLattStr
) : ( ( ) (
V11
() )
set
) ))
)
: ( ( ) ( )
M2
( the
U1
of
b
1
: ( ( non
empty
satisfying_DN_1
) ( non
empty
satisfying_DN_1
)
ComplLLattStr
) : ( ( ) (
V11
() )
set
) ))
`
)
: ( ( ) ( )
M2
( the
U1
of
b
1
: ( ( non
empty
satisfying_DN_1
) ( non
empty
satisfying_DN_1
)
ComplLLattStr
) : ( ( ) (
V11
() )
set
) ))
)
: ( ( ) ( )
M2
( the
U1
of
b
1
: ( ( non
empty
satisfying_DN_1
) ( non
empty
satisfying_DN_1
)
ComplLLattStr
) : ( ( ) (
V11
() )
set
) ))
`
: ( ( ) ( )
M2
( the
U1
of
b
1
: ( ( non
empty
satisfying_DN_1
) ( non
empty
satisfying_DN_1
)
ComplLLattStr
) : ( ( ) (
V11
() )
set
) ))
=
x
: ( ( ) ( )
Element
of ( ( ) (
V11
() )
set
) )
`
: ( ( ) ( )
M2
( the
U1
of
b
1
: ( ( non
empty
satisfying_DN_1
) ( non
empty
satisfying_DN_1
)
ComplLLattStr
) : ( ( ) (
V11
() )
set
) )) ;
theorem
:: ROBBINS2:21
for
L
being ( ( non
empty
satisfying_DN_1
) ( non
empty
satisfying_DN_1
)
ComplLLattStr
)
for
x
being ( ( ) ( )
Element
of ( ( ) (
V11
() )
set
) ) holds
(
x
: ( ( ) ( )
Element
of ( ( ) (
V11
() )
set
) )
+
x
: ( ( ) ( )
Element
of ( ( ) (
V11
() )
set
) )
)
: ( ( ) ( )
M2
( the
U1
of
b
1
: ( ( non
empty
satisfying_DN_1
) ( non
empty
satisfying_DN_1
)
ComplLLattStr
) : ( ( ) (
V11
() )
set
) ))
`
: ( ( ) ( )
M2
( the
U1
of
b
1
: ( ( non
empty
satisfying_DN_1
) ( non
empty
satisfying_DN_1
)
ComplLLattStr
) : ( ( ) (
V11
() )
set
) ))
=
x
: ( ( ) ( )
Element
of ( ( ) (
V11
() )
set
) )
`
: ( ( ) ( )
M2
( the
U1
of
b
1
: ( ( non
empty
satisfying_DN_1
) ( non
empty
satisfying_DN_1
)
ComplLLattStr
) : ( ( ) (
V11
() )
set
) )) ;
theorem
:: ROBBINS2:22
for
L
being ( ( non
empty
satisfying_DN_1
) ( non
empty
satisfying_DN_1
)
ComplLLattStr
)
for
x
,
y
being ( ( ) ( )
Element
of ( ( ) (
V11
() )
set
) ) holds
(
(
(
(
(
x
: ( ( ) ( )
Element
of ( ( ) (
V11
() )
set
) )
+
y
: ( ( ) ( )
Element
of ( ( ) (
V11
() )
set
) )
)
: ( ( ) ( )
M2
( the
U1
of
b
1
: ( ( non
empty
satisfying_DN_1
) ( non
empty
satisfying_DN_1
)
ComplLLattStr
) : ( ( ) (
V11
() )
set
) ))
`
)
: ( ( ) ( )
M2
( the
U1
of
b
1
: ( ( non
empty
satisfying_DN_1
) ( non
empty
satisfying_DN_1
)
ComplLLattStr
) : ( ( ) (
V11
() )
set
) ))
+
x
: ( ( ) ( )
Element
of ( ( ) (
V11
() )
set
) )
)
: ( ( ) ( )
M2
( the
U1
of
b
1
: ( ( non
empty
satisfying_DN_1
) ( non
empty
satisfying_DN_1
)
ComplLLattStr
) : ( ( ) (
V11
() )
set
) ))
`
)
: ( ( ) ( )
M2
( the
U1
of
b
1
: ( ( non
empty
satisfying_DN_1
) ( non
empty
satisfying_DN_1
)
ComplLLattStr
) : ( ( ) (
V11
() )
set
) ))
+
y
: ( ( ) ( )
Element
of ( ( ) (
V11
() )
set
) )
)
: ( ( ) ( )
M2
( the
U1
of
b
1
: ( ( non
empty
satisfying_DN_1
) ( non
empty
satisfying_DN_1
)
ComplLLattStr
) : ( ( ) (
V11
() )
set
) ))
`
: ( ( ) ( )
M2
( the
U1
of
b
1
: ( ( non
empty
satisfying_DN_1
) ( non
empty
satisfying_DN_1
)
ComplLLattStr
) : ( ( ) (
V11
() )
set
) ))
=
y
: ( ( ) ( )
Element
of ( ( ) (
V11
() )
set
) )
`
: ( ( ) ( )
M2
( the
U1
of
b
1
: ( ( non
empty
satisfying_DN_1
) ( non
empty
satisfying_DN_1
)
ComplLLattStr
) : ( ( ) (
V11
() )
set
) )) ;
theorem
:: ROBBINS2:23
for
L
being ( ( non
empty
satisfying_DN_1
) ( non
empty
satisfying_DN_1
)
ComplLLattStr
)
for
x
being ( ( ) ( )
Element
of ( ( ) (
V11
() )
set
) ) holds
(
x
: ( ( ) ( )
Element
of ( ( ) (
V11
() )
set
) )
`
)
: ( ( ) ( )
M2
( the
U1
of
b
1
: ( ( non
empty
satisfying_DN_1
) ( non
empty
satisfying_DN_1
)
ComplLLattStr
) : ( ( ) (
V11
() )
set
) ))
`
: ( ( ) ( )
M2
( the
U1
of
b
1
: ( ( non
empty
satisfying_DN_1
) ( non
empty
satisfying_DN_1
)
ComplLLattStr
) : ( ( ) (
V11
() )
set
) ))
=
x
: ( ( ) ( )
Element
of ( ( ) (
V11
() )
set
) ) ;
theorem
:: ROBBINS2:24
for
L
being ( ( non
empty
satisfying_DN_1
) ( non
empty
satisfying_DN_1
)
ComplLLattStr
)
for
x
,
y
being ( ( ) ( )
Element
of ( ( ) (
V11
() )
set
) ) holds
(
(
(
(
x
: ( ( ) ( )
Element
of ( ( ) (
V11
() )
set
) )
+
y
: ( ( ) ( )
Element
of ( ( ) (
V11
() )
set
) )
)
: ( ( ) ( )
M2
( the
U1
of
b
1
: ( ( non
empty
satisfying_DN_1
) ( non
empty
satisfying_DN_1
)
ComplLLattStr
) : ( ( ) (
V11
() )
set
) ))
`
)
: ( ( ) ( )
M2
( the
U1
of
b
1
: ( ( non
empty
satisfying_DN_1
) ( non
empty
satisfying_DN_1
)
ComplLLattStr
) : ( ( ) (
V11
() )
set
) ))
+
x
: ( ( ) ( )
Element
of ( ( ) (
V11
() )
set
) )
)
: ( ( ) ( )
M2
( the
U1
of
b
1
: ( ( non
empty
satisfying_DN_1
) ( non
empty
satisfying_DN_1
)
ComplLLattStr
) : ( ( ) (
V11
() )
set
) ))
`
)
: ( ( ) ( )
M2
( the
U1
of
b
1
: ( ( non
empty
satisfying_DN_1
) ( non
empty
satisfying_DN_1
)
ComplLLattStr
) : ( ( ) (
V11
() )
set
) ))
+
y
: ( ( ) ( )
Element
of ( ( ) (
V11
() )
set
) ) : ( ( ) ( )
M2
( the
U1
of
b
1
: ( ( non
empty
satisfying_DN_1
) ( non
empty
satisfying_DN_1
)
ComplLLattStr
) : ( ( ) (
V11
() )
set
) ))
=
(
y
: ( ( ) ( )
Element
of ( ( ) (
V11
() )
set
) )
`
)
: ( ( ) ( )
M2
( the
U1
of
b
1
: ( ( non
empty
satisfying_DN_1
) ( non
empty
satisfying_DN_1
)
ComplLLattStr
) : ( ( ) (
V11
() )
set
) ))
`
: ( ( ) ( )
M2
( the
U1
of
b
1
: ( ( non
empty
satisfying_DN_1
) ( non
empty
satisfying_DN_1
)
ComplLLattStr
) : ( ( ) (
V11
() )
set
) )) ;
theorem
:: ROBBINS2:25
for
L
being ( ( non
empty
satisfying_DN_1
) ( non
empty
satisfying_DN_1
)
ComplLLattStr
)
for
x
,
y
being ( ( ) ( )
Element
of ( ( ) (
V11
() )
set
) ) holds
(
(
x
: ( ( ) ( )
Element
of ( ( ) (
V11
() )
set
) )
+
y
: ( ( ) ( )
Element
of ( ( ) (
V11
() )
set
) )
)
: ( ( ) ( )
M2
( the
U1
of
b
1
: ( ( non
empty
satisfying_DN_1
) ( non
empty
satisfying_DN_1
)
ComplLLattStr
) : ( ( ) (
V11
() )
set
) ))
`
)
: ( ( ) ( )
M2
( the
U1
of
b
1
: ( ( non
empty
satisfying_DN_1
) ( non
empty
satisfying_DN_1
)
ComplLLattStr
) : ( ( ) (
V11
() )
set
) ))
`
: ( ( ) ( )
M2
( the
U1
of
b
1
: ( ( non
empty
satisfying_DN_1
) ( non
empty
satisfying_DN_1
)
ComplLLattStr
) : ( ( ) (
V11
() )
set
) ))
=
y
: ( ( ) ( )
Element
of ( ( ) (
V11
() )
set
) )
+
x
: ( ( ) ( )
Element
of ( ( ) (
V11
() )
set
) ) : ( ( ) ( )
M2
( the
U1
of
b
1
: ( ( non
empty
satisfying_DN_1
) ( non
empty
satisfying_DN_1
)
ComplLLattStr
) : ( ( ) (
V11
() )
set
) )) ;
theorem
:: ROBBINS2:26
for
L
being ( ( non
empty
satisfying_DN_1
) ( non
empty
satisfying_DN_1
)
ComplLLattStr
)
for
x
,
y
,
z
being ( ( ) ( )
Element
of ( ( ) (
V11
() )
set
) ) holds
x
: ( ( ) ( )
Element
of ( ( ) (
V11
() )
set
) )
+
(
(
(
(
y
: ( ( ) ( )
Element
of ( ( ) (
V11
() )
set
) )
+
z
: ( ( ) ( )
Element
of ( ( ) (
V11
() )
set
) )
)
: ( ( ) ( )
M2
( the
U1
of
b
1
: ( ( non
empty
satisfying_DN_1
) ( non
empty
satisfying_DN_1
)
ComplLLattStr
) : ( ( ) (
V11
() )
set
) ))
`
)
: ( ( ) ( )
M2
( the
U1
of
b
1
: ( ( non
empty
satisfying_DN_1
) ( non
empty
satisfying_DN_1
)
ComplLLattStr
) : ( ( ) (
V11
() )
set
) ))
+
(
(
y
: ( ( ) ( )
Element
of ( ( ) (
V11
() )
set
) )
+
x
: ( ( ) ( )
Element
of ( ( ) (
V11
() )
set
) )
)
: ( ( ) ( )
M2
( the
U1
of
b
1
: ( ( non
empty
satisfying_DN_1
) ( non
empty
satisfying_DN_1
)
ComplLLattStr
) : ( ( ) (
V11
() )
set
) ))
`
)
: ( ( ) ( )
M2
( the
U1
of
b
1
: ( ( non
empty
satisfying_DN_1
) ( non
empty
satisfying_DN_1
)
ComplLLattStr
) : ( ( ) (
V11
() )
set
) ))
)
: ( ( ) ( )
M2
( the
U1
of
b
1
: ( ( non
empty
satisfying_DN_1
) ( non
empty
satisfying_DN_1
)
ComplLLattStr
) : ( ( ) (
V11
() )
set
) ))
`
)
: ( ( ) ( )
M2
( the
U1
of
b
1
: ( ( non
empty
satisfying_DN_1
) ( non
empty
satisfying_DN_1
)
ComplLLattStr
) : ( ( ) (
V11
() )
set
) )) : ( ( ) ( )
M2
( the
U1
of
b
1
: ( ( non
empty
satisfying_DN_1
) ( non
empty
satisfying_DN_1
)
ComplLLattStr
) : ( ( ) (
V11
() )
set
) ))
=
(
(
y
: ( ( ) ( )
Element
of ( ( ) (
V11
() )
set
) )
+
x
: ( ( ) ( )
Element
of ( ( ) (
V11
() )
set
) )
)
: ( ( ) ( )
M2
( the
U1
of
b
1
: ( ( non
empty
satisfying_DN_1
) ( non
empty
satisfying_DN_1
)
ComplLLattStr
) : ( ( ) (
V11
() )
set
) ))
`
)
: ( ( ) ( )
M2
( the
U1
of
b
1
: ( ( non
empty
satisfying_DN_1
) ( non
empty
satisfying_DN_1
)
ComplLLattStr
) : ( ( ) (
V11
() )
set
) ))
`
: ( ( ) ( )
M2
( the
U1
of
b
1
: ( ( non
empty
satisfying_DN_1
) ( non
empty
satisfying_DN_1
)
ComplLLattStr
) : ( ( ) (
V11
() )
set
) )) ;
theorem
:: ROBBINS2:27
for
L
being ( ( non
empty
satisfying_DN_1
) ( non
empty
satisfying_DN_1
)
ComplLLattStr
)
for
x
,
y
being ( ( ) ( )
Element
of ( ( ) (
V11
() )
set
) ) holds
x
: ( ( ) ( )
Element
of ( ( ) (
V11
() )
set
) )
+
y
: ( ( ) ( )
Element
of ( ( ) (
V11
() )
set
) ) : ( ( ) ( )
M2
( the
U1
of
b
1
: ( ( non
empty
satisfying_DN_1
) ( non
empty
satisfying_DN_1
)
ComplLLattStr
) : ( ( ) (
V11
() )
set
) ))
=
y
: ( ( ) ( )
Element
of ( ( ) (
V11
() )
set
) )
+
x
: ( ( ) ( )
Element
of ( ( ) (
V11
() )
set
) ) : ( ( ) ( )
M2
( the
U1
of
b
1
: ( ( non
empty
satisfying_DN_1
) ( non
empty
satisfying_DN_1
)
ComplLLattStr
) : ( ( ) (
V11
() )
set
) )) ;
registration
cluster
non
empty
satisfying_DN_1
->
non
empty
join-commutative
for ( ( ) ( )
ComplLLattStr
) ;
end;
theorem
:: ROBBINS2:28
for
L
being ( ( non
empty
satisfying_DN_1
) ( non
empty
join-commutative
satisfying_DN_1
)
ComplLLattStr
)
for
x
,
y
being ( ( ) ( )
Element
of ( ( ) (
V11
() )
set
) ) holds
(
(
(
(
x
: ( ( ) ( )
Element
of ( ( ) (
V11
() )
set
) )
+
y
: ( ( ) ( )
Element
of ( ( ) (
V11
() )
set
) )
)
: ( ( ) ( )
M2
( the
U1
of
b
1
: ( ( non
empty
satisfying_DN_1
) ( non
empty
join-commutative
satisfying_DN_1
)
ComplLLattStr
) : ( ( ) (
V11
() )
set
) ))
`
)
: ( ( ) ( )
M2
( the
U1
of
b
1
: ( ( non
empty
satisfying_DN_1
) ( non
empty
join-commutative
satisfying_DN_1
)
ComplLLattStr
) : ( ( ) (
V11
() )
set
) ))
+
x
: ( ( ) ( )
Element
of ( ( ) (
V11
() )
set
) )
)
: ( ( ) ( )
M2
( the
U1
of
b
1
: ( ( non
empty
satisfying_DN_1
) ( non
empty
join-commutative
satisfying_DN_1
)
ComplLLattStr
) : ( ( ) (
V11
() )
set
) ))
`
)
: ( ( ) ( )
M2
( the
U1
of
b
1
: ( ( non
empty
satisfying_DN_1
) ( non
empty
join-commutative
satisfying_DN_1
)
ComplLLattStr
) : ( ( ) (
V11
() )
set
) ))
+
y
: ( ( ) ( )
Element
of ( ( ) (
V11
() )
set
) ) : ( ( ) ( )
M2
( the
U1
of
b
1
: ( ( non
empty
satisfying_DN_1
) ( non
empty
join-commutative
satisfying_DN_1
)
ComplLLattStr
) : ( ( ) (
V11
() )
set
) ))
=
y
: ( ( ) ( )
Element
of ( ( ) (
V11
() )
set
) ) ;
theorem
:: ROBBINS2:29
for
L
being ( ( non
empty
satisfying_DN_1
) ( non
empty
join-commutative
satisfying_DN_1
)
ComplLLattStr
)
for
x
,
y
being ( ( ) ( )
Element
of ( ( ) (
V11
() )
set
) ) holds
(
(
(
(
x
: ( ( ) ( )
Element
of ( ( ) (
V11
() )
set
) )
+
y
: ( ( ) ( )
Element
of ( ( ) (
V11
() )
set
) )
)
: ( ( ) ( )
M2
( the
U1
of
b
1
: ( ( non
empty
satisfying_DN_1
) ( non
empty
join-commutative
satisfying_DN_1
)
ComplLLattStr
) : ( ( ) (
V11
() )
set
) ))
`
)
: ( ( ) ( )
M2
( the
U1
of
b
1
: ( ( non
empty
satisfying_DN_1
) ( non
empty
join-commutative
satisfying_DN_1
)
ComplLLattStr
) : ( ( ) (
V11
() )
set
) ))
+
y
: ( ( ) ( )
Element
of ( ( ) (
V11
() )
set
) )
)
: ( ( ) ( )
M2
( the
U1
of
b
1
: ( ( non
empty
satisfying_DN_1
) ( non
empty
join-commutative
satisfying_DN_1
)
ComplLLattStr
) : ( ( ) (
V11
() )
set
) ))
`
)
: ( ( ) ( )
M2
( the
U1
of
b
1
: ( ( non
empty
satisfying_DN_1
) ( non
empty
join-commutative
satisfying_DN_1
)
ComplLLattStr
) : ( ( ) (
V11
() )
set
) ))
+
x
: ( ( ) ( )
Element
of ( ( ) (
V11
() )
set
) ) : ( ( ) ( )
M2
( the
U1
of
b
1
: ( ( non
empty
satisfying_DN_1
) ( non
empty
join-commutative
satisfying_DN_1
)
ComplLLattStr
) : ( ( ) (
V11
() )
set
) ))
=
x
: ( ( ) ( )
Element
of ( ( ) (
V11
() )
set
) ) ;
theorem
:: ROBBINS2:30
for
L
being ( ( non
empty
satisfying_DN_1
) ( non
empty
join-commutative
satisfying_DN_1
)
ComplLLattStr
)
for
x
,
y
being ( ( ) ( )
Element
of ( ( ) (
V11
() )
set
) ) holds
x
: ( ( ) ( )
Element
of ( ( ) (
V11
() )
set
) )
+
(
(
(
(
y
: ( ( ) ( )
Element
of ( ( ) (
V11
() )
set
) )
+
x
: ( ( ) ( )
Element
of ( ( ) (
V11
() )
set
) )
)
: ( ( ) ( )
M2
( the
U1
of
b
1
: ( ( non
empty
satisfying_DN_1
) ( non
empty
join-commutative
satisfying_DN_1
)
ComplLLattStr
) : ( ( ) (
V11
() )
set
) ))
`
)
: ( ( ) ( )
M2
( the
U1
of
b
1
: ( ( non
empty
satisfying_DN_1
) ( non
empty
join-commutative
satisfying_DN_1
)
ComplLLattStr
) : ( ( ) (
V11
() )
set
) ))
+
y
: ( ( ) ( )
Element
of ( ( ) (
V11
() )
set
) )
)
: ( ( ) ( )
M2
( the
U1
of
b
1
: ( ( non
empty
satisfying_DN_1
) ( non
empty
join-commutative
satisfying_DN_1
)
ComplLLattStr
) : ( ( ) (
V11
() )
set
) ))
`
)
: ( ( ) ( )
M2
( the
U1
of
b
1
: ( ( non
empty
satisfying_DN_1
) ( non
empty
join-commutative
satisfying_DN_1
)
ComplLLattStr
) : ( ( ) (
V11
() )
set
) )) : ( ( ) ( )
M2
( the
U1
of
b
1
: ( ( non
empty
satisfying_DN_1
) ( non
empty
join-commutative
satisfying_DN_1
)
ComplLLattStr
) : ( ( ) (
V11
() )
set
) ))
=
x
: ( ( ) ( )
Element
of ( ( ) (
V11
() )
set
) ) ;
theorem
:: ROBBINS2:31
for
L
being ( ( non
empty
satisfying_DN_1
) ( non
empty
join-commutative
satisfying_DN_1
)
ComplLLattStr
)
for
x
,
y
being ( ( ) ( )
Element
of ( ( ) (
V11
() )
set
) ) holds
(
(
x
: ( ( ) ( )
Element
of ( ( ) (
V11
() )
set
) )
+
(
y
: ( ( ) ( )
Element
of ( ( ) (
V11
() )
set
) )
`
)
: ( ( ) ( )
M2
( the
U1
of
b
1
: ( ( non
empty
satisfying_DN_1
) ( non
empty
join-commutative
satisfying_DN_1
)
ComplLLattStr
) : ( ( ) (
V11
() )
set
) ))
)
: ( ( ) ( )
M2
( the
U1
of
b
1
: ( ( non
empty
satisfying_DN_1
) ( non
empty
join-commutative
satisfying_DN_1
)
ComplLLattStr
) : ( ( ) (
V11
() )
set
) ))
`
)
: ( ( ) ( )
M2
( the
U1
of
b
1
: ( ( non
empty
satisfying_DN_1
) ( non
empty
join-commutative
satisfying_DN_1
)
ComplLLattStr
) : ( ( ) (
V11
() )
set
) ))
+
(
(
(
y
: ( ( ) ( )
Element
of ( ( ) (
V11
() )
set
) )
`
)
: ( ( ) ( )
M2
( the
U1
of
b
1
: ( ( non
empty
satisfying_DN_1
) ( non
empty
join-commutative
satisfying_DN_1
)
ComplLLattStr
) : ( ( ) (
V11
() )
set
) ))
+
y
: ( ( ) ( )
Element
of ( ( ) (
V11
() )
set
) )
)
: ( ( ) ( )
M2
( the
U1
of
b
1
: ( ( non
empty
satisfying_DN_1
) ( non
empty
join-commutative
satisfying_DN_1
)
ComplLLattStr
) : ( ( ) (
V11
() )
set
) ))
`
)
: ( ( ) ( )
M2
( the
U1
of
b
1
: ( ( non
empty
satisfying_DN_1
) ( non
empty
join-commutative
satisfying_DN_1
)
ComplLLattStr
) : ( ( ) (
V11
() )
set
) )) : ( ( ) ( )
M2
( the
U1
of
b
1
: ( ( non
empty
satisfying_DN_1
) ( non
empty
join-commutative
satisfying_DN_1
)
ComplLLattStr
) : ( ( ) (
V11
() )
set
) ))
=
(
x
: ( ( ) ( )
Element
of ( ( ) (
V11
() )
set
) )
+
(
y
: ( ( ) ( )
Element
of ( ( ) (
V11
() )
set
) )
`
)
: ( ( ) ( )
M2
( the
U1
of
b
1
: ( ( non
empty
satisfying_DN_1
) ( non
empty
join-commutative
satisfying_DN_1
)
ComplLLattStr
) : ( ( ) (
V11
() )
set
) ))
)
: ( ( ) ( )
M2
( the
U1
of
b
1
: ( ( non
empty
satisfying_DN_1
) ( non
empty
join-commutative
satisfying_DN_1
)
ComplLLattStr
) : ( ( ) (
V11
() )
set
) ))
`
: ( ( ) ( )
M2
( the
U1
of
b
1
: ( ( non
empty
satisfying_DN_1
) ( non
empty
join-commutative
satisfying_DN_1
)
ComplLLattStr
) : ( ( ) (
V11
() )
set
) )) ;
theorem
:: ROBBINS2:32
for
L
being ( ( non
empty
satisfying_DN_1
) ( non
empty
join-commutative
satisfying_DN_1
)
ComplLLattStr
)
for
x
,
y
being ( ( ) ( )
Element
of ( ( ) (
V11
() )
set
) ) holds
(
(
x
: ( ( ) ( )
Element
of ( ( ) (
V11
() )
set
) )
+
y
: ( ( ) ( )
Element
of ( ( ) (
V11
() )
set
) )
)
: ( ( ) ( )
M2
( the
U1
of
b
1
: ( ( non
empty
satisfying_DN_1
) ( non
empty
join-commutative
satisfying_DN_1
)
ComplLLattStr
) : ( ( ) (
V11
() )
set
) ))
`
)
: ( ( ) ( )
M2
( the
U1
of
b
1
: ( ( non
empty
satisfying_DN_1
) ( non
empty
join-commutative
satisfying_DN_1
)
ComplLLattStr
) : ( ( ) (
V11
() )
set
) ))
+
(
(
y
: ( ( ) ( )
Element
of ( ( ) (
V11
() )
set
) )
+
(
y
: ( ( ) ( )
Element
of ( ( ) (
V11
() )
set
) )
`
)
: ( ( ) ( )
M2
( the
U1
of
b
1
: ( ( non
empty
satisfying_DN_1
) ( non
empty
join-commutative
satisfying_DN_1
)
ComplLLattStr
) : ( ( ) (
V11
() )
set
) ))
)
: ( ( ) ( )
M2
( the
U1
of
b
1
: ( ( non
empty
satisfying_DN_1
) ( non
empty
join-commutative
satisfying_DN_1
)
ComplLLattStr
) : ( ( ) (
V11
() )
set
) ))
`
)
: ( ( ) ( )
M2
( the
U1
of
b
1
: ( ( non
empty
satisfying_DN_1
) ( non
empty
join-commutative
satisfying_DN_1
)
ComplLLattStr
) : ( ( ) (
V11
() )
set
) )) : ( ( ) ( )
M2
( the
U1
of
b
1
: ( ( non
empty
satisfying_DN_1
) ( non
empty
join-commutative
satisfying_DN_1
)
ComplLLattStr
) : ( ( ) (
V11
() )
set
) ))
=
(
x
: ( ( ) ( )
Element
of ( ( ) (
V11
() )
set
) )
+
y
: ( ( ) ( )
Element
of ( ( ) (
V11
() )
set
) )
)
: ( ( ) ( )
M2
( the
U1
of
b
1
: ( ( non
empty
satisfying_DN_1
) ( non
empty
join-commutative
satisfying_DN_1
)
ComplLLattStr
) : ( ( ) (
V11
() )
set
) ))
`
: ( ( ) ( )
M2
( the
U1
of
b
1
: ( ( non
empty
satisfying_DN_1
) ( non
empty
join-commutative
satisfying_DN_1
)
ComplLLattStr
) : ( ( ) (
V11
() )
set
) )) ;
theorem
:: ROBBINS2:33
for
L
being ( ( non
empty
satisfying_DN_1
) ( non
empty
join-commutative
satisfying_DN_1
)
ComplLLattStr
)
for
x
,
y
being ( ( ) ( )
Element
of ( ( ) (
V11
() )
set
) ) holds
(
(
x
: ( ( ) ( )
Element
of ( ( ) (
V11
() )
set
) )
+
y
: ( ( ) ( )
Element
of ( ( ) (
V11
() )
set
) )
)
: ( ( ) ( )
M2
( the
U1
of
b
1
: ( ( non
empty
satisfying_DN_1
) ( non
empty
join-commutative
satisfying_DN_1
)
ComplLLattStr
) : ( ( ) (
V11
() )
set
) ))
`
)
: ( ( ) ( )
M2
( the
U1
of
b
1
: ( ( non
empty
satisfying_DN_1
) ( non
empty
join-commutative
satisfying_DN_1
)
ComplLLattStr
) : ( ( ) (
V11
() )
set
) ))
+
(
(
(
y
: ( ( ) ( )
Element
of ( ( ) (
V11
() )
set
) )
`
)
: ( ( ) ( )
M2
( the
U1
of
b
1
: ( ( non
empty
satisfying_DN_1
) ( non
empty
join-commutative
satisfying_DN_1
)
ComplLLattStr
) : ( ( ) (
V11
() )
set
) ))
+
y
: ( ( ) ( )
Element
of ( ( ) (
V11
() )
set
) )
)
: ( ( ) ( )
M2
( the
U1
of
b
1
: ( ( non
empty
satisfying_DN_1
) ( non
empty
join-commutative
satisfying_DN_1
)
ComplLLattStr
) : ( ( ) (
V11
() )
set
) ))
`
)
: ( ( ) ( )
M2
( the
U1
of
b
1
: ( ( non
empty
satisfying_DN_1
) ( non
empty
join-commutative
satisfying_DN_1
)
ComplLLattStr
) : ( ( ) (
V11
() )
set
) )) : ( ( ) ( )
M2
( the
U1
of
b
1
: ( ( non
empty
satisfying_DN_1
) ( non
empty
join-commutative
satisfying_DN_1
)
ComplLLattStr
) : ( ( ) (
V11
() )
set
) ))
=
(
x
: ( ( ) ( )
Element
of ( ( ) (
V11
() )
set
) )
+
y
: ( ( ) ( )
Element
of ( ( ) (
V11
() )
set
) )
)
: ( ( ) ( )
M2
( the
U1
of
b
1
: ( ( non
empty
satisfying_DN_1
) ( non
empty
join-commutative
satisfying_DN_1
)
ComplLLattStr
) : ( ( ) (
V11
() )
set
) ))
`
: ( ( ) ( )
M2
( the
U1
of
b
1
: ( ( non
empty
satisfying_DN_1
) ( non
empty
join-commutative
satisfying_DN_1
)
ComplLLattStr
) : ( ( ) (
V11
() )
set
) )) ;
theorem
:: ROBBINS2:34
for
L
being ( ( non
empty
satisfying_DN_1
) ( non
empty
join-commutative
satisfying_DN_1
)
ComplLLattStr
)
for
x
,
y
being ( ( ) ( )
Element
of ( ( ) (
V11
() )
set
) ) holds
(
(
(
(
x
: ( ( ) ( )
Element
of ( ( ) (
V11
() )
set
) )
+
(
y
: ( ( ) ( )
Element
of ( ( ) (
V11
() )
set
) )
`
)
: ( ( ) ( )
M2
( the
U1
of
b
1
: ( ( non
empty
satisfying_DN_1
) ( non
empty
join-commutative
satisfying_DN_1
)
ComplLLattStr
) : ( ( ) (
V11
() )
set
) ))
)
: ( ( ) ( )
M2
( the
U1
of
b
1
: ( ( non
empty
satisfying_DN_1
) ( non
empty
join-commutative
satisfying_DN_1
)
ComplLLattStr
) : ( ( ) (
V11
() )
set
) ))
`
)
: ( ( ) ( )
M2
( the
U1
of
b
1
: ( ( non
empty
satisfying_DN_1
) ( non
empty
join-commutative
satisfying_DN_1
)
ComplLLattStr
) : ( ( ) (
V11
() )
set
) ))
`
)
: ( ( ) ( )
M2
( the
U1
of
b
1
: ( ( non
empty
satisfying_DN_1
) ( non
empty
join-commutative
satisfying_DN_1
)
ComplLLattStr
) : ( ( ) (
V11
() )
set
) ))
+
y
: ( ( ) ( )
Element
of ( ( ) (
V11
() )
set
) )
)
: ( ( ) ( )
M2
( the
U1
of
b
1
: ( ( non
empty
satisfying_DN_1
) ( non
empty
join-commutative
satisfying_DN_1
)
ComplLLattStr
) : ( ( ) (
V11
() )
set
) ))
`
: ( ( ) ( )
M2
( the
U1
of
b
1
: ( ( non
empty
satisfying_DN_1
) ( non
empty
join-commutative
satisfying_DN_1
)
ComplLLattStr
) : ( ( ) (
V11
() )
set
) ))
=
(
(
y
: ( ( ) ( )
Element
of ( ( ) (
V11
() )
set
) )
`
)
: ( ( ) ( )
M2
( the
U1
of
b
1
: ( ( non
empty
satisfying_DN_1
) ( non
empty
join-commutative
satisfying_DN_1
)
ComplLLattStr
) : ( ( ) (
V11
() )
set
) ))
+
y
: ( ( ) ( )
Element
of ( ( ) (
V11
() )
set
) )
)
: ( ( ) ( )
M2
( the
U1
of
b
1
: ( ( non
empty
satisfying_DN_1
) ( non
empty
join-commutative
satisfying_DN_1
)
ComplLLattStr
) : ( ( ) (
V11
() )
set
) ))
`
: ( ( ) ( )
M2
( the
U1
of
b
1
: ( ( non
empty
satisfying_DN_1
) ( non
empty
join-commutative
satisfying_DN_1
)
ComplLLattStr
) : ( ( ) (
V11
() )
set
) )) ;
theorem
:: ROBBINS2:35
for
L
being ( ( non
empty
satisfying_DN_1
) ( non
empty
join-commutative
satisfying_DN_1
)
ComplLLattStr
)
for
x
,
y
being ( ( ) ( )
Element
of ( ( ) (
V11
() )
set
) ) holds
(
(
x
: ( ( ) ( )
Element
of ( ( ) (
V11
() )
set
) )
+
(
y
: ( ( ) ( )
Element
of ( ( ) (
V11
() )
set
) )
`
)
: ( ( ) ( )
M2
( the
U1
of
b
1
: ( ( non
empty
satisfying_DN_1
) ( non
empty
join-commutative
satisfying_DN_1
)
ComplLLattStr
) : ( ( ) (
V11
() )
set
) ))
)
: ( ( ) ( )
M2
( the
U1
of
b
1
: ( ( non
empty
satisfying_DN_1
) ( non
empty
join-commutative
satisfying_DN_1
)
ComplLLattStr
) : ( ( ) (
V11
() )
set
) ))
+
y
: ( ( ) ( )
Element
of ( ( ) (
V11
() )
set
) )
)
: ( ( ) ( )
M2
( the
U1
of
b
1
: ( ( non
empty
satisfying_DN_1
) ( non
empty
join-commutative
satisfying_DN_1
)
ComplLLattStr
) : ( ( ) (
V11
() )
set
) ))
`
: ( ( ) ( )
M2
( the
U1
of
b
1
: ( ( non
empty
satisfying_DN_1
) ( non
empty
join-commutative
satisfying_DN_1
)
ComplLLattStr
) : ( ( ) (
V11
() )
set
) ))
=
(
(
y
: ( ( ) ( )
Element
of ( ( ) (
V11
() )
set
) )
`
)
: ( ( ) ( )
M2
( the
U1
of
b
1
: ( ( non
empty
satisfying_DN_1
) ( non
empty
join-commutative
satisfying_DN_1
)
ComplLLattStr
) : ( ( ) (
V11
() )
set
) ))
+
y
: ( ( ) ( )
Element
of ( ( ) (
V11
() )
set
) )
)
: ( ( ) ( )
M2
( the
U1
of
b
1
: ( ( non
empty
satisfying_DN_1
) ( non
empty
join-commutative
satisfying_DN_1
)
ComplLLattStr
) : ( ( ) (
V11
() )
set
) ))
`
: ( ( ) ( )
M2
( the
U1
of
b
1
: ( ( non
empty
satisfying_DN_1
) ( non
empty
join-commutative
satisfying_DN_1
)
ComplLLattStr
) : ( ( ) (
V11
() )
set
) )) ;
theorem
:: ROBBINS2:36
for
L
being ( ( non
empty
satisfying_DN_1
) ( non
empty
join-commutative
satisfying_DN_1
)
ComplLLattStr
)
for
x
,
y
,
z
being ( ( ) ( )
Element
of ( ( ) (
V11
() )
set
) ) holds
(
(
(
(
(
(
x
: ( ( ) ( )
Element
of ( ( ) (
V11
() )
set
) )
+
(
y
: ( ( ) ( )
Element
of ( ( ) (
V11
() )
set
) )
`
)
: ( ( ) ( )
M2
( the
U1
of
b
1
: ( ( non
empty
satisfying_DN_1
) ( non
empty
join-commutative
satisfying_DN_1
)
ComplLLattStr
) : ( ( ) (
V11
() )
set
) ))
)
: ( ( ) ( )
M2
( the
U1
of
b
1
: ( ( non
empty
satisfying_DN_1
) ( non
empty
join-commutative
satisfying_DN_1
)
ComplLLattStr
) : ( ( ) (
V11
() )
set
) ))
+
z
: ( ( ) ( )
Element
of ( ( ) (
V11
() )
set
) )
)
: ( ( ) ( )
M2
( the
U1
of
b
1
: ( ( non
empty
satisfying_DN_1
) ( non
empty
join-commutative
satisfying_DN_1
)
ComplLLattStr
) : ( ( ) (
V11
() )
set
) ))
`
)
: ( ( ) ( )
M2
( the
U1
of
b
1
: ( ( non
empty
satisfying_DN_1
) ( non
empty
join-commutative
satisfying_DN_1
)
ComplLLattStr
) : ( ( ) (
V11
() )
set
) ))
+
y
: ( ( ) ( )
Element
of ( ( ) (
V11
() )
set
) )
)
: ( ( ) ( )
M2
( the
U1
of
b
1
: ( ( non
empty
satisfying_DN_1
) ( non
empty
join-commutative
satisfying_DN_1
)
ComplLLattStr
) : ( ( ) (
V11
() )
set
) ))
`
)
: ( ( ) ( )
M2
( the
U1
of
b
1
: ( ( non
empty
satisfying_DN_1
) ( non
empty
join-commutative
satisfying_DN_1
)
ComplLLattStr
) : ( ( ) (
V11
() )
set
) ))
+
(
(
(
y
: ( ( ) ( )
Element
of ( ( ) (
V11
() )
set
) )
`
)
: ( ( ) ( )
M2
( the
U1
of
b
1
: ( ( non
empty
satisfying_DN_1
) ( non
empty
join-commutative
satisfying_DN_1
)
ComplLLattStr
) : ( ( ) (
V11
() )
set
) ))
+
y
: ( ( ) ( )
Element
of ( ( ) (
V11
() )
set
) )
)
: ( ( ) ( )
M2
( the
U1
of
b
1
: ( ( non
empty
satisfying_DN_1
) ( non
empty
join-commutative
satisfying_DN_1
)
ComplLLattStr
) : ( ( ) (
V11
() )
set
) ))
`
)
: ( ( ) ( )
M2
( the
U1
of
b
1
: ( ( non
empty
satisfying_DN_1
) ( non
empty
join-commutative
satisfying_DN_1
)
ComplLLattStr
) : ( ( ) (
V11
() )
set
) ))
)
: ( ( ) ( )
M2
( the
U1
of
b
1
: ( ( non
empty
satisfying_DN_1
) ( non
empty
join-commutative
satisfying_DN_1
)
ComplLLattStr
) : ( ( ) (
V11
() )
set
) ))
`
: ( ( ) ( )
M2
( the
U1
of
b
1
: ( ( non
empty
satisfying_DN_1
) ( non
empty
join-commutative
satisfying_DN_1
)
ComplLLattStr
) : ( ( ) (
V11
() )
set
) ))
=
y
: ( ( ) ( )
Element
of ( ( ) (
V11
() )
set
) ) ;
theorem
:: ROBBINS2:37
for
L
being ( ( non
empty
satisfying_DN_1
) ( non
empty
join-commutative
satisfying_DN_1
)
ComplLLattStr
)
for
x
,
y
,
z
being ( ( ) ( )
Element
of ( ( ) (
V11
() )
set
) ) holds
x
: ( ( ) ( )
Element
of ( ( ) (
V11
() )
set
) )
+
(
(
(
(
y
: ( ( ) ( )
Element
of ( ( ) (
V11
() )
set
) )
+
z
: ( ( ) ( )
Element
of ( ( ) (
V11
() )
set
) )
)
: ( ( ) ( )
M2
( the
U1
of
b
1
: ( ( non
empty
satisfying_DN_1
) ( non
empty
join-commutative
satisfying_DN_1
)
ComplLLattStr
) : ( ( ) (
V11
() )
set
) ))
`
)
: ( ( ) ( )
M2
( the
U1
of
b
1
: ( ( non
empty
satisfying_DN_1
) ( non
empty
join-commutative
satisfying_DN_1
)
ComplLLattStr
) : ( ( ) (
V11
() )
set
) ))
+
(
(
y
: ( ( ) ( )
Element
of ( ( ) (
V11
() )
set
) )
+
x
: ( ( ) ( )
Element
of ( ( ) (
V11
() )
set
) )
)
: ( ( ) ( )
M2
( the
U1
of
b
1
: ( ( non
empty
satisfying_DN_1
) ( non
empty
join-commutative
satisfying_DN_1
)
ComplLLattStr
) : ( ( ) (
V11
() )
set
) ))
`
)
: ( ( ) ( )
M2
( the
U1
of
b
1
: ( ( non
empty
satisfying_DN_1
) ( non
empty
join-commutative
satisfying_DN_1
)
ComplLLattStr
) : ( ( ) (
V11
() )
set
) ))
)
: ( ( ) ( )
M2
( the
U1
of
b
1
: ( ( non
empty
satisfying_DN_1
) ( non
empty
join-commutative
satisfying_DN_1
)
ComplLLattStr
) : ( ( ) (
V11
() )
set
) ))
`
)
: ( ( ) ( )
M2
( the
U1
of
b
1
: ( ( non
empty
satisfying_DN_1
) ( non
empty
join-commutative
satisfying_DN_1
)
ComplLLattStr
) : ( ( ) (
V11
() )
set
) )) : ( ( ) ( )
M2
( the
U1
of
b
1
: ( ( non
empty
satisfying_DN_1
) ( non
empty
join-commutative
satisfying_DN_1
)
ComplLLattStr
) : ( ( ) (
V11
() )
set
) ))
=
y
: ( ( ) ( )
Element
of ( ( ) (
V11
() )
set
) )
+
x
: ( ( ) ( )
Element
of ( ( ) (
V11
() )
set
) ) : ( ( ) ( )
M2
( the
U1
of
b
1
: ( ( non
empty
satisfying_DN_1
) ( non
empty
join-commutative
satisfying_DN_1
)
ComplLLattStr
) : ( ( ) (
V11
() )
set
) )) ;
theorem
:: ROBBINS2:38
for
L
being ( ( non
empty
satisfying_DN_1
) ( non
empty
join-commutative
satisfying_DN_1
)
ComplLLattStr
)
for
x
,
y
,
z
being ( ( ) ( )
Element
of ( ( ) (
V11
() )
set
) ) holds
x
: ( ( ) ( )
Element
of ( ( ) (
V11
() )
set
) )
+
(
(
y
: ( ( ) ( )
Element
of ( ( ) (
V11
() )
set
) )
+
(
(
(
(
z
: ( ( ) ( )
Element
of ( ( ) (
V11
() )
set
) )
+
y
: ( ( ) ( )
Element
of ( ( ) (
V11
() )
set
) )
)
: ( ( ) ( )
M2
( the
U1
of
b
1
: ( ( non
empty
satisfying_DN_1
) ( non
empty
join-commutative
satisfying_DN_1
)
ComplLLattStr
) : ( ( ) (
V11
() )
set
) ))
`
)
: ( ( ) ( )
M2
( the
U1
of
b
1
: ( ( non
empty
satisfying_DN_1
) ( non
empty
join-commutative
satisfying_DN_1
)
ComplLLattStr
) : ( ( ) (
V11
() )
set
) ))
+
x
: ( ( ) ( )
Element
of ( ( ) (
V11
() )
set
) )
)
: ( ( ) ( )
M2
( the
U1
of
b
1
: ( ( non
empty
satisfying_DN_1
) ( non
empty
join-commutative
satisfying_DN_1
)
ComplLLattStr
) : ( ( ) (
V11
() )
set
) ))
`
)
: ( ( ) ( )
M2
( the
U1
of
b
1
: ( ( non
empty
satisfying_DN_1
) ( non
empty
join-commutative
satisfying_DN_1
)
ComplLLattStr
) : ( ( ) (
V11
() )
set
) ))
)
: ( ( ) ( )
M2
( the
U1
of
b
1
: ( ( non
empty
satisfying_DN_1
) ( non
empty
join-commutative
satisfying_DN_1
)
ComplLLattStr
) : ( ( ) (
V11
() )
set
) ))
`
)
: ( ( ) ( )
M2
( the
U1
of
b
1
: ( ( non
empty
satisfying_DN_1
) ( non
empty
join-commutative
satisfying_DN_1
)
ComplLLattStr
) : ( ( ) (
V11
() )
set
) )) : ( ( ) ( )
M2
( the
U1
of
b
1
: ( ( non
empty
satisfying_DN_1
) ( non
empty
join-commutative
satisfying_DN_1
)
ComplLLattStr
) : ( ( ) (
V11
() )
set
) ))
=
(
(
z
: ( ( ) ( )
Element
of ( ( ) (
V11
() )
set
) )
+
y
: ( ( ) ( )
Element
of ( ( ) (
V11
() )
set
) )
)
: ( ( ) ( )
M2
( the
U1
of
b
1
: ( ( non
empty
satisfying_DN_1
) ( non
empty
join-commutative
satisfying_DN_1
)
ComplLLattStr
) : ( ( ) (
V11
() )
set
) ))
`
)
: ( ( ) ( )
M2
( the
U1
of
b
1
: ( ( non
empty
satisfying_DN_1
) ( non
empty
join-commutative
satisfying_DN_1
)
ComplLLattStr
) : ( ( ) (
V11
() )
set
) ))
+
x
: ( ( ) ( )
Element
of ( ( ) (
V11
() )
set
) ) : ( ( ) ( )
M2
( the
U1
of
b
1
: ( ( non
empty
satisfying_DN_1
) ( non
empty
join-commutative
satisfying_DN_1
)
ComplLLattStr
) : ( ( ) (
V11
() )
set
) )) ;
theorem
:: ROBBINS2:39
for
L
being ( ( non
empty
satisfying_DN_1
) ( non
empty
join-commutative
satisfying_DN_1
)
ComplLLattStr
)
for
x
,
y
,
z
being ( ( ) ( )
Element
of ( ( ) (
V11
() )
set
) ) holds
x
: ( ( ) ( )
Element
of ( ( ) (
V11
() )
set
) )
+
(
(
(
(
y
: ( ( ) ( )
Element
of ( ( ) (
V11
() )
set
) )
+
x
: ( ( ) ( )
Element
of ( ( ) (
V11
() )
set
) )
)
: ( ( ) ( )
M2
( the
U1
of
b
1
: ( ( non
empty
satisfying_DN_1
) ( non
empty
join-commutative
satisfying_DN_1
)
ComplLLattStr
) : ( ( ) (
V11
() )
set
) ))
`
)
: ( ( ) ( )
M2
( the
U1
of
b
1
: ( ( non
empty
satisfying_DN_1
) ( non
empty
join-commutative
satisfying_DN_1
)
ComplLLattStr
) : ( ( ) (
V11
() )
set
) ))
+
(
(
y
: ( ( ) ( )
Element
of ( ( ) (
V11
() )
set
) )
+
z
: ( ( ) ( )
Element
of ( ( ) (
V11
() )
set
) )
)
: ( ( ) ( )
M2
( the
U1
of
b
1
: ( ( non
empty
satisfying_DN_1
) ( non
empty
join-commutative
satisfying_DN_1
)
ComplLLattStr
) : ( ( ) (
V11
() )
set
) ))
`
)
: ( ( ) ( )
M2
( the
U1
of
b
1
: ( ( non
empty
satisfying_DN_1
) ( non
empty
join-commutative
satisfying_DN_1
)
ComplLLattStr
) : ( ( ) (
V11
() )
set
) ))
)
: ( ( ) ( )
M2
( the
U1
of
b
1
: ( ( non
empty
satisfying_DN_1
) ( non
empty
join-commutative
satisfying_DN_1
)
ComplLLattStr
) : ( ( ) (
V11
() )
set
) ))
`
)
: ( ( ) ( )
M2
( the
U1
of
b
1
: ( ( non
empty
satisfying_DN_1
) ( non
empty
join-commutative
satisfying_DN_1
)
ComplLLattStr
) : ( ( ) (
V11
() )
set
) )) : ( ( ) ( )
M2
( the
U1
of
b
1
: ( ( non
empty
satisfying_DN_1
) ( non
empty
join-commutative
satisfying_DN_1
)
ComplLLattStr
) : ( ( ) (
V11
() )
set
) ))
=
y
: ( ( ) ( )
Element
of ( ( ) (
V11
() )
set
) )
+
x
: ( ( ) ( )
Element
of ( ( ) (
V11
() )
set
) ) : ( ( ) ( )
M2
( the
U1
of
b
1
: ( ( non
empty
satisfying_DN_1
) ( non
empty
join-commutative
satisfying_DN_1
)
ComplLLattStr
) : ( ( ) (
V11
() )
set
) )) ;
theorem
:: ROBBINS2:40
for
L
being ( ( non
empty
satisfying_DN_1
) ( non
empty
join-commutative
satisfying_DN_1
)
ComplLLattStr
)
for
x
,
y
,
z
being ( ( ) ( )
Element
of ( ( ) (
V11
() )
set
) ) holds
(
(
(
(
x
: ( ( ) ( )
Element
of ( ( ) (
V11
() )
set
) )
+
y
: ( ( ) ( )
Element
of ( ( ) (
V11
() )
set
) )
)
: ( ( ) ( )
M2
( the
U1
of
b
1
: ( ( non
empty
satisfying_DN_1
) ( non
empty
join-commutative
satisfying_DN_1
)
ComplLLattStr
) : ( ( ) (
V11
() )
set
) ))
`
)
: ( ( ) ( )
M2
( the
U1
of
b
1
: ( ( non
empty
satisfying_DN_1
) ( non
empty
join-commutative
satisfying_DN_1
)
ComplLLattStr
) : ( ( ) (
V11
() )
set
) ))
+
(
(
(
(
x
: ( ( ) ( )
Element
of ( ( ) (
V11
() )
set
) )
+
y
: ( ( ) ( )
Element
of ( ( ) (
V11
() )
set
) )
)
: ( ( ) ( )
M2
( the
U1
of
b
1
: ( ( non
empty
satisfying_DN_1
) ( non
empty
join-commutative
satisfying_DN_1
)
ComplLLattStr
) : ( ( ) (
V11
() )
set
) ))
`
)
: ( ( ) ( )
M2
( the
U1
of
b
1
: ( ( non
empty
satisfying_DN_1
) ( non
empty
join-commutative
satisfying_DN_1
)
ComplLLattStr
) : ( ( ) (
V11
() )
set
) ))
+
(
(
x
: ( ( ) ( )
Element
of ( ( ) (
V11
() )
set
) )
+
z
: ( ( ) ( )
Element
of ( ( ) (
V11
() )
set
) )
)
: ( ( ) ( )
M2
( the
U1
of
b
1
: ( ( non
empty
satisfying_DN_1
) ( non
empty
join-commutative
satisfying_DN_1
)
ComplLLattStr
) : ( ( ) (
V11
() )
set
) ))
`
)
: ( ( ) ( )
M2
( the
U1
of
b
1
: ( ( non
empty
satisfying_DN_1
) ( non
empty
join-commutative
satisfying_DN_1
)
ComplLLattStr
) : ( ( ) (
V11
() )
set
) ))
)
: ( ( ) ( )
M2
( the
U1
of
b
1
: ( ( non
empty
satisfying_DN_1
) ( non
empty
join-commutative
satisfying_DN_1
)
ComplLLattStr
) : ( ( ) (
V11
() )
set
) ))
`
)
: ( ( ) ( )
M2
( the
U1
of
b
1
: ( ( non
empty
satisfying_DN_1
) ( non
empty
join-commutative
satisfying_DN_1
)
ComplLLattStr
) : ( ( ) (
V11
() )
set
) ))
)
: ( ( ) ( )
M2
( the
U1
of
b
1
: ( ( non
empty
satisfying_DN_1
) ( non
empty
join-commutative
satisfying_DN_1
)
ComplLLattStr
) : ( ( ) (
V11
() )
set
) ))
`
)
: ( ( ) ( )
M2
( the
U1
of
b
1
: ( ( non
empty
satisfying_DN_1
) ( non
empty
join-commutative
satisfying_DN_1
)
ComplLLattStr
) : ( ( ) (
V11
() )
set
) ))
+
y
: ( ( ) ( )
Element
of ( ( ) (
V11
() )
set
) ) : ( ( ) ( )
M2
( the
U1
of
b
1
: ( ( non
empty
satisfying_DN_1
) ( non
empty
join-commutative
satisfying_DN_1
)
ComplLLattStr
) : ( ( ) (
V11
() )
set
) ))
=
y
: ( ( ) ( )
Element
of ( ( ) (
V11
() )
set
) ) ;
theorem
:: ROBBINS2:41
for
L
being ( ( non
empty
satisfying_DN_1
) ( non
empty
join-commutative
satisfying_DN_1
)
ComplLLattStr
)
for
x
,
y
,
z
being ( ( ) ( )
Element
of ( ( ) (
V11
() )
set
) ) holds
(
(
(
(
(
x
: ( ( ) ( )
Element
of ( ( ) (
V11
() )
set
) )
+
(
y
: ( ( ) ( )
Element
of ( ( ) (
V11
() )
set
) )
`
)
: ( ( ) ( )
M2
( the
U1
of
b
1
: ( ( non
empty
satisfying_DN_1
) ( non
empty
join-commutative
satisfying_DN_1
)
ComplLLattStr
) : ( ( ) (
V11
() )
set
) ))
)
: ( ( ) ( )
M2
( the
U1
of
b
1
: ( ( non
empty
satisfying_DN_1
) ( non
empty
join-commutative
satisfying_DN_1
)
ComplLLattStr
) : ( ( ) (
V11
() )
set
) ))
+
z
: ( ( ) ( )
Element
of ( ( ) (
V11
() )
set
) )
)
: ( ( ) ( )
M2
( the
U1
of
b
1
: ( ( non
empty
satisfying_DN_1
) ( non
empty
join-commutative
satisfying_DN_1
)
ComplLLattStr
) : ( ( ) (
V11
() )
set
) ))
`
)
: ( ( ) ( )
M2
( the
U1
of
b
1
: ( ( non
empty
satisfying_DN_1
) ( non
empty
join-commutative
satisfying_DN_1
)
ComplLLattStr
) : ( ( ) (
V11
() )
set
) ))
+
y
: ( ( ) ( )
Element
of ( ( ) (
V11
() )
set
) )
)
: ( ( ) ( )
M2
( the
U1
of
b
1
: ( ( non
empty
satisfying_DN_1
) ( non
empty
join-commutative
satisfying_DN_1
)
ComplLLattStr
) : ( ( ) (
V11
() )
set
) ))
`
)
: ( ( ) ( )
M2
( the
U1
of
b
1
: ( ( non
empty
satisfying_DN_1
) ( non
empty
join-commutative
satisfying_DN_1
)
ComplLLattStr
) : ( ( ) (
V11
() )
set
) ))
`
: ( ( ) ( )
M2
( the
U1
of
b
1
: ( ( non
empty
satisfying_DN_1
) ( non
empty
join-commutative
satisfying_DN_1
)
ComplLLattStr
) : ( ( ) (
V11
() )
set
) ))
=
y
: ( ( ) ( )
Element
of ( ( ) (
V11
() )
set
) ) ;
theorem
:: ROBBINS2:42
for
L
being ( ( non
empty
satisfying_DN_1
) ( non
empty
join-commutative
satisfying_DN_1
)
ComplLLattStr
)
for
x
,
y
,
z
being ( ( ) ( )
Element
of ( ( ) (
V11
() )
set
) ) holds
x
: ( ( ) ( )
Element
of ( ( ) (
V11
() )
set
) )
+
(
(
(
y
: ( ( ) ( )
Element
of ( ( ) (
V11
() )
set
) )
+
(
x
: ( ( ) ( )
Element
of ( ( ) (
V11
() )
set
) )
`
)
: ( ( ) ( )
M2
( the
U1
of
b
1
: ( ( non
empty
satisfying_DN_1
) ( non
empty
join-commutative
satisfying_DN_1
)
ComplLLattStr
) : ( ( ) (
V11
() )
set
) ))
)
: ( ( ) ( )
M2
( the
U1
of
b
1
: ( ( non
empty
satisfying_DN_1
) ( non
empty
join-commutative
satisfying_DN_1
)
ComplLLattStr
) : ( ( ) (
V11
() )
set
) ))
+
z
: ( ( ) ( )
Element
of ( ( ) (
V11
() )
set
) )
)
: ( ( ) ( )
M2
( the
U1
of
b
1
: ( ( non
empty
satisfying_DN_1
) ( non
empty
join-commutative
satisfying_DN_1
)
ComplLLattStr
) : ( ( ) (
V11
() )
set
) ))
`
)
: ( ( ) ( )
M2
( the
U1
of
b
1
: ( ( non
empty
satisfying_DN_1
) ( non
empty
join-commutative
satisfying_DN_1
)
ComplLLattStr
) : ( ( ) (
V11
() )
set
) )) : ( ( ) ( )
M2
( the
U1
of
b
1
: ( ( non
empty
satisfying_DN_1
) ( non
empty
join-commutative
satisfying_DN_1
)
ComplLLattStr
) : ( ( ) (
V11
() )
set
) ))
=
x
: ( ( ) ( )
Element
of ( ( ) (
V11
() )
set
) ) ;
theorem
:: ROBBINS2:43
for
L
being ( ( non
empty
satisfying_DN_1
) ( non
empty
join-commutative
satisfying_DN_1
)
ComplLLattStr
)
for
x
,
y
,
z
being ( ( ) ( )
Element
of ( ( ) (
V11
() )
set
) ) holds
(
x
: ( ( ) ( )
Element
of ( ( ) (
V11
() )
set
) )
`
)
: ( ( ) ( )
M2
( the
U1
of
b
1
: ( ( non
empty
satisfying_DN_1
) ( non
empty
join-commutative
satisfying_DN_1
)
ComplLLattStr
) : ( ( ) (
V11
() )
set
) ))
+
(
(
(
y
: ( ( ) ( )
Element
of ( ( ) (
V11
() )
set
) )
+
x
: ( ( ) ( )
Element
of ( ( ) (
V11
() )
set
) )
)
: ( ( ) ( )
M2
( the
U1
of
b
1
: ( ( non
empty
satisfying_DN_1
) ( non
empty
join-commutative
satisfying_DN_1
)
ComplLLattStr
) : ( ( ) (
V11
() )
set
) ))
+
z
: ( ( ) ( )
Element
of ( ( ) (
V11
() )
set
) )
)
: ( ( ) ( )
M2
( the
U1
of
b
1
: ( ( non
empty
satisfying_DN_1
) ( non
empty
join-commutative
satisfying_DN_1
)
ComplLLattStr
) : ( ( ) (
V11
() )
set
) ))
`
)
: ( ( ) ( )
M2
( the
U1
of
b
1
: ( ( non
empty
satisfying_DN_1
) ( non
empty
join-commutative
satisfying_DN_1
)
ComplLLattStr
) : ( ( ) (
V11
() )
set
) )) : ( ( ) ( )
M2
( the
U1
of
b
1
: ( ( non
empty
satisfying_DN_1
) ( non
empty
join-commutative
satisfying_DN_1
)
ComplLLattStr
) : ( ( ) (
V11
() )
set
) ))
=
x
: ( ( ) ( )
Element
of ( ( ) (
V11
() )
set
) )
`
: ( ( ) ( )
M2
( the
U1
of
b
1
: ( ( non
empty
satisfying_DN_1
) ( non
empty
join-commutative
satisfying_DN_1
)
ComplLLattStr
) : ( ( ) (
V11
() )
set
) )) ;
theorem
:: ROBBINS2:44
for
L
being ( ( non
empty
satisfying_DN_1
) ( non
empty
join-commutative
satisfying_DN_1
)
ComplLLattStr
)
for
x
,
y
being ( ( ) ( )
Element
of ( ( ) (
V11
() )
set
) ) holds
(
(
x
: ( ( ) ( )
Element
of ( ( ) (
V11
() )
set
) )
+
y
: ( ( ) ( )
Element
of ( ( ) (
V11
() )
set
) )
)
: ( ( ) ( )
M2
( the
U1
of
b
1
: ( ( non
empty
satisfying_DN_1
) ( non
empty
join-commutative
satisfying_DN_1
)
ComplLLattStr
) : ( ( ) (
V11
() )
set
) ))
`
)
: ( ( ) ( )
M2
( the
U1
of
b
1
: ( ( non
empty
satisfying_DN_1
) ( non
empty
join-commutative
satisfying_DN_1
)
ComplLLattStr
) : ( ( ) (
V11
() )
set
) ))
+
x
: ( ( ) ( )
Element
of ( ( ) (
V11
() )
set
) ) : ( ( ) ( )
M2
( the
U1
of
b
1
: ( ( non
empty
satisfying_DN_1
) ( non
empty
join-commutative
satisfying_DN_1
)
ComplLLattStr
) : ( ( ) (
V11
() )
set
) ))
=
x
: ( ( ) ( )
Element
of ( ( ) (
V11
() )
set
) )
+
(
y
: ( ( ) ( )
Element
of ( ( ) (
V11
() )
set
) )
`
)
: ( ( ) ( )
M2
( the
U1
of
b
1
: ( ( non
empty
satisfying_DN_1
) ( non
empty
join-commutative
satisfying_DN_1
)
ComplLLattStr
) : ( ( ) (
V11
() )
set
) )) : ( ( ) ( )
M2
( the
U1
of
b
1
: ( ( non
empty
satisfying_DN_1
) ( non
empty
join-commutative
satisfying_DN_1
)
ComplLLattStr
) : ( ( ) (
V11
() )
set
) )) ;
theorem
:: ROBBINS2:45
for
L
being ( ( non
empty
satisfying_DN_1
) ( non
empty
join-commutative
satisfying_DN_1
)
ComplLLattStr
)
for
x
,
y
being ( ( ) ( )
Element
of ( ( ) (
V11
() )
set
) ) holds
(
x
: ( ( ) ( )
Element
of ( ( ) (
V11
() )
set
) )
+
(
(
x
: ( ( ) ( )
Element
of ( ( ) (
V11
() )
set
) )
+
(
y
: ( ( ) ( )
Element
of ( ( ) (
V11
() )
set
) )
`
)
: ( ( ) ( )
M2
( the
U1
of
b
1
: ( ( non
empty
satisfying_DN_1
) ( non
empty
join-commutative
satisfying_DN_1
)
ComplLLattStr
) : ( ( ) (
V11
() )
set
) ))
)
: ( ( ) ( )
M2
( the
U1
of
b
1
: ( ( non
empty
satisfying_DN_1
) ( non
empty
join-commutative
satisfying_DN_1
)
ComplLLattStr
) : ( ( ) (
V11
() )
set
) ))
`
)
: ( ( ) ( )
M2
( the
U1
of
b
1
: ( ( non
empty
satisfying_DN_1
) ( non
empty
join-commutative
satisfying_DN_1
)
ComplLLattStr
) : ( ( ) (
V11
() )
set
) ))
)
: ( ( ) ( )
M2
( the
U1
of
b
1
: ( ( non
empty
satisfying_DN_1
) ( non
empty
join-commutative
satisfying_DN_1
)
ComplLLattStr
) : ( ( ) (
V11
() )
set
) ))
`
: ( ( ) ( )
M2
( the
U1
of
b
1
: ( ( non
empty
satisfying_DN_1
) ( non
empty
join-commutative
satisfying_DN_1
)
ComplLLattStr
) : ( ( ) (
V11
() )
set
) ))
=
(
x
: ( ( ) ( )
Element
of ( ( ) (
V11
() )
set
) )
+
y
: ( ( ) ( )
Element
of ( ( ) (
V11
() )
set
) )
)
: ( ( ) ( )
M2
( the
U1
of
b
1
: ( ( non
empty
satisfying_DN_1
) ( non
empty
join-commutative
satisfying_DN_1
)
ComplLLattStr
) : ( ( ) (
V11
() )
set
) ))
`
: ( ( ) ( )
M2
( the
U1
of
b
1
: ( ( non
empty
satisfying_DN_1
) ( non
empty
join-commutative
satisfying_DN_1
)
ComplLLattStr
) : ( ( ) (
V11
() )
set
) )) ;
theorem
:: ROBBINS2:46
for
L
being ( ( non
empty
satisfying_DN_1
) ( non
empty
join-commutative
satisfying_DN_1
)
ComplLLattStr
)
for
x
,
y
,
z
being ( ( ) ( )
Element
of ( ( ) (
V11
() )
set
) ) holds
(
(
(
(
x
: ( ( ) ( )
Element
of ( ( ) (
V11
() )
set
) )
+
y
: ( ( ) ( )
Element
of ( ( ) (
V11
() )
set
) )
)
: ( ( ) ( )
M2
( the
U1
of
b
1
: ( ( non
empty
satisfying_DN_1
) ( non
empty
join-commutative
satisfying_DN_1
)
ComplLLattStr
) : ( ( ) (
V11
() )
set
) ))
`
)
: ( ( ) ( )
M2
( the
U1
of
b
1
: ( ( non
empty
satisfying_DN_1
) ( non
empty
join-commutative
satisfying_DN_1
)
ComplLLattStr
) : ( ( ) (
V11
() )
set
) ))
+
(
x
: ( ( ) ( )
Element
of ( ( ) (
V11
() )
set
) )
+
z
: ( ( ) ( )
Element
of ( ( ) (
V11
() )
set
) )
)
: ( ( ) ( )
M2
( the
U1
of
b
1
: ( ( non
empty
satisfying_DN_1
) ( non
empty
join-commutative
satisfying_DN_1
)
ComplLLattStr
) : ( ( ) (
V11
() )
set
) ))
)
: ( ( ) ( )
M2
( the
U1
of
b
1
: ( ( non
empty
satisfying_DN_1
) ( non
empty
join-commutative
satisfying_DN_1
)
ComplLLattStr
) : ( ( ) (
V11
() )
set
) ))
`
)
: ( ( ) ( )
M2
( the
U1
of
b
1
: ( ( non
empty
satisfying_DN_1
) ( non
empty
join-commutative
satisfying_DN_1
)
ComplLLattStr
) : ( ( ) (
V11
() )
set
) ))
+
y
: ( ( ) ( )
Element
of ( ( ) (
V11
() )
set
) ) : ( ( ) ( )
M2
( the
U1
of
b
1
: ( ( non
empty
satisfying_DN_1
) ( non
empty
join-commutative
satisfying_DN_1
)
ComplLLattStr
) : ( ( ) (
V11
() )
set
) ))
=
y
: ( ( ) ( )
Element
of ( ( ) (
V11
() )
set
) ) ;
theorem
:: ROBBINS2:47
for
L
being ( ( non
empty
satisfying_DN_1
) ( non
empty
join-commutative
satisfying_DN_1
)
ComplLLattStr
)
for
x
,
y
,
z
being ( ( ) ( )
Element
of ( ( ) (
V11
() )
set
) ) holds
(
(
(
(
(
(
x
: ( ( ) ( )
Element
of ( ( ) (
V11
() )
set
) )
+
y
: ( ( ) ( )
Element
of ( ( ) (
V11
() )
set
) )
)
: ( ( ) ( )
M2
( the
U1
of
b
1
: ( ( non
empty
satisfying_DN_1
) ( non
empty
join-commutative
satisfying_DN_1
)
ComplLLattStr
) : ( ( ) (
V11
() )
set
) ))
`
)
: ( ( ) ( )
M2
( the
U1
of
b
1
: ( ( non
empty
satisfying_DN_1
) ( non
empty
join-commutative
satisfying_DN_1
)
ComplLLattStr
) : ( ( ) (
V11
() )
set
) ))
+
z
: ( ( ) ( )
Element
of ( ( ) (
V11
() )
set
) )
)
: ( ( ) ( )
M2
( the
U1
of
b
1
: ( ( non
empty
satisfying_DN_1
) ( non
empty
join-commutative
satisfying_DN_1
)
ComplLLattStr
) : ( ( ) (
V11
() )
set
) ))
`
)
: ( ( ) ( )
M2
( the
U1
of
b
1
: ( ( non
empty
satisfying_DN_1
) ( non
empty
join-commutative
satisfying_DN_1
)
ComplLLattStr
) : ( ( ) (
V11
() )
set
) ))
+
(
(
(
x
: ( ( ) ( )
Element
of ( ( ) (
V11
() )
set
) )
`
)
: ( ( ) ( )
M2
( the
U1
of
b
1
: ( ( non
empty
satisfying_DN_1
) ( non
empty
join-commutative
satisfying_DN_1
)
ComplLLattStr
) : ( ( ) (
V11
() )
set
) ))
+
y
: ( ( ) ( )
Element
of ( ( ) (
V11
() )
set
) )
)
: ( ( ) ( )
M2
( the
U1
of
b
1
: ( ( non
empty
satisfying_DN_1
) ( non
empty
join-commutative
satisfying_DN_1
)
ComplLLattStr
) : ( ( ) (
V11
() )
set
) ))
`
)
: ( ( ) ( )
M2
( the
U1
of
b
1
: ( ( non
empty
satisfying_DN_1
) ( non
empty
join-commutative
satisfying_DN_1
)
ComplLLattStr
) : ( ( ) (
V11
() )
set
) ))
)
: ( ( ) ( )
M2
( the
U1
of
b
1
: ( ( non
empty
satisfying_DN_1
) ( non
empty
join-commutative
satisfying_DN_1
)
ComplLLattStr
) : ( ( ) (
V11
() )
set
) ))
`
)
: ( ( ) ( )
M2
( the
U1
of
b
1
: ( ( non
empty
satisfying_DN_1
) ( non
empty
join-commutative
satisfying_DN_1
)
ComplLLattStr
) : ( ( ) (
V11
() )
set
) ))
+
y
: ( ( ) ( )
Element
of ( ( ) (
V11
() )
set
) ) : ( ( ) ( )
M2
( the
U1
of
b
1
: ( ( non
empty
satisfying_DN_1
) ( non
empty
join-commutative
satisfying_DN_1
)
ComplLLattStr
) : ( ( ) (
V11
() )
set
) ))
=
(
(
(
x
: ( ( ) ( )
Element
of ( ( ) (
V11
() )
set
) )
`
)
: ( ( ) ( )
M2
( the
U1
of
b
1
: ( ( non
empty
satisfying_DN_1
) ( non
empty
join-commutative
satisfying_DN_1
)
ComplLLattStr
) : ( ( ) (
V11
() )
set
) ))
+
y
: ( ( ) ( )
Element
of ( ( ) (
V11
() )
set
) )
)
: ( ( ) ( )
M2
( the
U1
of
b
1
: ( ( non
empty
satisfying_DN_1
) ( non
empty
join-commutative
satisfying_DN_1
)
ComplLLattStr
) : ( ( ) (
V11
() )
set
) ))
`
)
: ( ( ) ( )
M2
( the
U1
of
b
1
: ( ( non
empty
satisfying_DN_1
) ( non
empty
join-commutative
satisfying_DN_1
)
ComplLLattStr
) : ( ( ) (
V11
() )
set
) ))
`
: ( ( ) ( )
M2
( the
U1
of
b
1
: ( ( non
empty
satisfying_DN_1
) ( non
empty
join-commutative
satisfying_DN_1
)
ComplLLattStr
) : ( ( ) (
V11
() )
set
) )) ;
theorem
:: ROBBINS2:48
for
L
being ( ( non
empty
satisfying_DN_1
) ( non
empty
join-commutative
satisfying_DN_1
)
ComplLLattStr
)
for
x
,
y
,
z
being ( ( ) ( )
Element
of ( ( ) (
V11
() )
set
) ) holds
(
(
(
(
(
(
x
: ( ( ) ( )
Element
of ( ( ) (
V11
() )
set
) )
+
y
: ( ( ) ( )
Element
of ( ( ) (
V11
() )
set
) )
)
: ( ( ) ( )
M2
( the
U1
of
b
1
: ( ( non
empty
satisfying_DN_1
) ( non
empty
join-commutative
satisfying_DN_1
)
ComplLLattStr
) : ( ( ) (
V11
() )
set
) ))
`
)
: ( ( ) ( )
M2
( the
U1
of
b
1
: ( ( non
empty
satisfying_DN_1
) ( non
empty
join-commutative
satisfying_DN_1
)
ComplLLattStr
) : ( ( ) (
V11
() )
set
) ))
+
z
: ( ( ) ( )
Element
of ( ( ) (
V11
() )
set
) )
)
: ( ( ) ( )
M2
( the
U1
of
b
1
: ( ( non
empty
satisfying_DN_1
) ( non
empty
join-commutative
satisfying_DN_1
)
ComplLLattStr
) : ( ( ) (
V11
() )
set
) ))
`
)
: ( ( ) ( )
M2
( the
U1
of
b
1
: ( ( non
empty
satisfying_DN_1
) ( non
empty
join-commutative
satisfying_DN_1
)
ComplLLattStr
) : ( ( ) (
V11
() )
set
) ))
+
(
(
(
x
: ( ( ) ( )
Element
of ( ( ) (
V11
() )
set
) )
`
)
: ( ( ) ( )
M2
( the
U1
of
b
1
: ( ( non
empty
satisfying_DN_1
) ( non
empty
join-commutative
satisfying_DN_1
)
ComplLLattStr
) : ( ( ) (
V11
() )
set
) ))
+
y
: ( ( ) ( )
Element
of ( ( ) (
V11
() )
set
) )
)
: ( ( ) ( )
M2
( the
U1
of
b
1
: ( ( non
empty
satisfying_DN_1
) ( non
empty
join-commutative
satisfying_DN_1
)
ComplLLattStr
) : ( ( ) (
V11
() )
set
) ))
`
)
: ( ( ) ( )
M2
( the
U1
of
b
1
: ( ( non
empty
satisfying_DN_1
) ( non
empty
join-commutative
satisfying_DN_1
)
ComplLLattStr
) : ( ( ) (
V11
() )
set
) ))
)
: ( ( ) ( )
M2
( the
U1
of
b
1
: ( ( non
empty
satisfying_DN_1
) ( non
empty
join-commutative
satisfying_DN_1
)
ComplLLattStr
) : ( ( ) (
V11
() )
set
) ))
`
)
: ( ( ) ( )
M2
( the
U1
of
b
1
: ( ( non
empty
satisfying_DN_1
) ( non
empty
join-commutative
satisfying_DN_1
)
ComplLLattStr
) : ( ( ) (
V11
() )
set
) ))
+
y
: ( ( ) ( )
Element
of ( ( ) (
V11
() )
set
) ) : ( ( ) ( )
M2
( the
U1
of
b
1
: ( ( non
empty
satisfying_DN_1
) ( non
empty
join-commutative
satisfying_DN_1
)
ComplLLattStr
) : ( ( ) (
V11
() )
set
) ))
=
(
x
: ( ( ) ( )
Element
of ( ( ) (
V11
() )
set
) )
`
)
: ( ( ) ( )
M2
( the
U1
of
b
1
: ( ( non
empty
satisfying_DN_1
) ( non
empty
join-commutative
satisfying_DN_1
)
ComplLLattStr
) : ( ( ) (
V11
() )
set
) ))
+
y
: ( ( ) ( )
Element
of ( ( ) (
V11
() )
set
) ) : ( ( ) ( )
M2
( the
U1
of
b
1
: ( ( non
empty
satisfying_DN_1
) ( non
empty
join-commutative
satisfying_DN_1
)
ComplLLattStr
) : ( ( ) (
V11
() )
set
) )) ;
theorem
:: ROBBINS2:49
for
L
being ( ( non
empty
satisfying_DN_1
) ( non
empty
join-commutative
satisfying_DN_1
)
ComplLLattStr
)
for
x
,
y
,
z
being ( ( ) ( )
Element
of ( ( ) (
V11
() )
set
) ) holds
(
(
(
x
: ( ( ) ( )
Element
of ( ( ) (
V11
() )
set
) )
`
)
: ( ( ) ( )
M2
( the
U1
of
b
1
: ( ( non
empty
satisfying_DN_1
) ( non
empty
join-commutative
satisfying_DN_1
)
ComplLLattStr
) : ( ( ) (
V11
() )
set
) ))
+
(
(
(
(
(
y
: ( ( ) ( )
Element
of ( ( ) (
V11
() )
set
) )
+
x
: ( ( ) ( )
Element
of ( ( ) (
V11
() )
set
) )
)
: ( ( ) ( )
M2
( the
U1
of
b
1
: ( ( non
empty
satisfying_DN_1
) ( non
empty
join-commutative
satisfying_DN_1
)
ComplLLattStr
) : ( ( ) (
V11
() )
set
) ))
`
)
: ( ( ) ( )
M2
( the
U1
of
b
1
: ( ( non
empty
satisfying_DN_1
) ( non
empty
join-commutative
satisfying_DN_1
)
ComplLLattStr
) : ( ( ) (
V11
() )
set
) ))
`
)
: ( ( ) ( )
M2
( the
U1
of
b
1
: ( ( non
empty
satisfying_DN_1
) ( non
empty
join-commutative
satisfying_DN_1
)
ComplLLattStr
) : ( ( ) (
V11
() )
set
) ))
+
(
y
: ( ( ) ( )
Element
of ( ( ) (
V11
() )
set
) )
+
z
: ( ( ) ( )
Element
of ( ( ) (
V11
() )
set
) )
)
: ( ( ) ( )
M2
( the
U1
of
b
1
: ( ( non
empty
satisfying_DN_1
) ( non
empty
join-commutative
satisfying_DN_1
)
ComplLLattStr
) : ( ( ) (
V11
() )
set
) ))
)
: ( ( ) ( )
M2
( the
U1
of
b
1
: ( ( non
empty
satisfying_DN_1
) ( non
empty
join-commutative
satisfying_DN_1
)
ComplLLattStr
) : ( ( ) (
V11
() )
set
) ))
`
)
: ( ( ) ( )
M2
( the
U1
of
b
1
: ( ( non
empty
satisfying_DN_1
) ( non
empty
join-commutative
satisfying_DN_1
)
ComplLLattStr
) : ( ( ) (
V11
() )
set
) ))
)
: ( ( ) ( )
M2
( the
U1
of
b
1
: ( ( non
empty
satisfying_DN_1
) ( non
empty
join-commutative
satisfying_DN_1
)
ComplLLattStr
) : ( ( ) (
V11
() )
set
) ))
`
)
: ( ( ) ( )
M2
( the
U1
of
b
1
: ( ( non
empty
satisfying_DN_1
) ( non
empty
join-commutative
satisfying_DN_1
)
ComplLLattStr
) : ( ( ) (
V11
() )
set
) ))
+
(
y
: ( ( ) ( )
Element
of ( ( ) (
V11
() )
set
) )
+
z
: ( ( ) ( )
Element
of ( ( ) (
V11
() )
set
) )
)
: ( ( ) ( )
M2
( the
U1
of
b
1
: ( ( non
empty
satisfying_DN_1
) ( non
empty
join-commutative
satisfying_DN_1
)
ComplLLattStr
) : ( ( ) (
V11
() )
set
) )) : ( ( ) ( )
M2
( the
U1
of
b
1
: ( ( non
empty
satisfying_DN_1
) ( non
empty
join-commutative
satisfying_DN_1
)
ComplLLattStr
) : ( ( ) (
V11
() )
set
) ))
=
(
(
(
y
: ( ( ) ( )
Element
of ( ( ) (
V11
() )
set
) )
+
x
: ( ( ) ( )
Element
of ( ( ) (
V11
() )
set
) )
)
: ( ( ) ( )
M2
( the
U1
of
b
1
: ( ( non
empty
satisfying_DN_1
) ( non
empty
join-commutative
satisfying_DN_1
)
ComplLLattStr
) : ( ( ) (
V11
() )
set
) ))
`
)
: ( ( ) ( )
M2
( the
U1
of
b
1
: ( ( non
empty
satisfying_DN_1
) ( non
empty
join-commutative
satisfying_DN_1
)
ComplLLattStr
) : ( ( ) (
V11
() )
set
) ))
`
)
: ( ( ) ( )
M2
( the
U1
of
b
1
: ( ( non
empty
satisfying_DN_1
) ( non
empty
join-commutative
satisfying_DN_1
)
ComplLLattStr
) : ( ( ) (
V11
() )
set
) ))
+
(
y
: ( ( ) ( )
Element
of ( ( ) (
V11
() )
set
) )
+
z
: ( ( ) ( )
Element
of ( ( ) (
V11
() )
set
) )
)
: ( ( ) ( )
M2
( the
U1
of
b
1
: ( ( non
empty
satisfying_DN_1
) ( non
empty
join-commutative
satisfying_DN_1
)
ComplLLattStr
) : ( ( ) (
V11
() )
set
) )) : ( ( ) ( )
M2
( the
U1
of
b
1
: ( ( non
empty
satisfying_DN_1
) ( non
empty
join-commutative
satisfying_DN_1
)
ComplLLattStr
) : ( ( ) (
V11
() )
set
) )) ;
theorem
:: ROBBINS2:50
for
L
being ( ( non
empty
satisfying_DN_1
) ( non
empty
join-commutative
satisfying_DN_1
)
ComplLLattStr
)
for
x
,
y
,
z
being ( ( ) ( )
Element
of ( ( ) (
V11
() )
set
) ) holds
(
(
(
x
: ( ( ) ( )
Element
of ( ( ) (
V11
() )
set
) )
`
)
: ( ( ) ( )
M2
( the
U1
of
b
1
: ( ( non
empty
satisfying_DN_1
) ( non
empty
join-commutative
satisfying_DN_1
)
ComplLLattStr
) : ( ( ) (
V11
() )
set
) ))
+
(
(
(
y
: ( ( ) ( )
Element
of ( ( ) (
V11
() )
set
) )
+
x
: ( ( ) ( )
Element
of ( ( ) (
V11
() )
set
) )
)
: ( ( ) ( )
M2
( the
U1
of
b
1
: ( ( non
empty
satisfying_DN_1
) ( non
empty
join-commutative
satisfying_DN_1
)
ComplLLattStr
) : ( ( ) (
V11
() )
set
) ))
+
(
y
: ( ( ) ( )
Element
of ( ( ) (
V11
() )
set
) )
+
z
: ( ( ) ( )
Element
of ( ( ) (
V11
() )
set
) )
)
: ( ( ) ( )
M2
( the
U1
of
b
1
: ( ( non
empty
satisfying_DN_1
) ( non
empty
join-commutative
satisfying_DN_1
)
ComplLLattStr
) : ( ( ) (
V11
() )
set
) ))
)
: ( ( ) ( )
M2
( the
U1
of
b
1
: ( ( non
empty
satisfying_DN_1
) ( non
empty
join-commutative
satisfying_DN_1
)
ComplLLattStr
) : ( ( ) (
V11
() )
set
) ))
`
)
: ( ( ) ( )
M2
( the
U1
of
b
1
: ( ( non
empty
satisfying_DN_1
) ( non
empty
join-commutative
satisfying_DN_1
)
ComplLLattStr
) : ( ( ) (
V11
() )
set
) ))
)
: ( ( ) ( )
M2
( the
U1
of
b
1
: ( ( non
empty
satisfying_DN_1
) ( non
empty
join-commutative
satisfying_DN_1
)
ComplLLattStr
) : ( ( ) (
V11
() )
set
) ))
`
)
: ( ( ) ( )
M2
( the
U1
of
b
1
: ( ( non
empty
satisfying_DN_1
) ( non
empty
join-commutative
satisfying_DN_1
)
ComplLLattStr
) : ( ( ) (
V11
() )
set
) ))
+
(
y
: ( ( ) ( )
Element
of ( ( ) (
V11
() )
set
) )
+
z
: ( ( ) ( )
Element
of ( ( ) (
V11
() )
set
) )
)
: ( ( ) ( )
M2
( the
U1
of
b
1
: ( ( non
empty
satisfying_DN_1
) ( non
empty
join-commutative
satisfying_DN_1
)
ComplLLattStr
) : ( ( ) (
V11
() )
set
) )) : ( ( ) ( )
M2
( the
U1
of
b
1
: ( ( non
empty
satisfying_DN_1
) ( non
empty
join-commutative
satisfying_DN_1
)
ComplLLattStr
) : ( ( ) (
V11
() )
set
) ))
=
(
(
(
y
: ( ( ) ( )
Element
of ( ( ) (
V11
() )
set
) )
+
x
: ( ( ) ( )
Element
of ( ( ) (
V11
() )
set
) )
)
: ( ( ) ( )
M2
( the
U1
of
b
1
: ( ( non
empty
satisfying_DN_1
) ( non
empty
join-commutative
satisfying_DN_1
)
ComplLLattStr
) : ( ( ) (
V11
() )
set
) ))
`
)
: ( ( ) ( )
M2
( the
U1
of
b
1
: ( ( non
empty
satisfying_DN_1
) ( non
empty
join-commutative
satisfying_DN_1
)
ComplLLattStr
) : ( ( ) (
V11
() )
set
) ))
`
)
: ( ( ) ( )
M2
( the
U1
of
b
1
: ( ( non
empty
satisfying_DN_1
) ( non
empty
join-commutative
satisfying_DN_1
)
ComplLLattStr
) : ( ( ) (
V11
() )
set
) ))
+
(
y
: ( ( ) ( )
Element
of ( ( ) (
V11
() )
set
) )
+
z
: ( ( ) ( )
Element
of ( ( ) (
V11
() )
set
) )
)
: ( ( ) ( )
M2
( the
U1
of
b
1
: ( ( non
empty
satisfying_DN_1
) ( non
empty
join-commutative
satisfying_DN_1
)
ComplLLattStr
) : ( ( ) (
V11
() )
set
) )) : ( ( ) ( )
M2
( the
U1
of
b
1
: ( ( non
empty
satisfying_DN_1
) ( non
empty
join-commutative
satisfying_DN_1
)
ComplLLattStr
) : ( ( ) (
V11
() )
set
) )) ;
theorem
:: ROBBINS2:51
for
L
being ( ( non
empty
satisfying_DN_1
) ( non
empty
join-commutative
satisfying_DN_1
)
ComplLLattStr
)
for
x
,
y
,
z
being ( ( ) ( )
Element
of ( ( ) (
V11
() )
set
) ) holds
(
(
(
x
: ( ( ) ( )
Element
of ( ( ) (
V11
() )
set
) )
`
)
: ( ( ) ( )
M2
( the
U1
of
b
1
: ( ( non
empty
satisfying_DN_1
) ( non
empty
join-commutative
satisfying_DN_1
)
ComplLLattStr
) : ( ( ) (
V11
() )
set
) ))
+
(
(
(
y
: ( ( ) ( )
Element
of ( ( ) (
V11
() )
set
) )
+
x
: ( ( ) ( )
Element
of ( ( ) (
V11
() )
set
) )
)
: ( ( ) ( )
M2
( the
U1
of
b
1
: ( ( non
empty
satisfying_DN_1
) ( non
empty
join-commutative
satisfying_DN_1
)
ComplLLattStr
) : ( ( ) (
V11
() )
set
) ))
+
(
y
: ( ( ) ( )
Element
of ( ( ) (
V11
() )
set
) )
+
z
: ( ( ) ( )
Element
of ( ( ) (
V11
() )
set
) )
)
: ( ( ) ( )
M2
( the
U1
of
b
1
: ( ( non
empty
satisfying_DN_1
) ( non
empty
join-commutative
satisfying_DN_1
)
ComplLLattStr
) : ( ( ) (
V11
() )
set
) ))
)
: ( ( ) ( )
M2
( the
U1
of
b
1
: ( ( non
empty
satisfying_DN_1
) ( non
empty
join-commutative
satisfying_DN_1
)
ComplLLattStr
) : ( ( ) (
V11
() )
set
) ))
`
)
: ( ( ) ( )
M2
( the
U1
of
b
1
: ( ( non
empty
satisfying_DN_1
) ( non
empty
join-commutative
satisfying_DN_1
)
ComplLLattStr
) : ( ( ) (
V11
() )
set
) ))
)
: ( ( ) ( )
M2
( the
U1
of
b
1
: ( ( non
empty
satisfying_DN_1
) ( non
empty
join-commutative
satisfying_DN_1
)
ComplLLattStr
) : ( ( ) (
V11
() )
set
) ))
`
)
: ( ( ) ( )
M2
( the
U1
of
b
1
: ( ( non
empty
satisfying_DN_1
) ( non
empty
join-commutative
satisfying_DN_1
)
ComplLLattStr
) : ( ( ) (
V11
() )
set
) ))
+
(
y
: ( ( ) ( )
Element
of ( ( ) (
V11
() )
set
) )
+
z
: ( ( ) ( )
Element
of ( ( ) (
V11
() )
set
) )
)
: ( ( ) ( )
M2
( the
U1
of
b
1
: ( ( non
empty
satisfying_DN_1
) ( non
empty
join-commutative
satisfying_DN_1
)
ComplLLattStr
) : ( ( ) (
V11
() )
set
) )) : ( ( ) ( )
M2
( the
U1
of
b
1
: ( ( non
empty
satisfying_DN_1
) ( non
empty
join-commutative
satisfying_DN_1
)
ComplLLattStr
) : ( ( ) (
V11
() )
set
) ))
=
(
y
: ( ( ) ( )
Element
of ( ( ) (
V11
() )
set
) )
+
x
: ( ( ) ( )
Element
of ( ( ) (
V11
() )
set
) )
)
: ( ( ) ( )
M2
( the
U1
of
b
1
: ( ( non
empty
satisfying_DN_1
) ( non
empty
join-commutative
satisfying_DN_1
)
ComplLLattStr
) : ( ( ) (
V11
() )
set
) ))
+
(
y
: ( ( ) ( )
Element
of ( ( ) (
V11
() )
set
) )
+
z
: ( ( ) ( )
Element
of ( ( ) (
V11
() )
set
) )
)
: ( ( ) ( )
M2
( the
U1
of
b
1
: ( ( non
empty
satisfying_DN_1
) ( non
empty
join-commutative
satisfying_DN_1
)
ComplLLattStr
) : ( ( ) (
V11
() )
set
) )) : ( ( ) ( )
M2
( the
U1
of
b
1
: ( ( non
empty
satisfying_DN_1
) ( non
empty
join-commutative
satisfying_DN_1
)
ComplLLattStr
) : ( ( ) (
V11
() )
set
) )) ;
theorem
:: ROBBINS2:52
for
L
being ( ( non
empty
satisfying_DN_1
) ( non
empty
join-commutative
satisfying_DN_1
)
ComplLLattStr
)
for
x
,
y
,
z
being ( ( ) ( )
Element
of ( ( ) (
V11
() )
set
) ) holds
(
(
x
: ( ( ) ( )
Element
of ( ( ) (
V11
() )
set
) )
`
)
: ( ( ) ( )
M2
( the
U1
of
b
1
: ( ( non
empty
satisfying_DN_1
) ( non
empty
join-commutative
satisfying_DN_1
)
ComplLLattStr
) : ( ( ) (
V11
() )
set
) ))
`
)
: ( ( ) ( )
M2
( the
U1
of
b
1
: ( ( non
empty
satisfying_DN_1
) ( non
empty
join-commutative
satisfying_DN_1
)
ComplLLattStr
) : ( ( ) (
V11
() )
set
) ))
+
(
y
: ( ( ) ( )
Element
of ( ( ) (
V11
() )
set
) )
+
z
: ( ( ) ( )
Element
of ( ( ) (
V11
() )
set
) )
)
: ( ( ) ( )
M2
( the
U1
of
b
1
: ( ( non
empty
satisfying_DN_1
) ( non
empty
join-commutative
satisfying_DN_1
)
ComplLLattStr
) : ( ( ) (
V11
() )
set
) )) : ( ( ) ( )
M2
( the
U1
of
b
1
: ( ( non
empty
satisfying_DN_1
) ( non
empty
join-commutative
satisfying_DN_1
)
ComplLLattStr
) : ( ( ) (
V11
() )
set
) ))
=
(
y
: ( ( ) ( )
Element
of ( ( ) (
V11
() )
set
) )
+
x
: ( ( ) ( )
Element
of ( ( ) (
V11
() )
set
) )
)
: ( ( ) ( )
M2
( the
U1
of
b
1
: ( ( non
empty
satisfying_DN_1
) ( non
empty
join-commutative
satisfying_DN_1
)
ComplLLattStr
) : ( ( ) (
V11
() )
set
) ))
+
(
y
: ( ( ) ( )
Element
of ( ( ) (
V11
() )
set
) )
+
z
: ( ( ) ( )
Element
of ( ( ) (
V11
() )
set
) )
)
: ( ( ) ( )
M2
( the
U1
of
b
1
: ( ( non
empty
satisfying_DN_1
) ( non
empty
join-commutative
satisfying_DN_1
)
ComplLLattStr
) : ( ( ) (
V11
() )
set
) )) : ( ( ) ( )
M2
( the
U1
of
b
1
: ( ( non
empty
satisfying_DN_1
) ( non
empty
join-commutative
satisfying_DN_1
)
ComplLLattStr
) : ( ( ) (
V11
() )
set
) )) ;
theorem
:: ROBBINS2:53
for
L
being ( ( non
empty
satisfying_DN_1
) ( non
empty
join-commutative
satisfying_DN_1
)
ComplLLattStr
)
for
x
,
y
,
z
being ( ( ) ( )
Element
of ( ( ) (
V11
() )
set
) ) holds
(
x
: ( ( ) ( )
Element
of ( ( ) (
V11
() )
set
) )
+
y
: ( ( ) ( )
Element
of ( ( ) (
V11
() )
set
) )
)
: ( ( ) ( )
M2
( the
U1
of
b
1
: ( ( non
empty
satisfying_DN_1
) ( non
empty
join-commutative
satisfying_DN_1
)
ComplLLattStr
) : ( ( ) (
V11
() )
set
) ))
+
(
x
: ( ( ) ( )
Element
of ( ( ) (
V11
() )
set
) )
+
z
: ( ( ) ( )
Element
of ( ( ) (
V11
() )
set
) )
)
: ( ( ) ( )
M2
( the
U1
of
b
1
: ( ( non
empty
satisfying_DN_1
) ( non
empty
join-commutative
satisfying_DN_1
)
ComplLLattStr
) : ( ( ) (
V11
() )
set
) )) : ( ( ) ( )
M2
( the
U1
of
b
1
: ( ( non
empty
satisfying_DN_1
) ( non
empty
join-commutative
satisfying_DN_1
)
ComplLLattStr
) : ( ( ) (
V11
() )
set
) ))
=
y
: ( ( ) ( )
Element
of ( ( ) (
V11
() )
set
) )
+
(
x
: ( ( ) ( )
Element
of ( ( ) (
V11
() )
set
) )
+
z
: ( ( ) ( )
Element
of ( ( ) (
V11
() )
set
) )
)
: ( ( ) ( )
M2
( the
U1
of
b
1
: ( ( non
empty
satisfying_DN_1
) ( non
empty
join-commutative
satisfying_DN_1
)
ComplLLattStr
) : ( ( ) (
V11
() )
set
) )) : ( ( ) ( )
M2
( the
U1
of
b
1
: ( ( non
empty
satisfying_DN_1
) ( non
empty
join-commutative
satisfying_DN_1
)
ComplLLattStr
) : ( ( ) (
V11
() )
set
) )) ;
theorem
:: ROBBINS2:54
for
L
being ( ( non
empty
satisfying_DN_1
) ( non
empty
join-commutative
satisfying_DN_1
)
ComplLLattStr
)
for
x
,
y
,
z
being ( ( ) ( )
Element
of ( ( ) (
V11
() )
set
) ) holds
(
x
: ( ( ) ( )
Element
of ( ( ) (
V11
() )
set
) )
+
y
: ( ( ) ( )
Element
of ( ( ) (
V11
() )
set
) )
)
: ( ( ) ( )
M2
( the
U1
of
b
1
: ( ( non
empty
satisfying_DN_1
) ( non
empty
join-commutative
satisfying_DN_1
)
ComplLLattStr
) : ( ( ) (
V11
() )
set
) ))
+
(
x
: ( ( ) ( )
Element
of ( ( ) (
V11
() )
set
) )
+
z
: ( ( ) ( )
Element
of ( ( ) (
V11
() )
set
) )
)
: ( ( ) ( )
M2
( the
U1
of
b
1
: ( ( non
empty
satisfying_DN_1
) ( non
empty
join-commutative
satisfying_DN_1
)
ComplLLattStr
) : ( ( ) (
V11
() )
set
) )) : ( ( ) ( )
M2
( the
U1
of
b
1
: ( ( non
empty
satisfying_DN_1
) ( non
empty
join-commutative
satisfying_DN_1
)
ComplLLattStr
) : ( ( ) (
V11
() )
set
) ))
=
z
: ( ( ) ( )
Element
of ( ( ) (
V11
() )
set
) )
+
(
x
: ( ( ) ( )
Element
of ( ( ) (
V11
() )
set
) )
+
y
: ( ( ) ( )
Element
of ( ( ) (
V11
() )
set
) )
)
: ( ( ) ( )
M2
( the
U1
of
b
1
: ( ( non
empty
satisfying_DN_1
) ( non
empty
join-commutative
satisfying_DN_1
)
ComplLLattStr
) : ( ( ) (
V11
() )
set
) )) : ( ( ) ( )
M2
( the
U1
of
b
1
: ( ( non
empty
satisfying_DN_1
) ( non
empty
join-commutative
satisfying_DN_1
)
ComplLLattStr
) : ( ( ) (
V11
() )
set
) )) ;
theorem
:: ROBBINS2:55
for
L
being ( ( non
empty
satisfying_DN_1
) ( non
empty
join-commutative
satisfying_DN_1
)
ComplLLattStr
)
for
x
,
y
,
z
being ( ( ) ( )
Element
of ( ( ) (
V11
() )
set
) ) holds
x
: ( ( ) ( )
Element
of ( ( ) (
V11
() )
set
) )
+
(
y
: ( ( ) ( )
Element
of ( ( ) (
V11
() )
set
) )
+
z
: ( ( ) ( )
Element
of ( ( ) (
V11
() )
set
) )
)
: ( ( ) ( )
M2
( the
U1
of
b
1
: ( ( non
empty
satisfying_DN_1
) ( non
empty
join-commutative
satisfying_DN_1
)
ComplLLattStr
) : ( ( ) (
V11
() )
set
) )) : ( ( ) ( )
M2
( the
U1
of
b
1
: ( ( non
empty
satisfying_DN_1
) ( non
empty
join-commutative
satisfying_DN_1
)
ComplLLattStr
) : ( ( ) (
V11
() )
set
) ))
=
z
: ( ( ) ( )
Element
of ( ( ) (
V11
() )
set
) )
+
(
y
: ( ( ) ( )
Element
of ( ( ) (
V11
() )
set
) )
+
x
: ( ( ) ( )
Element
of ( ( ) (
V11
() )
set
) )
)
: ( ( ) ( )
M2
( the
U1
of
b
1
: ( ( non
empty
satisfying_DN_1
) ( non
empty
join-commutative
satisfying_DN_1
)
ComplLLattStr
) : ( ( ) (
V11
() )
set
) )) : ( ( ) ( )
M2
( the
U1
of
b
1
: ( ( non
empty
satisfying_DN_1
) ( non
empty
join-commutative
satisfying_DN_1
)
ComplLLattStr
) : ( ( ) (
V11
() )
set
) )) ;
theorem
:: ROBBINS2:56
for
L
being ( ( non
empty
satisfying_DN_1
) ( non
empty
join-commutative
satisfying_DN_1
)
ComplLLattStr
)
for
x
,
y
,
z
being ( ( ) ( )
Element
of ( ( ) (
V11
() )
set
) ) holds
x
: ( ( ) ( )
Element
of ( ( ) (
V11
() )
set
) )
+
(
y
: ( ( ) ( )
Element
of ( ( ) (
V11
() )
set
) )
+
z
: ( ( ) ( )
Element
of ( ( ) (
V11
() )
set
) )
)
: ( ( ) ( )
M2
( the
U1
of
b
1
: ( ( non
empty
satisfying_DN_1
) ( non
empty
join-commutative
satisfying_DN_1
)
ComplLLattStr
) : ( ( ) (
V11
() )
set
) )) : ( ( ) ( )
M2
( the
U1
of
b
1
: ( ( non
empty
satisfying_DN_1
) ( non
empty
join-commutative
satisfying_DN_1
)
ComplLLattStr
) : ( ( ) (
V11
() )
set
) ))
=
y
: ( ( ) ( )
Element
of ( ( ) (
V11
() )
set
) )
+
(
z
: ( ( ) ( )
Element
of ( ( ) (
V11
() )
set
) )
+
x
: ( ( ) ( )
Element
of ( ( ) (
V11
() )
set
) )
)
: ( ( ) ( )
M2
( the
U1
of
b
1
: ( ( non
empty
satisfying_DN_1
) ( non
empty
join-commutative
satisfying_DN_1
)
ComplLLattStr
) : ( ( ) (
V11
() )
set
) )) : ( ( ) ( )
M2
( the
U1
of
b
1
: ( ( non
empty
satisfying_DN_1
) ( non
empty
join-commutative
satisfying_DN_1
)
ComplLLattStr
) : ( ( ) (
V11
() )
set
) )) ;
theorem
:: ROBBINS2:57
for
L
being ( ( non
empty
satisfying_DN_1
) ( non
empty
join-commutative
satisfying_DN_1
)
ComplLLattStr
)
for
x
,
y
,
z
being ( ( ) ( )
Element
of ( ( ) (
V11
() )
set
) ) holds
(
x
: ( ( ) ( )
Element
of ( ( ) (
V11
() )
set
) )
+
y
: ( ( ) ( )
Element
of ( ( ) (
V11
() )
set
) )
)
: ( ( ) ( )
M2
( the
U1
of
b
1
: ( ( non
empty
satisfying_DN_1
) ( non
empty
join-commutative
satisfying_DN_1
)
ComplLLattStr
) : ( ( ) (
V11
() )
set
) ))
+
z
: ( ( ) ( )
Element
of ( ( ) (
V11
() )
set
) ) : ( ( ) ( )
M2
( the
U1
of
b
1
: ( ( non
empty
satisfying_DN_1
) ( non
empty
join-commutative
satisfying_DN_1
)
ComplLLattStr
) : ( ( ) (
V11
() )
set
) ))
=
x
: ( ( ) ( )
Element
of ( ( ) (
V11
() )
set
) )
+
(
y
: ( ( ) ( )
Element
of ( ( ) (
V11
() )
set
) )
+
z
: ( ( ) ( )
Element
of ( ( ) (
V11
() )
set
) )
)
: ( ( ) ( )
M2
( the
U1
of
b
1
: ( ( non
empty
satisfying_DN_1
) ( non
empty
join-commutative
satisfying_DN_1
)
ComplLLattStr
) : ( ( ) (
V11
() )
set
) )) : ( ( ) ( )
M2
( the
U1
of
b
1
: ( ( non
empty
satisfying_DN_1
) ( non
empty
join-commutative
satisfying_DN_1
)
ComplLLattStr
) : ( ( ) (
V11
() )
set
) )) ;
registration
cluster
non
empty
satisfying_DN_1
->
non
empty
join-associative
for ( ( ) ( )
ComplLLattStr
) ;
cluster
non
empty
satisfying_DN_1
->
non
empty
Robbins
for ( ( ) ( )
ComplLLattStr
) ;
end;
theorem
:: ROBBINS2:58
for
L
being ( ( non
empty
) ( non
empty
)
ComplLLattStr
)
for
x
,
z
being ( ( ) ( )
Element
of ( ( ) (
V11
() )
set
) ) st
L
: ( ( non
empty
) ( non
empty
)
ComplLLattStr
) is
join-commutative
&
L
: ( ( non
empty
) ( non
empty
)
ComplLLattStr
) is
join-associative
&
L
: ( ( non
empty
) ( non
empty
)
ComplLLattStr
) is
Huntington
holds
(
z
: ( ( ) ( )
Element
of ( ( ) (
V11
() )
set
) )
+
x
: ( ( ) ( )
Element
of ( ( ) (
V11
() )
set
) )
)
: ( ( ) ( )
M2
( the
U1
of
b
1
: ( ( non
empty
) ( non
empty
)
ComplLLattStr
) : ( ( ) (
V11
() )
set
) ))
*'
(
z
: ( ( ) ( )
Element
of ( ( ) (
V11
() )
set
) )
+
(
x
: ( ( ) ( )
Element
of ( ( ) (
V11
() )
set
) )
`
)
: ( ( ) ( )
M2
( the
U1
of
b
1
: ( ( non
empty
) ( non
empty
)
ComplLLattStr
) : ( ( ) (
V11
() )
set
) ))
)
: ( ( ) ( )
M2
( the
U1
of
b
1
: ( ( non
empty
) ( non
empty
)
ComplLLattStr
) : ( ( ) (
V11
() )
set
) )) : ( ( ) ( )
M2
( the
U1
of
b
1
: ( ( non
empty
) ( non
empty
)
ComplLLattStr
) : ( ( ) (
V11
() )
set
) ))
=
z
: ( ( ) ( )
Element
of ( ( ) (
V11
() )
set
) ) ;
theorem
:: ROBBINS2:59
for
L
being ( ( non
empty
join-commutative
join-associative
) ( non
empty
join-commutative
join-associative
)
ComplLLattStr
) st
L
: ( ( non
empty
join-commutative
join-associative
) ( non
empty
join-commutative
join-associative
)
ComplLLattStr
) is
Robbins
holds
L
: ( ( non
empty
join-commutative
join-associative
) ( non
empty
join-commutative
join-associative
)
ComplLLattStr
) is
satisfying_DN_1
;
registration
cluster
non
empty
join-commutative
join-associative
Robbins
->
non
empty
satisfying_DN_1
for ( ( ) ( )
ComplLLattStr
) ;
end;
registration
cluster
non
empty
join-commutative
join-associative
meet-commutative
meet-associative
meet-absorbing
join-absorbing
Lattice-like
de_Morgan
satisfying_DN_1
for ( ( ) ( )
OrthoLattStr
) ;
end;
registration
cluster
non
empty
Lattice-like
de_Morgan
satisfying_DN_1
->
non
empty
Lattice-like
Boolean
for ( ( ) ( )
OrthoLattStr
) ;
cluster
non
empty
Lattice-like
Boolean
well-complemented
->
non
empty
Lattice-like
well-complemented
satisfying_DN_1
for ( ( ) ( )
OrthoLattStr
) ;
end;
begin
definition
let
L
be ( ( non
empty
) ( non
empty
)
ComplLLattStr
) ;
attr
L
is
satisfying_MD_1
means
:: ROBBINS2:def 2
for
x
,
y
being ( ( ) ( )
Element
of ( ( ) ( )
set
) ) holds
(
(
(
x
: ( ( ) ( )
Element
of ( ( ) (
V11
() )
set
) )
`
)
: ( ( ) ( )
M2
( the
U1
of
L
: ( (
V33
() ) (
V33
() )
set
) : ( ( ) ( )
set
) ))
+
y
: ( ( ) ( )
Element
of ( ( ) (
V11
() )
set
) )
)
: ( ( ) ( )
M2
( the
U1
of
L
: ( (
V33
() ) (
V33
() )
set
) : ( ( ) ( )
set
) ))
`
)
: ( ( ) ( )
M2
( the
U1
of
L
: ( (
V33
() ) (
V33
() )
set
) : ( ( ) ( )
set
) ))
+
x
: ( ( ) ( )
Element
of ( ( ) (
V11
() )
set
) ) : ( ( ) ( )
M2
( the
U1
of
L
: ( (
V33
() ) (
V33
() )
set
) : ( ( ) ( )
set
) ))
=
x
: ( ( ) ( )
Element
of ( ( ) (
V11
() )
set
) ) ;
attr
L
is
satisfying_MD_2
means
:: ROBBINS2:def 3
for
x
,
y
,
z
being ( ( ) ( )
Element
of ( ( ) ( )
set
) ) holds
(
(
(
x
: ( ( ) ( )
Element
of ( ( ) (
V11
() )
set
) )
`
)
: ( ( ) ( )
M2
( the
U1
of
L
: ( (
V33
() ) (
V33
() )
set
) : ( ( ) ( )
set
) ))
+
y
: ( ( ) ( )
Element
of ( ( ) (
V11
() )
set
) )
)
: ( ( ) ( )
M2
( the
U1
of
L
: ( (
V33
() ) (
V33
() )
set
) : ( ( ) ( )
set
) ))
`
)
: ( ( ) ( )
M2
( the
U1
of
L
: ( (
V33
() ) (
V33
() )
set
) : ( ( ) ( )
set
) ))
+
(
z
: ( ( ) ( )
Element
of ( ( ) (
V11
() )
set
) )
+
y
: ( ( ) ( )
Element
of ( ( ) (
V11
() )
set
) )
)
: ( ( ) ( )
M2
( the
U1
of
L
: ( (
V33
() ) (
V33
() )
set
) : ( ( ) ( )
set
) )) : ( ( ) ( )
M2
( the
U1
of
L
: ( (
V33
() ) (
V33
() )
set
) : ( ( ) ( )
set
) ))
=
y
: ( ( ) ( )
Element
of ( ( ) (
V11
() )
set
) )
+
(
z
: ( ( ) ( )
Element
of ( ( ) (
V11
() )
set
) )
+
x
: ( ( ) ( )
Element
of ( ( ) (
V11
() )
set
) )
)
: ( ( ) ( )
M2
( the
U1
of
L
: ( (
V33
() ) (
V33
() )
set
) : ( ( ) ( )
set
) )) : ( ( ) ( )
M2
( the
U1
of
L
: ( (
V33
() ) (
V33
() )
set
) : ( ( ) ( )
set
) )) ;
end;
registration
cluster
non
empty
satisfying_MD_1
satisfying_MD_2
->
non
empty
join-commutative
join-associative
Huntington
for ( ( ) ( )
ComplLLattStr
) ;
cluster
non
empty
join-commutative
join-associative
Huntington
->
non
empty
satisfying_MD_1
satisfying_MD_2
for ( ( ) ( )
ComplLLattStr
) ;
end;
registration
cluster
non
empty
join-commutative
join-associative
meet-commutative
meet-associative
meet-absorbing
join-absorbing
Lattice-like
de_Morgan
satisfying_DN_1
satisfying_MD_1
satisfying_MD_2
for ( ( ) ( )
OrthoLattStr
) ;
end;
registration
cluster
non
empty
Lattice-like
de_Morgan
satisfying_MD_1
satisfying_MD_2
->
non
empty
Lattice-like
Boolean
for ( ( ) ( )
OrthoLattStr
) ;
cluster
non
empty
Lattice-like
Boolean
well-complemented
->
non
empty
Lattice-like
well-complemented
satisfying_MD_1
satisfying_MD_2
for ( ( ) ( )
OrthoLattStr
) ;
end;