:: MATHMORP semantic presentation
begin
definition
let
T
be ( ( non
empty
) ( non
empty
)
addMagma
) ;
let
p
be ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) ) ;
let
X
be ( ( ) ( )
Subset
of ) ;
func
X
+
p
->
( ( ) ( )
Subset
of )
equals
:: MATHMORP:def 1
{
(
q
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) )
+
p
: ( ( ) ( )
Element
of
T
: ( ( ) ( )
RLTopStruct
) )
)
: ( ( ) ( )
Element
of the
carrier
of
T
: ( ( ) ( )
RLTopStruct
) : ( ( ) ( )
set
) ) where
q
is ( ( ) ( )
Element
of ( ( ) ( )
set
) ) :
q
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) )
in
X
: ( (
V12
()
V30
(
K33
(
T
: ( ( ) ( )
RLTopStruct
) ,
T
: ( ( ) ( )
RLTopStruct
) ) : ( ( ) ( )
set
) ,
T
: ( ( ) ( )
RLTopStruct
) ) ) (
V12
()
V30
(
K33
(
T
: ( ( ) ( )
RLTopStruct
) ,
T
: ( ( ) ( )
RLTopStruct
) ) : ( ( ) ( )
set
) ,
T
: ( ( ) ( )
RLTopStruct
) ) )
Element
of
K32
(
K33
(
K33
(
T
: ( ( ) ( )
RLTopStruct
) ,
T
: ( ( ) ( )
RLTopStruct
) ) : ( ( ) ( )
set
) ,
T
: ( ( ) ( )
RLTopStruct
) ) : ( ( ) ( )
set
) ) : ( ( ) ( )
set
) )
}
;
end;
definition
let
T
be ( ( non
empty
) ( non
empty
)
addLoopStr
) ;
let
X
be ( ( ) ( )
Subset
of ) ;
func
X
!
->
( ( ) ( )
Subset
of )
equals
:: MATHMORP:def 2
{
(
-
q
: ( ( ) ( )
Point
of ( ( ) ( non
empty
)
set
) )
)
: ( ( ) ( )
Element
of the
carrier
of
T
: ( ( ) ( )
RLTopStruct
) : ( ( ) ( )
set
) ) where
q
is ( ( ) ( )
Point
of ( ( ) ( )
set
) ) :
q
: ( ( ) ( )
Point
of ( ( ) ( non
empty
)
set
) )
in
X
: ( ( ) ( )
Element
of
T
: ( ( ) ( )
RLTopStruct
) )
}
;
end;
definition
let
T
be ( ( non
empty
) ( non
empty
)
addMagma
) ;
let
X
,
B
be ( ( ) ( )
Subset
of ) ;
func
X
(-)
B
->
( ( ) ( )
Subset
of )
equals
:: MATHMORP:def 3
{
y
: ( ( ) ( )
Point
of ( ( ) ( non
empty
)
set
) ) where
y
is ( ( ) ( )
Point
of ( ( ) ( )
set
) ) :
B
: ( (
V12
()
V30
(
K33
(
T
: ( ( ) ( )
RLTopStruct
) ,
T
: ( ( ) ( )
RLTopStruct
) ) : ( ( ) ( )
set
) ,
T
: ( ( ) ( )
RLTopStruct
) ) ) (
V12
()
V30
(
K33
(
T
: ( ( ) ( )
RLTopStruct
) ,
T
: ( ( ) ( )
RLTopStruct
) ) : ( ( ) ( )
set
) ,
T
: ( ( ) ( )
RLTopStruct
) ) )
Element
of
K32
(
K33
(
K33
(
T
: ( ( ) ( )
RLTopStruct
) ,
T
: ( ( ) ( )
RLTopStruct
) ) : ( ( ) ( )
set
) ,
T
: ( ( ) ( )
RLTopStruct
) ) : ( ( ) ( )
set
) ) : ( ( ) ( )
set
) )
+
y
: ( ( ) ( )
Point
of ( ( ) ( non
empty
)
set
) ) : ( ( ) ( )
Subset
of )
c=
X
: ( ( ) ( )
Element
of
T
: ( ( ) ( )
RLTopStruct
) )
}
;
end;
notation
let
T
be ( ( non
empty
) ( non
empty
)
addLoopStr
) ;
let
A
,
B
be ( ( ) ( )
Subset
of ) ;
synonym
A
(+)
B
for
A
+
B
;
end;
theorem
:: MATHMORP:1
for
T
being ( ( non
empty
right_complementable
add-associative
right_zeroed
) ( non
empty
right_complementable
add-associative
right_zeroed
)
RLSStruct
)
for
B
being ( ( ) ( )
Subset
of ) holds
(
B
: ( ( ) ( )
Subset
of )
!
)
: ( ( ) ( )
Subset
of )
!
: ( ( ) ( )
Subset
of )
=
B
: ( ( ) ( )
Subset
of ) ;
theorem
:: MATHMORP:2
for
T
being ( ( non
empty
right_complementable
Abelian
add-associative
right_zeroed
) ( non
empty
left_complementable
right_complementable
Abelian
add-associative
right_zeroed
V153
() )
RLSStruct
)
for
x
being ( ( ) ( )
Point
of ( ( ) ( non
empty
)
set
) ) holds
{
(
0.
T
: ( ( non
empty
right_complementable
Abelian
add-associative
right_zeroed
) ( non
empty
left_complementable
right_complementable
Abelian
add-associative
right_zeroed
V153
() )
RLSStruct
)
)
: ( ( ) (
V49
(
b
1
: ( ( non
empty
right_complementable
Abelian
add-associative
right_zeroed
) ( non
empty
left_complementable
right_complementable
Abelian
add-associative
right_zeroed
V153
() )
RLSStruct
) ) )
Element
of the
carrier
of
b
1
: ( ( non
empty
right_complementable
Abelian
add-associative
right_zeroed
) ( non
empty
left_complementable
right_complementable
Abelian
add-associative
right_zeroed
V153
() )
RLSStruct
) : ( ( ) ( non
empty
)
set
) )
}
: ( ( ) ( non
empty
)
Element
of
K32
( the
carrier
of
b
1
: ( ( non
empty
right_complementable
Abelian
add-associative
right_zeroed
) ( non
empty
left_complementable
right_complementable
Abelian
add-associative
right_zeroed
V153
() )
RLSStruct
) : ( ( ) ( non
empty
)
set
) ) : ( ( ) ( )
set
) )
+
x
: ( ( ) ( )
Point
of ( ( ) ( non
empty
)
set
) ) : ( ( ) ( )
Subset
of )
=
{
x
: ( ( ) ( )
Point
of ( ( ) ( non
empty
)
set
) )
}
: ( ( ) ( non
empty
)
Element
of
K32
( the
carrier
of
b
1
: ( ( non
empty
right_complementable
Abelian
add-associative
right_zeroed
) ( non
empty
left_complementable
right_complementable
Abelian
add-associative
right_zeroed
V153
() )
RLSStruct
) : ( ( ) ( non
empty
)
set
) ) : ( ( ) ( )
set
) ) ;
theorem
:: MATHMORP:3
for
T
being ( ( non
empty
right_complementable
Abelian
add-associative
right_zeroed
) ( non
empty
left_complementable
right_complementable
Abelian
add-associative
right_zeroed
V153
() )
RLSStruct
)
for
B1
,
B2
being ( ( ) ( )
Subset
of )
for
p
being ( ( ) ( )
Point
of ( ( ) ( non
empty
)
set
) ) st
B1
: ( ( ) ( )
Subset
of )
c=
B2
: ( ( ) ( )
Subset
of ) holds
B1
: ( ( ) ( )
Subset
of )
+
p
: ( ( ) ( )
Point
of ( ( ) ( non
empty
)
set
) ) : ( ( ) ( )
Subset
of )
c=
B2
: ( ( ) ( )
Subset
of )
+
p
: ( ( ) ( )
Point
of ( ( ) ( non
empty
)
set
) ) : ( ( ) ( )
Subset
of ) ;
theorem
:: MATHMORP:4
for
T
being ( ( non
empty
right_complementable
Abelian
add-associative
right_zeroed
) ( non
empty
left_complementable
right_complementable
Abelian
add-associative
right_zeroed
V153
() )
RLSStruct
)
for
x
being ( ( ) ( )
Point
of ( ( ) ( non
empty
)
set
) )
for
X
being ( ( ) ( )
Subset
of ) st
X
: ( ( ) ( )
Subset
of )
=
{}
: ( ( ) (
empty
V134
()
V135
()
V136
()
V137
()
V138
()
V139
()
V140
() )
set
) holds
X
: ( ( ) ( )
Subset
of )
+
x
: ( ( ) ( )
Point
of ( ( ) ( non
empty
)
set
) ) : ( ( ) ( )
Subset
of )
=
{}
: ( ( ) (
empty
V134
()
V135
()
V136
()
V137
()
V138
()
V139
()
V140
() )
set
) ;
theorem
:: MATHMORP:5
for
T
being ( ( non
empty
right_complementable
Abelian
add-associative
right_zeroed
) ( non
empty
left_complementable
right_complementable
Abelian
add-associative
right_zeroed
V153
() )
RLSStruct
)
for
X
being ( ( ) ( )
Subset
of ) holds
X
: ( ( ) ( )
Subset
of )
(-)
{
(
0.
T
: ( ( non
empty
right_complementable
Abelian
add-associative
right_zeroed
) ( non
empty
left_complementable
right_complementable
Abelian
add-associative
right_zeroed
V153
() )
RLSStruct
)
)
: ( ( ) (
V49
(
b
1
: ( ( non
empty
right_complementable
Abelian
add-associative
right_zeroed
) ( non
empty
left_complementable
right_complementable
Abelian
add-associative
right_zeroed
V153
() )
RLSStruct
) ) )
Element
of the
carrier
of
b
1
: ( ( non
empty
right_complementable
Abelian
add-associative
right_zeroed
) ( non
empty
left_complementable
right_complementable
Abelian
add-associative
right_zeroed
V153
() )
RLSStruct
) : ( ( ) ( non
empty
)
set
) )
}
: ( ( ) ( non
empty
)
Element
of
K32
( the
carrier
of
b
1
: ( ( non
empty
right_complementable
Abelian
add-associative
right_zeroed
) ( non
empty
left_complementable
right_complementable
Abelian
add-associative
right_zeroed
V153
() )
RLSStruct
) : ( ( ) ( non
empty
)
set
) ) : ( ( ) ( )
set
) ) : ( ( ) ( )
Subset
of )
=
X
: ( ( ) ( )
Subset
of ) ;
theorem
:: MATHMORP:6
for
T
being ( ( non
empty
right_complementable
Abelian
add-associative
right_zeroed
) ( non
empty
left_complementable
right_complementable
Abelian
add-associative
right_zeroed
V153
() )
RLSStruct
)
for
X
being ( ( ) ( )
Subset
of ) holds
X
: ( ( ) ( )
Subset
of )
(+)
{
(
0.
T
: ( ( non
empty
right_complementable
Abelian
add-associative
right_zeroed
) ( non
empty
left_complementable
right_complementable
Abelian
add-associative
right_zeroed
V153
() )
RLSStruct
)
)
: ( ( ) (
V49
(
b
1
: ( ( non
empty
right_complementable
Abelian
add-associative
right_zeroed
) ( non
empty
left_complementable
right_complementable
Abelian
add-associative
right_zeroed
V153
() )
RLSStruct
) ) )
Element
of the
carrier
of
b
1
: ( ( non
empty
right_complementable
Abelian
add-associative
right_zeroed
) ( non
empty
left_complementable
right_complementable
Abelian
add-associative
right_zeroed
V153
() )
RLSStruct
) : ( ( ) ( non
empty
)
set
) )
}
: ( ( ) ( non
empty
)
Element
of
K32
( the
carrier
of
b
1
: ( ( non
empty
right_complementable
Abelian
add-associative
right_zeroed
) ( non
empty
left_complementable
right_complementable
Abelian
add-associative
right_zeroed
V153
() )
RLSStruct
) : ( ( ) ( non
empty
)
set
) ) : ( ( ) ( )
set
) ) : ( ( ) ( )
Element
of
K32
( the
carrier
of
b
1
: ( ( non
empty
right_complementable
Abelian
add-associative
right_zeroed
) ( non
empty
left_complementable
right_complementable
Abelian
add-associative
right_zeroed
V153
() )
RLSStruct
) : ( ( ) ( non
empty
)
set
) ) : ( ( ) ( )
set
) )
=
X
: ( ( ) ( )
Subset
of ) ;
theorem
:: MATHMORP:7
for
T
being ( ( non
empty
right_complementable
Abelian
add-associative
right_zeroed
) ( non
empty
left_complementable
right_complementable
Abelian
add-associative
right_zeroed
V153
() )
RLSStruct
)
for
X
being ( ( ) ( )
Subset
of )
for
x
being ( ( ) ( )
Point
of ( ( ) ( non
empty
)
set
) ) holds
X
: ( ( ) ( )
Subset
of )
(+)
{
x
: ( ( ) ( )
Point
of ( ( ) ( non
empty
)
set
) )
}
: ( ( ) ( non
empty
)
Element
of
K32
( the
carrier
of
b
1
: ( ( non
empty
right_complementable
Abelian
add-associative
right_zeroed
) ( non
empty
left_complementable
right_complementable
Abelian
add-associative
right_zeroed
V153
() )
RLSStruct
) : ( ( ) ( non
empty
)
set
) ) : ( ( ) ( )
set
) ) : ( ( ) ( )
Element
of
K32
( the
carrier
of
b
1
: ( ( non
empty
right_complementable
Abelian
add-associative
right_zeroed
) ( non
empty
left_complementable
right_complementable
Abelian
add-associative
right_zeroed
V153
() )
RLSStruct
) : ( ( ) ( non
empty
)
set
) ) : ( ( ) ( )
set
) )
=
X
: ( ( ) ( )
Subset
of )
+
x
: ( ( ) ( )
Point
of ( ( ) ( non
empty
)
set
) ) : ( ( ) ( )
Subset
of ) ;
theorem
:: MATHMORP:8
for
T
being ( ( non
empty
right_complementable
Abelian
add-associative
right_zeroed
) ( non
empty
left_complementable
right_complementable
Abelian
add-associative
right_zeroed
V153
() )
RLSStruct
)
for
X
,
Y
being ( ( ) ( )
Subset
of ) st
Y
: ( ( ) ( )
Subset
of )
=
{}
: ( ( ) (
empty
V134
()
V135
()
V136
()
V137
()
V138
()
V139
()
V140
() )
set
) holds
X
: ( ( ) ( )
Subset
of )
(-)
Y
: ( ( ) ( )
Subset
of ) : ( ( ) ( )
Subset
of )
=
the
carrier
of
T
: ( ( non
empty
right_complementable
Abelian
add-associative
right_zeroed
) ( non
empty
left_complementable
right_complementable
Abelian
add-associative
right_zeroed
V153
() )
RLSStruct
) : ( ( ) ( non
empty
)
set
) ;
theorem
:: MATHMORP:9
for
T
being ( ( non
empty
right_complementable
Abelian
add-associative
right_zeroed
) ( non
empty
left_complementable
right_complementable
Abelian
add-associative
right_zeroed
V153
() )
RLSStruct
)
for
X
,
Y
,
B
being ( ( ) ( )
Subset
of ) st
X
: ( ( ) ( )
Subset
of )
c=
Y
: ( ( ) ( )
Subset
of ) holds
(
X
: ( ( ) ( )
Subset
of )
(-)
B
: ( ( ) ( )
Subset
of ) : ( ( ) ( )
Subset
of )
c=
Y
: ( ( ) ( )
Subset
of )
(-)
B
: ( ( ) ( )
Subset
of ) : ( ( ) ( )
Subset
of ) &
X
: ( ( ) ( )
Subset
of )
(+)
B
: ( ( ) ( )
Subset
of ) : ( ( ) ( )
Element
of
K32
( the
carrier
of
b
1
: ( ( non
empty
right_complementable
Abelian
add-associative
right_zeroed
) ( non
empty
left_complementable
right_complementable
Abelian
add-associative
right_zeroed
V153
() )
RLSStruct
) : ( ( ) ( non
empty
)
set
) ) : ( ( ) ( )
set
) )
c=
Y
: ( ( ) ( )
Subset
of )
(+)
B
: ( ( ) ( )
Subset
of ) : ( ( ) ( )
Element
of
K32
( the
carrier
of
b
1
: ( ( non
empty
right_complementable
Abelian
add-associative
right_zeroed
) ( non
empty
left_complementable
right_complementable
Abelian
add-associative
right_zeroed
V153
() )
RLSStruct
) : ( ( ) ( non
empty
)
set
) ) : ( ( ) ( )
set
) ) ) ;
theorem
:: MATHMORP:10
for
T
being ( ( non
empty
right_complementable
Abelian
add-associative
right_zeroed
) ( non
empty
left_complementable
right_complementable
Abelian
add-associative
right_zeroed
V153
() )
RLSStruct
)
for
B1
,
B2
,
X
being ( ( ) ( )
Subset
of ) st
B1
: ( ( ) ( )
Subset
of )
c=
B2
: ( ( ) ( )
Subset
of ) holds
(
X
: ( ( ) ( )
Subset
of )
(-)
B2
: ( ( ) ( )
Subset
of ) : ( ( ) ( )
Subset
of )
c=
X
: ( ( ) ( )
Subset
of )
(-)
B1
: ( ( ) ( )
Subset
of ) : ( ( ) ( )
Subset
of ) &
X
: ( ( ) ( )
Subset
of )
(+)
B1
: ( ( ) ( )
Subset
of ) : ( ( ) ( )
Element
of
K32
( the
carrier
of
b
1
: ( ( non
empty
right_complementable
Abelian
add-associative
right_zeroed
) ( non
empty
left_complementable
right_complementable
Abelian
add-associative
right_zeroed
V153
() )
RLSStruct
) : ( ( ) ( non
empty
)
set
) ) : ( ( ) ( )
set
) )
c=
X
: ( ( ) ( )
Subset
of )
(+)
B2
: ( ( ) ( )
Subset
of ) : ( ( ) ( )
Element
of
K32
( the
carrier
of
b
1
: ( ( non
empty
right_complementable
Abelian
add-associative
right_zeroed
) ( non
empty
left_complementable
right_complementable
Abelian
add-associative
right_zeroed
V153
() )
RLSStruct
) : ( ( ) ( non
empty
)
set
) ) : ( ( ) ( )
set
) ) ) ;
theorem
:: MATHMORP:11
for
T
being ( ( non
empty
right_complementable
Abelian
add-associative
right_zeroed
) ( non
empty
left_complementable
right_complementable
Abelian
add-associative
right_zeroed
V153
() )
RLSStruct
)
for
B
,
X
being ( ( ) ( )
Subset
of ) st
0.
T
: ( ( non
empty
right_complementable
Abelian
add-associative
right_zeroed
) ( non
empty
left_complementable
right_complementable
Abelian
add-associative
right_zeroed
V153
() )
RLSStruct
) : ( ( ) (
V49
(
b
1
: ( ( non
empty
right_complementable
Abelian
add-associative
right_zeroed
) ( non
empty
left_complementable
right_complementable
Abelian
add-associative
right_zeroed
V153
() )
RLSStruct
) ) )
Element
of the
carrier
of
b
1
: ( ( non
empty
right_complementable
Abelian
add-associative
right_zeroed
) ( non
empty
left_complementable
right_complementable
Abelian
add-associative
right_zeroed
V153
() )
RLSStruct
) : ( ( ) ( non
empty
)
set
) )
in
B
: ( ( ) ( )
Subset
of ) holds
(
X
: ( ( ) ( )
Subset
of )
(-)
B
: ( ( ) ( )
Subset
of ) : ( ( ) ( )
Subset
of )
c=
X
: ( ( ) ( )
Subset
of ) &
X
: ( ( ) ( )
Subset
of )
c=
X
: ( ( ) ( )
Subset
of )
(+)
B
: ( ( ) ( )
Subset
of ) : ( ( ) ( )
Element
of
K32
( the
carrier
of
b
1
: ( ( non
empty
right_complementable
Abelian
add-associative
right_zeroed
) ( non
empty
left_complementable
right_complementable
Abelian
add-associative
right_zeroed
V153
() )
RLSStruct
) : ( ( ) ( non
empty
)
set
) ) : ( ( ) ( )
set
) ) ) ;
theorem
:: MATHMORP:12
for
T
being ( ( non
empty
right_complementable
Abelian
add-associative
right_zeroed
) ( non
empty
left_complementable
right_complementable
Abelian
add-associative
right_zeroed
V153
() )
RLSStruct
)
for
X
,
Y
being ( ( ) ( )
Subset
of ) holds
X
: ( ( ) ( )
Subset
of )
(+)
Y
: ( ( ) ( )
Subset
of ) : ( ( ) ( )
Element
of
K32
( the
carrier
of
b
1
: ( ( non
empty
right_complementable
Abelian
add-associative
right_zeroed
) ( non
empty
left_complementable
right_complementable
Abelian
add-associative
right_zeroed
V153
() )
RLSStruct
) : ( ( ) ( non
empty
)
set
) ) : ( ( ) ( )
set
) )
=
Y
: ( ( ) ( )
Subset
of )
(+)
X
: ( ( ) ( )
Subset
of ) : ( ( ) ( )
Element
of
K32
( the
carrier
of
b
1
: ( ( non
empty
right_complementable
Abelian
add-associative
right_zeroed
) ( non
empty
left_complementable
right_complementable
Abelian
add-associative
right_zeroed
V153
() )
RLSStruct
) : ( ( ) ( non
empty
)
set
) ) : ( ( ) ( )
set
) ) ;
theorem
:: MATHMORP:13
for
T
being ( ( non
empty
right_complementable
Abelian
add-associative
right_zeroed
) ( non
empty
left_complementable
right_complementable
Abelian
add-associative
right_zeroed
V153
() )
RLSStruct
)
for
Y
,
X
being ( ( ) ( )
Subset
of )
for
y
,
x
being ( ( ) ( )
Point
of ( ( ) ( non
empty
)
set
) ) holds
(
Y
: ( ( ) ( )
Subset
of )
+
y
: ( ( ) ( )
Point
of ( ( ) ( non
empty
)
set
) ) : ( ( ) ( )
Subset
of )
c=
X
: ( ( ) ( )
Subset
of )
+
x
: ( ( ) ( )
Point
of ( ( ) ( non
empty
)
set
) ) : ( ( ) ( )
Subset
of ) iff
Y
: ( ( ) ( )
Subset
of )
+
(
y
: ( ( ) ( )
Point
of ( ( ) ( non
empty
)
set
) )
-
x
: ( ( ) ( )
Point
of ( ( ) ( non
empty
)
set
) )
)
: ( ( ) ( )
Element
of the
carrier
of
b
1
: ( ( non
empty
right_complementable
Abelian
add-associative
right_zeroed
) ( non
empty
left_complementable
right_complementable
Abelian
add-associative
right_zeroed
V153
() )
RLSStruct
) : ( ( ) ( non
empty
)
set
) ) : ( ( ) ( )
Subset
of )
c=
X
: ( ( ) ( )
Subset
of ) ) ;
theorem
:: MATHMORP:14
for
T
being ( ( non
empty
right_complementable
Abelian
add-associative
right_zeroed
) ( non
empty
left_complementable
right_complementable
Abelian
add-associative
right_zeroed
V153
() )
RLSStruct
)
for
X
,
Y
being ( ( ) ( )
Subset
of )
for
p
being ( ( ) ( )
Point
of ( ( ) ( non
empty
)
set
) ) holds
(
X
: ( ( ) ( )
Subset
of )
+
p
: ( ( ) ( )
Point
of ( ( ) ( non
empty
)
set
) )
)
: ( ( ) ( )
Subset
of )
(-)
Y
: ( ( ) ( )
Subset
of ) : ( ( ) ( )
Subset
of )
=
(
X
: ( ( ) ( )
Subset
of )
(-)
Y
: ( ( ) ( )
Subset
of )
)
: ( ( ) ( )
Subset
of )
+
p
: ( ( ) ( )
Point
of ( ( ) ( non
empty
)
set
) ) : ( ( ) ( )
Subset
of ) ;
theorem
:: MATHMORP:15
for
T
being ( ( non
empty
right_complementable
Abelian
add-associative
right_zeroed
) ( non
empty
left_complementable
right_complementable
Abelian
add-associative
right_zeroed
V153
() )
RLSStruct
)
for
X
,
Y
being ( ( ) ( )
Subset
of )
for
p
being ( ( ) ( )
Point
of ( ( ) ( non
empty
)
set
) ) holds
(
X
: ( ( ) ( )
Subset
of )
+
p
: ( ( ) ( )
Point
of ( ( ) ( non
empty
)
set
) )
)
: ( ( ) ( )
Subset
of )
(+)
Y
: ( ( ) ( )
Subset
of ) : ( ( ) ( )
Element
of
K32
( the
carrier
of
b
1
: ( ( non
empty
right_complementable
Abelian
add-associative
right_zeroed
) ( non
empty
left_complementable
right_complementable
Abelian
add-associative
right_zeroed
V153
() )
RLSStruct
) : ( ( ) ( non
empty
)
set
) ) : ( ( ) ( )
set
) )
=
(
X
: ( ( ) ( )
Subset
of )
(+)
Y
: ( ( ) ( )
Subset
of )
)
: ( ( ) ( )
Element
of
K32
( the
carrier
of
b
1
: ( ( non
empty
right_complementable
Abelian
add-associative
right_zeroed
) ( non
empty
left_complementable
right_complementable
Abelian
add-associative
right_zeroed
V153
() )
RLSStruct
) : ( ( ) ( non
empty
)
set
) ) : ( ( ) ( )
set
) )
+
p
: ( ( ) ( )
Point
of ( ( ) ( non
empty
)
set
) ) : ( ( ) ( )
Subset
of ) ;
theorem
:: MATHMORP:16
for
T
being ( ( non
empty
right_complementable
Abelian
add-associative
right_zeroed
) ( non
empty
left_complementable
right_complementable
Abelian
add-associative
right_zeroed
V153
() )
RLSStruct
)
for
X
being ( ( ) ( )
Subset
of )
for
x
,
y
being ( ( ) ( )
Point
of ( ( ) ( non
empty
)
set
) ) holds
(
X
: ( ( ) ( )
Subset
of )
+
x
: ( ( ) ( )
Point
of ( ( ) ( non
empty
)
set
) )
)
: ( ( ) ( )
Subset
of )
+
y
: ( ( ) ( )
Point
of ( ( ) ( non
empty
)
set
) ) : ( ( ) ( )
Subset
of )
=
X
: ( ( ) ( )
Subset
of )
+
(
x
: ( ( ) ( )
Point
of ( ( ) ( non
empty
)
set
) )
+
y
: ( ( ) ( )
Point
of ( ( ) ( non
empty
)
set
) )
)
: ( ( ) ( )
Element
of the
carrier
of
b
1
: ( ( non
empty
right_complementable
Abelian
add-associative
right_zeroed
) ( non
empty
left_complementable
right_complementable
Abelian
add-associative
right_zeroed
V153
() )
RLSStruct
) : ( ( ) ( non
empty
)
set
) ) : ( ( ) ( )
Subset
of ) ;
theorem
:: MATHMORP:17
for
T
being ( ( non
empty
right_complementable
Abelian
add-associative
right_zeroed
) ( non
empty
left_complementable
right_complementable
Abelian
add-associative
right_zeroed
V153
() )
RLSStruct
)
for
X
,
Y
being ( ( ) ( )
Subset
of )
for
p
being ( ( ) ( )
Point
of ( ( ) ( non
empty
)
set
) ) holds
X
: ( ( ) ( )
Subset
of )
(-)
(
Y
: ( ( ) ( )
Subset
of )
+
p
: ( ( ) ( )
Point
of ( ( ) ( non
empty
)
set
) )
)
: ( ( ) ( )
Subset
of ) : ( ( ) ( )
Subset
of )
=
(
X
: ( ( ) ( )
Subset
of )
(-)
Y
: ( ( ) ( )
Subset
of )
)
: ( ( ) ( )
Subset
of )
+
(
-
p
: ( ( ) ( )
Point
of ( ( ) ( non
empty
)
set
) )
)
: ( ( ) ( )
Element
of the
carrier
of
b
1
: ( ( non
empty
right_complementable
Abelian
add-associative
right_zeroed
) ( non
empty
left_complementable
right_complementable
Abelian
add-associative
right_zeroed
V153
() )
RLSStruct
) : ( ( ) ( non
empty
)
set
) ) : ( ( ) ( )
Subset
of ) ;
theorem
:: MATHMORP:18
for
T
being ( ( non
empty
right_complementable
Abelian
add-associative
right_zeroed
) ( non
empty
left_complementable
right_complementable
Abelian
add-associative
right_zeroed
V153
() )
RLSStruct
)
for
X
,
Y
being ( ( ) ( )
Subset
of )
for
p
being ( ( ) ( )
Point
of ( ( ) ( non
empty
)
set
) ) holds
X
: ( ( ) ( )
Subset
of )
(+)
(
Y
: ( ( ) ( )
Subset
of )
+
p
: ( ( ) ( )
Point
of ( ( ) ( non
empty
)
set
) )
)
: ( ( ) ( )
Subset
of ) : ( ( ) ( )
Element
of
K32
( the
carrier
of
b
1
: ( ( non
empty
right_complementable
Abelian
add-associative
right_zeroed
) ( non
empty
left_complementable
right_complementable
Abelian
add-associative
right_zeroed
V153
() )
RLSStruct
) : ( ( ) ( non
empty
)
set
) ) : ( ( ) ( )
set
) )
=
(
X
: ( ( ) ( )
Subset
of )
(+)
Y
: ( ( ) ( )
Subset
of )
)
: ( ( ) ( )
Element
of
K32
( the
carrier
of
b
1
: ( ( non
empty
right_complementable
Abelian
add-associative
right_zeroed
) ( non
empty
left_complementable
right_complementable
Abelian
add-associative
right_zeroed
V153
() )
RLSStruct
) : ( ( ) ( non
empty
)
set
) ) : ( ( ) ( )
set
) )
+
p
: ( ( ) ( )
Point
of ( ( ) ( non
empty
)
set
) ) : ( ( ) ( )
Subset
of ) ;
theorem
:: MATHMORP:19
for
T
being ( ( non
empty
right_complementable
Abelian
add-associative
right_zeroed
) ( non
empty
left_complementable
right_complementable
Abelian
add-associative
right_zeroed
V153
() )
RLSStruct
)
for
X
,
B
being ( ( ) ( )
Subset
of )
for
x
being ( ( ) ( )
Point
of ( ( ) ( non
empty
)
set
) ) st
x
: ( ( ) ( )
Point
of ( ( ) ( non
empty
)
set
) )
in
X
: ( ( ) ( )
Subset
of ) holds
B
: ( ( ) ( )
Subset
of )
+
x
: ( ( ) ( )
Point
of ( ( ) ( non
empty
)
set
) ) : ( ( ) ( )
Subset
of )
c=
B
: ( ( ) ( )
Subset
of )
(+)
X
: ( ( ) ( )
Subset
of ) : ( ( ) ( )
Element
of
K32
( the
carrier
of
b
1
: ( ( non
empty
right_complementable
Abelian
add-associative
right_zeroed
) ( non
empty
left_complementable
right_complementable
Abelian
add-associative
right_zeroed
V153
() )
RLSStruct
) : ( ( ) ( non
empty
)
set
) ) : ( ( ) ( )
set
) ) ;
theorem
:: MATHMORP:20
for
T
being ( ( non
empty
right_complementable
Abelian
add-associative
right_zeroed
) ( non
empty
left_complementable
right_complementable
Abelian
add-associative
right_zeroed
V153
() )
RLSStruct
)
for
X
,
B
being ( ( ) ( )
Subset
of ) holds
X
: ( ( ) ( )
Subset
of )
c=
(
X
: ( ( ) ( )
Subset
of )
(+)
B
: ( ( ) ( )
Subset
of )
)
: ( ( ) ( )
Element
of
K32
( the
carrier
of
b
1
: ( ( non
empty
right_complementable
Abelian
add-associative
right_zeroed
) ( non
empty
left_complementable
right_complementable
Abelian
add-associative
right_zeroed
V153
() )
RLSStruct
) : ( ( ) ( non
empty
)
set
) ) : ( ( ) ( )
set
) )
(-)
B
: ( ( ) ( )
Subset
of ) : ( ( ) ( )
Subset
of ) ;
theorem
:: MATHMORP:21
for
T
being ( ( non
empty
right_complementable
Abelian
add-associative
right_zeroed
) ( non
empty
left_complementable
right_complementable
Abelian
add-associative
right_zeroed
V153
() )
RLSStruct
)
for
X
being ( ( ) ( )
Subset
of ) holds
X
: ( ( ) ( )
Subset
of )
+
(
0.
T
: ( ( non
empty
right_complementable
Abelian
add-associative
right_zeroed
) ( non
empty
left_complementable
right_complementable
Abelian
add-associative
right_zeroed
V153
() )
RLSStruct
)
)
: ( ( ) (
V49
(
b
1
: ( ( non
empty
right_complementable
Abelian
add-associative
right_zeroed
) ( non
empty
left_complementable
right_complementable
Abelian
add-associative
right_zeroed
V153
() )
RLSStruct
) ) )
Element
of the
carrier
of
b
1
: ( ( non
empty
right_complementable
Abelian
add-associative
right_zeroed
) ( non
empty
left_complementable
right_complementable
Abelian
add-associative
right_zeroed
V153
() )
RLSStruct
) : ( ( ) ( non
empty
)
set
) ) : ( ( ) ( )
Subset
of )
=
X
: ( ( ) ( )
Subset
of ) ;
theorem
:: MATHMORP:22
for
T
being ( ( non
empty
right_complementable
Abelian
add-associative
right_zeroed
) ( non
empty
left_complementable
right_complementable
Abelian
add-associative
right_zeroed
V153
() )
RLSStruct
)
for
X
being ( ( ) ( )
Subset
of )
for
x
being ( ( ) ( )
Point
of ( ( ) ( non
empty
)
set
) ) holds
X
: ( ( ) ( )
Subset
of )
(-)
{
x
: ( ( ) ( )
Point
of ( ( ) ( non
empty
)
set
) )
}
: ( ( ) ( non
empty
)
Element
of
K32
( the
carrier
of
b
1
: ( ( non
empty
right_complementable
Abelian
add-associative
right_zeroed
) ( non
empty
left_complementable
right_complementable
Abelian
add-associative
right_zeroed
V153
() )
RLSStruct
) : ( ( ) ( non
empty
)
set
) ) : ( ( ) ( )
set
) ) : ( ( ) ( )
Subset
of )
=
X
: ( ( ) ( )
Subset
of )
+
(
-
x
: ( ( ) ( )
Point
of ( ( ) ( non
empty
)
set
) )
)
: ( ( ) ( )
Element
of the
carrier
of
b
1
: ( ( non
empty
right_complementable
Abelian
add-associative
right_zeroed
) ( non
empty
left_complementable
right_complementable
Abelian
add-associative
right_zeroed
V153
() )
RLSStruct
) : ( ( ) ( non
empty
)
set
) ) : ( ( ) ( )
Subset
of ) ;
theorem
:: MATHMORP:23
for
T
being ( ( non
empty
right_complementable
Abelian
add-associative
right_zeroed
) ( non
empty
left_complementable
right_complementable
Abelian
add-associative
right_zeroed
V153
() )
RLSStruct
)
for
X
,
Y
,
Z
being ( ( ) ( )
Subset
of ) holds
X
: ( ( ) ( )
Subset
of )
(-)
(
Y
: ( ( ) ( )
Subset
of )
(+)
Z
: ( ( ) ( )
Subset
of )
)
: ( ( ) ( )
Element
of
K32
( the
carrier
of
b
1
: ( ( non
empty
right_complementable
Abelian
add-associative
right_zeroed
) ( non
empty
left_complementable
right_complementable
Abelian
add-associative
right_zeroed
V153
() )
RLSStruct
) : ( ( ) ( non
empty
)
set
) ) : ( ( ) ( )
set
) ) : ( ( ) ( )
Subset
of )
=
(
X
: ( ( ) ( )
Subset
of )
(-)
Y
: ( ( ) ( )
Subset
of )
)
: ( ( ) ( )
Subset
of )
(-)
Z
: ( ( ) ( )
Subset
of ) : ( ( ) ( )
Subset
of ) ;
theorem
:: MATHMORP:24
for
T
being ( ( non
empty
right_complementable
Abelian
add-associative
right_zeroed
) ( non
empty
left_complementable
right_complementable
Abelian
add-associative
right_zeroed
V153
() )
RLSStruct
)
for
X
,
Y
,
Z
being ( ( ) ( )
Subset
of ) holds
X
: ( ( ) ( )
Subset
of )
(-)
(
Y
: ( ( ) ( )
Subset
of )
(+)
Z
: ( ( ) ( )
Subset
of )
)
: ( ( ) ( )
Element
of
K32
( the
carrier
of
b
1
: ( ( non
empty
right_complementable
Abelian
add-associative
right_zeroed
) ( non
empty
left_complementable
right_complementable
Abelian
add-associative
right_zeroed
V153
() )
RLSStruct
) : ( ( ) ( non
empty
)
set
) ) : ( ( ) ( )
set
) ) : ( ( ) ( )
Subset
of )
=
(
X
: ( ( ) ( )
Subset
of )
(-)
Z
: ( ( ) ( )
Subset
of )
)
: ( ( ) ( )
Subset
of )
(-)
Y
: ( ( ) ( )
Subset
of ) : ( ( ) ( )
Subset
of ) ;
theorem
:: MATHMORP:25
for
T
being ( ( non
empty
right_complementable
Abelian
add-associative
right_zeroed
) ( non
empty
left_complementable
right_complementable
Abelian
add-associative
right_zeroed
V153
() )
RLSStruct
)
for
X
,
Y
,
Z
being ( ( ) ( )
Subset
of ) holds
X
: ( ( ) ( )
Subset
of )
(+)
(
Y
: ( ( ) ( )
Subset
of )
(-)
Z
: ( ( ) ( )
Subset
of )
)
: ( ( ) ( )
Subset
of ) : ( ( ) ( )
Element
of
K32
( the
carrier
of
b
1
: ( ( non
empty
right_complementable
Abelian
add-associative
right_zeroed
) ( non
empty
left_complementable
right_complementable
Abelian
add-associative
right_zeroed
V153
() )
RLSStruct
) : ( ( ) ( non
empty
)
set
) ) : ( ( ) ( )
set
) )
c=
(
X
: ( ( ) ( )
Subset
of )
(+)
Y
: ( ( ) ( )
Subset
of )
)
: ( ( ) ( )
Element
of
K32
( the
carrier
of
b
1
: ( ( non
empty
right_complementable
Abelian
add-associative
right_zeroed
) ( non
empty
left_complementable
right_complementable
Abelian
add-associative
right_zeroed
V153
() )
RLSStruct
) : ( ( ) ( non
empty
)
set
) ) : ( ( ) ( )
set
) )
(-)
Z
: ( ( ) ( )
Subset
of ) : ( ( ) ( )
Subset
of ) ;
theorem
:: MATHMORP:26
for
T
being ( ( non
empty
right_complementable
Abelian
add-associative
right_zeroed
) ( non
empty
left_complementable
right_complementable
Abelian
add-associative
right_zeroed
V153
() )
RLSStruct
)
for
X
,
Y
,
Z
being ( ( ) ( )
Subset
of ) holds
X
: ( ( ) ( )
Subset
of )
(+)
(
Y
: ( ( ) ( )
Subset
of )
(+)
Z
: ( ( ) ( )
Subset
of )
)
: ( ( ) ( )
Element
of
K32
( the
carrier
of
b
1
: ( ( non
empty
right_complementable
Abelian
add-associative
right_zeroed
) ( non
empty
left_complementable
right_complementable
Abelian
add-associative
right_zeroed
V153
() )
RLSStruct
) : ( ( ) ( non
empty
)
set
) ) : ( ( ) ( )
set
) ) : ( ( ) ( )
Element
of
K32
( the
carrier
of
b
1
: ( ( non
empty
right_complementable
Abelian
add-associative
right_zeroed
) ( non
empty
left_complementable
right_complementable
Abelian
add-associative
right_zeroed
V153
() )
RLSStruct
) : ( ( ) ( non
empty
)
set
) ) : ( ( ) ( )
set
) )
=
(
X
: ( ( ) ( )
Subset
of )
(+)
Y
: ( ( ) ( )
Subset
of )
)
: ( ( ) ( )
Element
of
K32
( the
carrier
of
b
1
: ( ( non
empty
right_complementable
Abelian
add-associative
right_zeroed
) ( non
empty
left_complementable
right_complementable
Abelian
add-associative
right_zeroed
V153
() )
RLSStruct
) : ( ( ) ( non
empty
)
set
) ) : ( ( ) ( )
set
) )
(+)
Z
: ( ( ) ( )
Subset
of ) : ( ( ) ( )
Element
of
K32
( the
carrier
of
b
1
: ( ( non
empty
right_complementable
Abelian
add-associative
right_zeroed
) ( non
empty
left_complementable
right_complementable
Abelian
add-associative
right_zeroed
V153
() )
RLSStruct
) : ( ( ) ( non
empty
)
set
) ) : ( ( ) ( )
set
) ) ;
theorem
:: MATHMORP:27
for
T
being ( ( non
empty
right_complementable
Abelian
add-associative
right_zeroed
) ( non
empty
left_complementable
right_complementable
Abelian
add-associative
right_zeroed
V153
() )
RLSStruct
)
for
B
,
C
being ( ( ) ( )
Subset
of )
for
y
being ( ( ) ( )
Point
of ( ( ) ( non
empty
)
set
) ) holds
(
B
: ( ( ) ( )
Subset
of )
\/
C
: ( ( ) ( )
Subset
of )
)
: ( ( ) ( )
Element
of
K32
( the
carrier
of
b
1
: ( ( non
empty
right_complementable
Abelian
add-associative
right_zeroed
) ( non
empty
left_complementable
right_complementable
Abelian
add-associative
right_zeroed
V153
() )
RLSStruct
) : ( ( ) ( non
empty
)
set
) ) : ( ( ) ( )
set
) )
+
y
: ( ( ) ( )
Point
of ( ( ) ( non
empty
)
set
) ) : ( ( ) ( )
Subset
of )
=
(
B
: ( ( ) ( )
Subset
of )
+
y
: ( ( ) ( )
Point
of ( ( ) ( non
empty
)
set
) )
)
: ( ( ) ( )
Subset
of )
\/
(
C
: ( ( ) ( )
Subset
of )
+
y
: ( ( ) ( )
Point
of ( ( ) ( non
empty
)
set
) )
)
: ( ( ) ( )
Subset
of ) : ( ( ) ( )
Element
of
K32
( the
carrier
of
b
1
: ( ( non
empty
right_complementable
Abelian
add-associative
right_zeroed
) ( non
empty
left_complementable
right_complementable
Abelian
add-associative
right_zeroed
V153
() )
RLSStruct
) : ( ( ) ( non
empty
)
set
) ) : ( ( ) ( )
set
) ) ;
theorem
:: MATHMORP:28
for
T
being ( ( non
empty
right_complementable
Abelian
add-associative
right_zeroed
) ( non
empty
left_complementable
right_complementable
Abelian
add-associative
right_zeroed
V153
() )
RLSStruct
)
for
B
,
C
being ( ( ) ( )
Subset
of )
for
y
being ( ( ) ( )
Point
of ( ( ) ( non
empty
)
set
) ) holds
(
B
: ( ( ) ( )
Subset
of )
/\
C
: ( ( ) ( )
Subset
of )
)
: ( ( ) ( )
Element
of
K32
( the
carrier
of
b
1
: ( ( non
empty
right_complementable
Abelian
add-associative
right_zeroed
) ( non
empty
left_complementable
right_complementable
Abelian
add-associative
right_zeroed
V153
() )
RLSStruct
) : ( ( ) ( non
empty
)
set
) ) : ( ( ) ( )
set
) )
+
y
: ( ( ) ( )
Point
of ( ( ) ( non
empty
)
set
) ) : ( ( ) ( )
Subset
of )
=
(
B
: ( ( ) ( )
Subset
of )
+
y
: ( ( ) ( )
Point
of ( ( ) ( non
empty
)
set
) )
)
: ( ( ) ( )
Subset
of )
/\
(
C
: ( ( ) ( )
Subset
of )
+
y
: ( ( ) ( )
Point
of ( ( ) ( non
empty
)
set
) )
)
: ( ( ) ( )
Subset
of ) : ( ( ) ( )
Element
of
K32
( the
carrier
of
b
1
: ( ( non
empty
right_complementable
Abelian
add-associative
right_zeroed
) ( non
empty
left_complementable
right_complementable
Abelian
add-associative
right_zeroed
V153
() )
RLSStruct
) : ( ( ) ( non
empty
)
set
) ) : ( ( ) ( )
set
) ) ;
theorem
:: MATHMORP:29
for
T
being ( ( non
empty
right_complementable
Abelian
add-associative
right_zeroed
) ( non
empty
left_complementable
right_complementable
Abelian
add-associative
right_zeroed
V153
() )
RLSStruct
)
for
X
,
B
,
C
being ( ( ) ( )
Subset
of ) holds
X
: ( ( ) ( )
Subset
of )
(-)
(
B
: ( ( ) ( )
Subset
of )
\/
C
: ( ( ) ( )
Subset
of )
)
: ( ( ) ( )
Element
of
K32
( the
carrier
of
b
1
: ( ( non
empty
right_complementable
Abelian
add-associative
right_zeroed
) ( non
empty
left_complementable
right_complementable
Abelian
add-associative
right_zeroed
V153
() )
RLSStruct
) : ( ( ) ( non
empty
)
set
) ) : ( ( ) ( )
set
) ) : ( ( ) ( )
Subset
of )
=
(
X
: ( ( ) ( )
Subset
of )
(-)
B
: ( ( ) ( )
Subset
of )
)
: ( ( ) ( )
Subset
of )
/\
(
X
: ( ( ) ( )
Subset
of )
(-)
C
: ( ( ) ( )
Subset
of )
)
: ( ( ) ( )
Subset
of ) : ( ( ) ( )
Element
of
K32
( the
carrier
of
b
1
: ( ( non
empty
right_complementable
Abelian
add-associative
right_zeroed
) ( non
empty
left_complementable
right_complementable
Abelian
add-associative
right_zeroed
V153
() )
RLSStruct
) : ( ( ) ( non
empty
)
set
) ) : ( ( ) ( )
set
) ) ;
theorem
:: MATHMORP:30
for
T
being ( ( non
empty
right_complementable
Abelian
add-associative
right_zeroed
) ( non
empty
left_complementable
right_complementable
Abelian
add-associative
right_zeroed
V153
() )
RLSStruct
)
for
X
,
B
,
C
being ( ( ) ( )
Subset
of ) holds
X
: ( ( ) ( )
Subset
of )
(+)
(
B
: ( ( ) ( )
Subset
of )
\/
C
: ( ( ) ( )
Subset
of )
)
: ( ( ) ( )
Element
of
K32
( the
carrier
of
b
1
: ( ( non
empty
right_complementable
Abelian
add-associative
right_zeroed
) ( non
empty
left_complementable
right_complementable
Abelian
add-associative
right_zeroed
V153
() )
RLSStruct
) : ( ( ) ( non
empty
)
set
) ) : ( ( ) ( )
set
) ) : ( ( ) ( )
Element
of
K32
( the
carrier
of
b
1
: ( ( non
empty
right_complementable
Abelian
add-associative
right_zeroed
) ( non
empty
left_complementable
right_complementable
Abelian
add-associative
right_zeroed
V153
() )
RLSStruct
) : ( ( ) ( non
empty
)
set
) ) : ( ( ) ( )
set
) )
=
(
X
: ( ( ) ( )
Subset
of )
(+)
B
: ( ( ) ( )
Subset
of )
)
: ( ( ) ( )
Element
of
K32
( the
carrier
of
b
1
: ( ( non
empty
right_complementable
Abelian
add-associative
right_zeroed
) ( non
empty
left_complementable
right_complementable
Abelian
add-associative
right_zeroed
V153
() )
RLSStruct
) : ( ( ) ( non
empty
)
set
) ) : ( ( ) ( )
set
) )
\/
(
X
: ( ( ) ( )
Subset
of )
(+)
C
: ( ( ) ( )
Subset
of )
)
: ( ( ) ( )
Element
of
K32
( the
carrier
of
b
1
: ( ( non
empty
right_complementable
Abelian
add-associative
right_zeroed
) ( non
empty
left_complementable
right_complementable
Abelian
add-associative
right_zeroed
V153
() )
RLSStruct
) : ( ( ) ( non
empty
)
set
) ) : ( ( ) ( )
set
) ) : ( ( ) ( )
Element
of
K32
( the
carrier
of
b
1
: ( ( non
empty
right_complementable
Abelian
add-associative
right_zeroed
) ( non
empty
left_complementable
right_complementable
Abelian
add-associative
right_zeroed
V153
() )
RLSStruct
) : ( ( ) ( non
empty
)
set
) ) : ( ( ) ( )
set
) ) ;
theorem
:: MATHMORP:31
for
T
being ( ( non
empty
right_complementable
Abelian
add-associative
right_zeroed
) ( non
empty
left_complementable
right_complementable
Abelian
add-associative
right_zeroed
V153
() )
RLSStruct
)
for
X
,
B
,
Y
being ( ( ) ( )
Subset
of ) holds
(
X
: ( ( ) ( )
Subset
of )
(-)
B
: ( ( ) ( )
Subset
of )
)
: ( ( ) ( )
Subset
of )
\/
(
Y
: ( ( ) ( )
Subset
of )
(-)
B
: ( ( ) ( )
Subset
of )
)
: ( ( ) ( )
Subset
of ) : ( ( ) ( )
Element
of
K32
( the
carrier
of
b
1
: ( ( non
empty
right_complementable
Abelian
add-associative
right_zeroed
) ( non
empty
left_complementable
right_complementable
Abelian
add-associative
right_zeroed
V153
() )
RLSStruct
) : ( ( ) ( non
empty
)
set
) ) : ( ( ) ( )
set
) )
c=
(
X
: ( ( ) ( )
Subset
of )
\/
Y
: ( ( ) ( )
Subset
of )
)
: ( ( ) ( )
Element
of
K32
( the
carrier
of
b
1
: ( ( non
empty
right_complementable
Abelian
add-associative
right_zeroed
) ( non
empty
left_complementable
right_complementable
Abelian
add-associative
right_zeroed
V153
() )
RLSStruct
) : ( ( ) ( non
empty
)
set
) ) : ( ( ) ( )
set
) )
(-)
B
: ( ( ) ( )
Subset
of ) : ( ( ) ( )
Subset
of ) ;
theorem
:: MATHMORP:32
for
T
being ( ( non
empty
right_complementable
Abelian
add-associative
right_zeroed
) ( non
empty
left_complementable
right_complementable
Abelian
add-associative
right_zeroed
V153
() )
RLSStruct
)
for
X
,
Y
,
B
being ( ( ) ( )
Subset
of ) holds
(
X
: ( ( ) ( )
Subset
of )
\/
Y
: ( ( ) ( )
Subset
of )
)
: ( ( ) ( )
Element
of
K32
( the
carrier
of
b
1
: ( ( non
empty
right_complementable
Abelian
add-associative
right_zeroed
) ( non
empty
left_complementable
right_complementable
Abelian
add-associative
right_zeroed
V153
() )
RLSStruct
) : ( ( ) ( non
empty
)
set
) ) : ( ( ) ( )
set
) )
(+)
B
: ( ( ) ( )
Subset
of ) : ( ( ) ( )
Element
of
K32
( the
carrier
of
b
1
: ( ( non
empty
right_complementable
Abelian
add-associative
right_zeroed
) ( non
empty
left_complementable
right_complementable
Abelian
add-associative
right_zeroed
V153
() )
RLSStruct
) : ( ( ) ( non
empty
)
set
) ) : ( ( ) ( )
set
) )
=
(
X
: ( ( ) ( )
Subset
of )
(+)
B
: ( ( ) ( )
Subset
of )
)
: ( ( ) ( )
Element
of
K32
( the
carrier
of
b
1
: ( ( non
empty
right_complementable
Abelian
add-associative
right_zeroed
) ( non
empty
left_complementable
right_complementable
Abelian
add-associative
right_zeroed
V153
() )
RLSStruct
) : ( ( ) ( non
empty
)
set
) ) : ( ( ) ( )
set
) )
\/
(
Y
: ( ( ) ( )
Subset
of )
(+)
B
: ( ( ) ( )
Subset
of )
)
: ( ( ) ( )
Element
of
K32
( the
carrier
of
b
1
: ( ( non
empty
right_complementable
Abelian
add-associative
right_zeroed
) ( non
empty
left_complementable
right_complementable
Abelian
add-associative
right_zeroed
V153
() )
RLSStruct
) : ( ( ) ( non
empty
)
set
) ) : ( ( ) ( )
set
) ) : ( ( ) ( )
Element
of
K32
( the
carrier
of
b
1
: ( ( non
empty
right_complementable
Abelian
add-associative
right_zeroed
) ( non
empty
left_complementable
right_complementable
Abelian
add-associative
right_zeroed
V153
() )
RLSStruct
) : ( ( ) ( non
empty
)
set
) ) : ( ( ) ( )
set
) ) ;
theorem
:: MATHMORP:33
for
T
being ( ( non
empty
right_complementable
Abelian
add-associative
right_zeroed
) ( non
empty
left_complementable
right_complementable
Abelian
add-associative
right_zeroed
V153
() )
RLSStruct
)
for
X
,
Y
,
B
being ( ( ) ( )
Subset
of ) holds
(
X
: ( ( ) ( )
Subset
of )
/\
Y
: ( ( ) ( )
Subset
of )
)
: ( ( ) ( )
Element
of
K32
( the
carrier
of
b
1
: ( ( non
empty
right_complementable
Abelian
add-associative
right_zeroed
) ( non
empty
left_complementable
right_complementable
Abelian
add-associative
right_zeroed
V153
() )
RLSStruct
) : ( ( ) ( non
empty
)
set
) ) : ( ( ) ( )
set
) )
(-)
B
: ( ( ) ( )
Subset
of ) : ( ( ) ( )
Subset
of )
=
(
X
: ( ( ) ( )
Subset
of )
(-)
B
: ( ( ) ( )
Subset
of )
)
: ( ( ) ( )
Subset
of )
/\
(
Y
: ( ( ) ( )
Subset
of )
(-)
B
: ( ( ) ( )
Subset
of )
)
: ( ( ) ( )
Subset
of ) : ( ( ) ( )
Element
of
K32
( the
carrier
of
b
1
: ( ( non
empty
right_complementable
Abelian
add-associative
right_zeroed
) ( non
empty
left_complementable
right_complementable
Abelian
add-associative
right_zeroed
V153
() )
RLSStruct
) : ( ( ) ( non
empty
)
set
) ) : ( ( ) ( )
set
) ) ;
theorem
:: MATHMORP:34
for
T
being ( ( non
empty
right_complementable
Abelian
add-associative
right_zeroed
) ( non
empty
left_complementable
right_complementable
Abelian
add-associative
right_zeroed
V153
() )
RLSStruct
)
for
X
,
Y
,
B
being ( ( ) ( )
Subset
of ) holds
(
X
: ( ( ) ( )
Subset
of )
/\
Y
: ( ( ) ( )
Subset
of )
)
: ( ( ) ( )
Element
of
K32
( the
carrier
of
b
1
: ( ( non
empty
right_complementable
Abelian
add-associative
right_zeroed
) ( non
empty
left_complementable
right_complementable
Abelian
add-associative
right_zeroed
V153
() )
RLSStruct
) : ( ( ) ( non
empty
)
set
) ) : ( ( ) ( )
set
) )
(+)
B
: ( ( ) ( )
Subset
of ) : ( ( ) ( )
Element
of
K32
( the
carrier
of
b
1
: ( ( non
empty
right_complementable
Abelian
add-associative
right_zeroed
) ( non
empty
left_complementable
right_complementable
Abelian
add-associative
right_zeroed
V153
() )
RLSStruct
) : ( ( ) ( non
empty
)
set
) ) : ( ( ) ( )
set
) )
c=
(
X
: ( ( ) ( )
Subset
of )
(+)
B
: ( ( ) ( )
Subset
of )
)
: ( ( ) ( )
Element
of
K32
( the
carrier
of
b
1
: ( ( non
empty
right_complementable
Abelian
add-associative
right_zeroed
) ( non
empty
left_complementable
right_complementable
Abelian
add-associative
right_zeroed
V153
() )
RLSStruct
) : ( ( ) ( non
empty
)
set
) ) : ( ( ) ( )
set
) )
/\
(
Y
: ( ( ) ( )
Subset
of )
(+)
B
: ( ( ) ( )
Subset
of )
)
: ( ( ) ( )
Element
of
K32
( the
carrier
of
b
1
: ( ( non
empty
right_complementable
Abelian
add-associative
right_zeroed
) ( non
empty
left_complementable
right_complementable
Abelian
add-associative
right_zeroed
V153
() )
RLSStruct
) : ( ( ) ( non
empty
)
set
) ) : ( ( ) ( )
set
) ) : ( ( ) ( )
Element
of
K32
( the
carrier
of
b
1
: ( ( non
empty
right_complementable
Abelian
add-associative
right_zeroed
) ( non
empty
left_complementable
right_complementable
Abelian
add-associative
right_zeroed
V153
() )
RLSStruct
) : ( ( ) ( non
empty
)
set
) ) : ( ( ) ( )
set
) ) ;
theorem
:: MATHMORP:35
for
T
being ( ( non
empty
right_complementable
Abelian
add-associative
right_zeroed
) ( non
empty
left_complementable
right_complementable
Abelian
add-associative
right_zeroed
V153
() )
RLSStruct
)
for
B
,
X
,
Y
being ( ( ) ( )
Subset
of ) holds
B
: ( ( ) ( )
Subset
of )
(+)
(
X
: ( ( ) ( )
Subset
of )
/\
Y
: ( ( ) ( )
Subset
of )
)
: ( ( ) ( )
Element
of
K32
( the
carrier
of
b
1
: ( ( non
empty
right_complementable
Abelian
add-associative
right_zeroed
) ( non
empty
left_complementable
right_complementable
Abelian
add-associative
right_zeroed
V153
() )
RLSStruct
) : ( ( ) ( non
empty
)
set
) ) : ( ( ) ( )
set
) ) : ( ( ) ( )
Element
of
K32
( the
carrier
of
b
1
: ( ( non
empty
right_complementable
Abelian
add-associative
right_zeroed
) ( non
empty
left_complementable
right_complementable
Abelian
add-associative
right_zeroed
V153
() )
RLSStruct
) : ( ( ) ( non
empty
)
set
) ) : ( ( ) ( )
set
) )
c=
(
B
: ( ( ) ( )
Subset
of )
(+)
X
: ( ( ) ( )
Subset
of )
)
: ( ( ) ( )
Element
of
K32
( the
carrier
of
b
1
: ( ( non
empty
right_complementable
Abelian
add-associative
right_zeroed
) ( non
empty
left_complementable
right_complementable
Abelian
add-associative
right_zeroed
V153
() )
RLSStruct
) : ( ( ) ( non
empty
)
set
) ) : ( ( ) ( )
set
) )
/\
(
B
: ( ( ) ( )
Subset
of )
(+)
Y
: ( ( ) ( )
Subset
of )
)
: ( ( ) ( )
Element
of
K32
( the
carrier
of
b
1
: ( ( non
empty
right_complementable
Abelian
add-associative
right_zeroed
) ( non
empty
left_complementable
right_complementable
Abelian
add-associative
right_zeroed
V153
() )
RLSStruct
) : ( ( ) ( non
empty
)
set
) ) : ( ( ) ( )
set
) ) : ( ( ) ( )
Element
of
K32
( the
carrier
of
b
1
: ( ( non
empty
right_complementable
Abelian
add-associative
right_zeroed
) ( non
empty
left_complementable
right_complementable
Abelian
add-associative
right_zeroed
V153
() )
RLSStruct
) : ( ( ) ( non
empty
)
set
) ) : ( ( ) ( )
set
) ) ;
theorem
:: MATHMORP:36
for
T
being ( ( non
empty
right_complementable
Abelian
add-associative
right_zeroed
) ( non
empty
left_complementable
right_complementable
Abelian
add-associative
right_zeroed
V153
() )
RLSStruct
)
for
B
,
X
,
Y
being ( ( ) ( )
Subset
of ) holds
(
B
: ( ( ) ( )
Subset
of )
(-)
X
: ( ( ) ( )
Subset
of )
)
: ( ( ) ( )
Subset
of )
\/
(
B
: ( ( ) ( )
Subset
of )
(-)
Y
: ( ( ) ( )
Subset
of )
)
: ( ( ) ( )
Subset
of ) : ( ( ) ( )
Element
of
K32
( the
carrier
of
b
1
: ( ( non
empty
right_complementable
Abelian
add-associative
right_zeroed
) ( non
empty
left_complementable
right_complementable
Abelian
add-associative
right_zeroed
V153
() )
RLSStruct
) : ( ( ) ( non
empty
)
set
) ) : ( ( ) ( )
set
) )
c=
B
: ( ( ) ( )
Subset
of )
(-)
(
X
: ( ( ) ( )
Subset
of )
/\
Y
: ( ( ) ( )
Subset
of )
)
: ( ( ) ( )
Element
of
K32
( the
carrier
of
b
1
: ( ( non
empty
right_complementable
Abelian
add-associative
right_zeroed
) ( non
empty
left_complementable
right_complementable
Abelian
add-associative
right_zeroed
V153
() )
RLSStruct
) : ( ( ) ( non
empty
)
set
) ) : ( ( ) ( )
set
) ) : ( ( ) ( )
Subset
of ) ;
theorem
:: MATHMORP:37
for
T
being ( ( non
empty
right_complementable
Abelian
add-associative
right_zeroed
) ( non
empty
left_complementable
right_complementable
Abelian
add-associative
right_zeroed
V153
() )
RLSStruct
)
for
X
,
B
being ( ( ) ( )
Subset
of ) holds
(
(
X
: ( ( ) ( )
Subset
of )
`
)
: ( ( ) ( )
Element
of
K32
( the
carrier
of
b
1
: ( ( non
empty
right_complementable
Abelian
add-associative
right_zeroed
) ( non
empty
left_complementable
right_complementable
Abelian
add-associative
right_zeroed
V153
() )
RLSStruct
) : ( ( ) ( non
empty
)
set
) ) : ( ( ) ( )
set
) )
(-)
B
: ( ( ) ( )
Subset
of )
)
: ( ( ) ( )
Subset
of )
`
: ( ( ) ( )
Element
of
K32
( the
carrier
of
b
1
: ( ( non
empty
right_complementable
Abelian
add-associative
right_zeroed
) ( non
empty
left_complementable
right_complementable
Abelian
add-associative
right_zeroed
V153
() )
RLSStruct
) : ( ( ) ( non
empty
)
set
) ) : ( ( ) ( )
set
) )
=
X
: ( ( ) ( )
Subset
of )
(+)
(
B
: ( ( ) ( )
Subset
of )
!
)
: ( ( ) ( )
Subset
of ) : ( ( ) ( )
Element
of
K32
( the
carrier
of
b
1
: ( ( non
empty
right_complementable
Abelian
add-associative
right_zeroed
) ( non
empty
left_complementable
right_complementable
Abelian
add-associative
right_zeroed
V153
() )
RLSStruct
) : ( ( ) ( non
empty
)
set
) ) : ( ( ) ( )
set
) ) ;
theorem
:: MATHMORP:38
for
T
being ( ( non
empty
right_complementable
Abelian
add-associative
right_zeroed
) ( non
empty
left_complementable
right_complementable
Abelian
add-associative
right_zeroed
V153
() )
RLSStruct
)
for
X
,
B
being ( ( ) ( )
Subset
of ) holds
(
X
: ( ( ) ( )
Subset
of )
(-)
B
: ( ( ) ( )
Subset
of )
)
: ( ( ) ( )
Subset
of )
`
: ( ( ) ( )
Element
of
K32
( the
carrier
of
b
1
: ( ( non
empty
right_complementable
Abelian
add-associative
right_zeroed
) ( non
empty
left_complementable
right_complementable
Abelian
add-associative
right_zeroed
V153
() )
RLSStruct
) : ( ( ) ( non
empty
)
set
) ) : ( ( ) ( )
set
) )
=
(
X
: ( ( ) ( )
Subset
of )
`
)
: ( ( ) ( )
Element
of
K32
( the
carrier
of
b
1
: ( ( non
empty
right_complementable
Abelian
add-associative
right_zeroed
) ( non
empty
left_complementable
right_complementable
Abelian
add-associative
right_zeroed
V153
() )
RLSStruct
) : ( ( ) ( non
empty
)
set
) ) : ( ( ) ( )
set
) )
(+)
(
B
: ( ( ) ( )
Subset
of )
!
)
: ( ( ) ( )
Subset
of ) : ( ( ) ( )
Element
of
K32
( the
carrier
of
b
1
: ( ( non
empty
right_complementable
Abelian
add-associative
right_zeroed
) ( non
empty
left_complementable
right_complementable
Abelian
add-associative
right_zeroed
V153
() )
RLSStruct
) : ( ( ) ( non
empty
)
set
) ) : ( ( ) ( )
set
) ) ;
begin
definition
let
T
be ( ( non
empty
) ( non
empty
)
addLoopStr
) ;
let
X
,
B
be ( ( ) ( )
Subset
of ) ;
func
X
(O)
B
->
( ( ) ( )
Subset
of )
equals
:: MATHMORP:def 4
(
X
: ( ( ) ( )
Element
of
T
: ( ( ) ( )
RLTopStruct
) )
(-)
B
: ( (
V12
()
V30
(
K33
(
T
: ( ( ) ( )
RLTopStruct
) ,
T
: ( ( ) ( )
RLTopStruct
) ) : ( ( ) ( )
set
) ,
T
: ( ( ) ( )
RLTopStruct
) ) ) (
V12
()
V30
(
K33
(
T
: ( ( ) ( )
RLTopStruct
) ,
T
: ( ( ) ( )
RLTopStruct
) ) : ( ( ) ( )
set
) ,
T
: ( ( ) ( )
RLTopStruct
) ) )
Element
of
K32
(
K33
(
K33
(
T
: ( ( ) ( )
RLTopStruct
) ,
T
: ( ( ) ( )
RLTopStruct
) ) : ( ( ) ( )
set
) ,
T
: ( ( ) ( )
RLTopStruct
) ) : ( ( ) ( )
set
) ) : ( ( ) ( )
set
) )
)
: ( ( ) ( )
Subset
of )
(+)
B
: ( (
V12
()
V30
(
K33
(
T
: ( ( ) ( )
RLTopStruct
) ,
T
: ( ( ) ( )
RLTopStruct
) ) : ( ( ) ( )
set
) ,
T
: ( ( ) ( )
RLTopStruct
) ) ) (
V12
()
V30
(
K33
(
T
: ( ( ) ( )
RLTopStruct
) ,
T
: ( ( ) ( )
RLTopStruct
) ) : ( ( ) ( )
set
) ,
T
: ( ( ) ( )
RLTopStruct
) ) )
Element
of
K32
(
K33
(
K33
(
T
: ( ( ) ( )
RLTopStruct
) ,
T
: ( ( ) ( )
RLTopStruct
) ) : ( ( ) ( )
set
) ,
T
: ( ( ) ( )
RLTopStruct
) ) : ( ( ) ( )
set
) ) : ( ( ) ( )
set
) ) : ( ( ) ( )
Element
of
K32
( the
carrier
of
T
: ( ( ) ( )
RLTopStruct
) : ( ( ) ( )
set
) ) : ( ( ) ( )
set
) ) ;
end;
definition
let
T
be ( ( non
empty
) ( non
empty
)
addLoopStr
) ;
let
X
,
B
be ( ( ) ( )
Subset
of ) ;
func
X
(o)
B
->
( ( ) ( )
Subset
of )
equals
:: MATHMORP:def 5
(
X
: ( ( ) ( )
Element
of
T
: ( ( ) ( )
RLTopStruct
) )
(+)
B
: ( (
V12
()
V30
(
K33
(
T
: ( ( ) ( )
RLTopStruct
) ,
T
: ( ( ) ( )
RLTopStruct
) ) : ( ( ) ( )
set
) ,
T
: ( ( ) ( )
RLTopStruct
) ) ) (
V12
()
V30
(
K33
(
T
: ( ( ) ( )
RLTopStruct
) ,
T
: ( ( ) ( )
RLTopStruct
) ) : ( ( ) ( )
set
) ,
T
: ( ( ) ( )
RLTopStruct
) ) )
Element
of
K32
(
K33
(
K33
(
T
: ( ( ) ( )
RLTopStruct
) ,
T
: ( ( ) ( )
RLTopStruct
) ) : ( ( ) ( )
set
) ,
T
: ( ( ) ( )
RLTopStruct
) ) : ( ( ) ( )
set
) ) : ( ( ) ( )
set
) )
)
: ( ( ) ( )
Element
of
K32
( the
carrier
of
T
: ( ( ) ( )
RLTopStruct
) : ( ( ) ( )
set
) ) : ( ( ) ( )
set
) )
(-)
B
: ( (
V12
()
V30
(
K33
(
T
: ( ( ) ( )
RLTopStruct
) ,
T
: ( ( ) ( )
RLTopStruct
) ) : ( ( ) ( )
set
) ,
T
: ( ( ) ( )
RLTopStruct
) ) ) (
V12
()
V30
(
K33
(
T
: ( ( ) ( )
RLTopStruct
) ,
T
: ( ( ) ( )
RLTopStruct
) ) : ( ( ) ( )
set
) ,
T
: ( ( ) ( )
RLTopStruct
) ) )
Element
of
K32
(
K33
(
K33
(
T
: ( ( ) ( )
RLTopStruct
) ,
T
: ( ( ) ( )
RLTopStruct
) ) : ( ( ) ( )
set
) ,
T
: ( ( ) ( )
RLTopStruct
) ) : ( ( ) ( )
set
) ) : ( ( ) ( )
set
) ) : ( ( ) ( )
Subset
of ) ;
end;
theorem
:: MATHMORP:39
for
T
being ( ( non
empty
right_complementable
Abelian
add-associative
right_zeroed
) ( non
empty
left_complementable
right_complementable
Abelian
add-associative
right_zeroed
V153
() )
RLSStruct
)
for
X
,
B
being ( ( ) ( )
Subset
of ) holds
(
(
X
: ( ( ) ( )
Subset
of )
`
)
: ( ( ) ( )
Element
of
K32
( the
carrier
of
b
1
: ( ( non
empty
right_complementable
Abelian
add-associative
right_zeroed
) ( non
empty
left_complementable
right_complementable
Abelian
add-associative
right_zeroed
V153
() )
RLSStruct
) : ( ( ) ( non
empty
)
set
) ) : ( ( ) ( )
set
) )
(O)
(
B
: ( ( ) ( )
Subset
of )
!
)
: ( ( ) ( )
Subset
of )
)
: ( ( ) ( )
Subset
of )
`
: ( ( ) ( )
Element
of
K32
( the
carrier
of
b
1
: ( ( non
empty
right_complementable
Abelian
add-associative
right_zeroed
) ( non
empty
left_complementable
right_complementable
Abelian
add-associative
right_zeroed
V153
() )
RLSStruct
) : ( ( ) ( non
empty
)
set
) ) : ( ( ) ( )
set
) )
=
X
: ( ( ) ( )
Subset
of )
(o)
B
: ( ( ) ( )
Subset
of ) : ( ( ) ( )
Subset
of ) ;
theorem
:: MATHMORP:40
for
T
being ( ( non
empty
right_complementable
Abelian
add-associative
right_zeroed
) ( non
empty
left_complementable
right_complementable
Abelian
add-associative
right_zeroed
V153
() )
RLSStruct
)
for
X
,
B
being ( ( ) ( )
Subset
of ) holds
(
(
X
: ( ( ) ( )
Subset
of )
`
)
: ( ( ) ( )
Element
of
K32
( the
carrier
of
b
1
: ( ( non
empty
right_complementable
Abelian
add-associative
right_zeroed
) ( non
empty
left_complementable
right_complementable
Abelian
add-associative
right_zeroed
V153
() )
RLSStruct
) : ( ( ) ( non
empty
)
set
) ) : ( ( ) ( )
set
) )
(o)
(
B
: ( ( ) ( )
Subset
of )
!
)
: ( ( ) ( )
Subset
of )
)
: ( ( ) ( )
Subset
of )
`
: ( ( ) ( )
Element
of
K32
( the
carrier
of
b
1
: ( ( non
empty
right_complementable
Abelian
add-associative
right_zeroed
) ( non
empty
left_complementable
right_complementable
Abelian
add-associative
right_zeroed
V153
() )
RLSStruct
) : ( ( ) ( non
empty
)
set
) ) : ( ( ) ( )
set
) )
=
X
: ( ( ) ( )
Subset
of )
(O)
B
: ( ( ) ( )
Subset
of ) : ( ( ) ( )
Subset
of ) ;
theorem
:: MATHMORP:41
for
T
being ( ( non
empty
right_complementable
Abelian
add-associative
right_zeroed
) ( non
empty
left_complementable
right_complementable
Abelian
add-associative
right_zeroed
V153
() )
RLSStruct
)
for
X
,
B
being ( ( ) ( )
Subset
of ) holds
(
X
: ( ( ) ( )
Subset
of )
(O)
B
: ( ( ) ( )
Subset
of ) : ( ( ) ( )
Subset
of )
c=
X
: ( ( ) ( )
Subset
of ) &
X
: ( ( ) ( )
Subset
of )
c=
X
: ( ( ) ( )
Subset
of )
(o)
B
: ( ( ) ( )
Subset
of ) : ( ( ) ( )
Subset
of ) ) ;
theorem
:: MATHMORP:42
for
T
being ( ( non
empty
right_complementable
Abelian
add-associative
right_zeroed
) ( non
empty
left_complementable
right_complementable
Abelian
add-associative
right_zeroed
V153
() )
RLSStruct
)
for
X
being ( ( ) ( )
Subset
of ) holds
X
: ( ( ) ( )
Subset
of )
(O)
X
: ( ( ) ( )
Subset
of ) : ( ( ) ( )
Subset
of )
=
X
: ( ( ) ( )
Subset
of ) ;
theorem
:: MATHMORP:43
for
T
being ( ( non
empty
right_complementable
Abelian
add-associative
right_zeroed
) ( non
empty
left_complementable
right_complementable
Abelian
add-associative
right_zeroed
V153
() )
RLSStruct
)
for
X
,
B
being ( ( ) ( )
Subset
of ) holds
(
(
X
: ( ( ) ( )
Subset
of )
(O)
B
: ( ( ) ( )
Subset
of )
)
: ( ( ) ( )
Subset
of )
(-)
B
: ( ( ) ( )
Subset
of ) : ( ( ) ( )
Subset
of )
c=
X
: ( ( ) ( )
Subset
of )
(-)
B
: ( ( ) ( )
Subset
of ) : ( ( ) ( )
Subset
of ) &
(
X
: ( ( ) ( )
Subset
of )
(O)
B
: ( ( ) ( )
Subset
of )
)
: ( ( ) ( )
Subset
of )
(+)
B
: ( ( ) ( )
Subset
of ) : ( ( ) ( )
Element
of
K32
( the
carrier
of
b
1
: ( ( non
empty
right_complementable
Abelian
add-associative
right_zeroed
) ( non
empty
left_complementable
right_complementable
Abelian
add-associative
right_zeroed
V153
() )
RLSStruct
) : ( ( ) ( non
empty
)
set
) ) : ( ( ) ( )
set
) )
c=
X
: ( ( ) ( )
Subset
of )
(+)
B
: ( ( ) ( )
Subset
of ) : ( ( ) ( )
Element
of
K32
( the
carrier
of
b
1
: ( ( non
empty
right_complementable
Abelian
add-associative
right_zeroed
) ( non
empty
left_complementable
right_complementable
Abelian
add-associative
right_zeroed
V153
() )
RLSStruct
) : ( ( ) ( non
empty
)
set
) ) : ( ( ) ( )
set
) ) ) ;
theorem
:: MATHMORP:44
for
T
being ( ( non
empty
right_complementable
Abelian
add-associative
right_zeroed
) ( non
empty
left_complementable
right_complementable
Abelian
add-associative
right_zeroed
V153
() )
RLSStruct
)
for
X
,
B
being ( ( ) ( )
Subset
of ) holds
(
X
: ( ( ) ( )
Subset
of )
(-)
B
: ( ( ) ( )
Subset
of ) : ( ( ) ( )
Subset
of )
c=
(
X
: ( ( ) ( )
Subset
of )
(o)
B
: ( ( ) ( )
Subset
of )
)
: ( ( ) ( )
Subset
of )
(-)
B
: ( ( ) ( )
Subset
of ) : ( ( ) ( )
Subset
of ) &
X
: ( ( ) ( )
Subset
of )
(+)
B
: ( ( ) ( )
Subset
of ) : ( ( ) ( )
Element
of
K32
( the
carrier
of
b
1
: ( ( non
empty
right_complementable
Abelian
add-associative
right_zeroed
) ( non
empty
left_complementable
right_complementable
Abelian
add-associative
right_zeroed
V153
() )
RLSStruct
) : ( ( ) ( non
empty
)
set
) ) : ( ( ) ( )
set
) )
c=
(
X
: ( ( ) ( )
Subset
of )
(o)
B
: ( ( ) ( )
Subset
of )
)
: ( ( ) ( )
Subset
of )
(+)
B
: ( ( ) ( )
Subset
of ) : ( ( ) ( )
Element
of
K32
( the
carrier
of
b
1
: ( ( non
empty
right_complementable
Abelian
add-associative
right_zeroed
) ( non
empty
left_complementable
right_complementable
Abelian
add-associative
right_zeroed
V153
() )
RLSStruct
) : ( ( ) ( non
empty
)
set
) ) : ( ( ) ( )
set
) ) ) ;
theorem
:: MATHMORP:45
for
T
being ( ( non
empty
right_complementable
Abelian
add-associative
right_zeroed
) ( non
empty
left_complementable
right_complementable
Abelian
add-associative
right_zeroed
V153
() )
RLSStruct
)
for
X
,
Y
,
B
being ( ( ) ( )
Subset
of ) st
X
: ( ( ) ( )
Subset
of )
c=
Y
: ( ( ) ( )
Subset
of ) holds
(
X
: ( ( ) ( )
Subset
of )
(O)
B
: ( ( ) ( )
Subset
of ) : ( ( ) ( )
Subset
of )
c=
Y
: ( ( ) ( )
Subset
of )
(O)
B
: ( ( ) ( )
Subset
of ) : ( ( ) ( )
Subset
of ) &
X
: ( ( ) ( )
Subset
of )
(o)
B
: ( ( ) ( )
Subset
of ) : ( ( ) ( )
Subset
of )
c=
Y
: ( ( ) ( )
Subset
of )
(o)
B
: ( ( ) ( )
Subset
of ) : ( ( ) ( )
Subset
of ) ) ;
theorem
:: MATHMORP:46
for
T
being ( ( non
empty
right_complementable
Abelian
add-associative
right_zeroed
) ( non
empty
left_complementable
right_complementable
Abelian
add-associative
right_zeroed
V153
() )
RLSStruct
)
for
X
,
Y
being ( ( ) ( )
Subset
of )
for
p
being ( ( ) ( )
Point
of ( ( ) ( non
empty
)
set
) ) holds
(
X
: ( ( ) ( )
Subset
of )
+
p
: ( ( ) ( )
Point
of ( ( ) ( non
empty
)
set
) )
)
: ( ( ) ( )
Subset
of )
(O)
Y
: ( ( ) ( )
Subset
of ) : ( ( ) ( )
Subset
of )
=
(
X
: ( ( ) ( )
Subset
of )
(O)
Y
: ( ( ) ( )
Subset
of )
)
: ( ( ) ( )
Subset
of )
+
p
: ( ( ) ( )
Point
of ( ( ) ( non
empty
)
set
) ) : ( ( ) ( )
Subset
of ) ;
theorem
:: MATHMORP:47
for
T
being ( ( non
empty
right_complementable
Abelian
add-associative
right_zeroed
) ( non
empty
left_complementable
right_complementable
Abelian
add-associative
right_zeroed
V153
() )
RLSStruct
)
for
X
,
Y
being ( ( ) ( )
Subset
of )
for
p
being ( ( ) ( )
Point
of ( ( ) ( non
empty
)
set
) ) holds
(
X
: ( ( ) ( )
Subset
of )
+
p
: ( ( ) ( )
Point
of ( ( ) ( non
empty
)
set
) )
)
: ( ( ) ( )
Subset
of )
(o)
Y
: ( ( ) ( )
Subset
of ) : ( ( ) ( )
Subset
of )
=
(
X
: ( ( ) ( )
Subset
of )
(o)
Y
: ( ( ) ( )
Subset
of )
)
: ( ( ) ( )
Subset
of )
+
p
: ( ( ) ( )
Point
of ( ( ) ( non
empty
)
set
) ) : ( ( ) ( )
Subset
of ) ;
theorem
:: MATHMORP:48
for
T
being ( ( non
empty
right_complementable
Abelian
add-associative
right_zeroed
) ( non
empty
left_complementable
right_complementable
Abelian
add-associative
right_zeroed
V153
() )
RLSStruct
)
for
C
,
B
,
X
being ( ( ) ( )
Subset
of ) st
C
: ( ( ) ( )
Subset
of )
c=
B
: ( ( ) ( )
Subset
of ) holds
X
: ( ( ) ( )
Subset
of )
(O)
B
: ( ( ) ( )
Subset
of ) : ( ( ) ( )
Subset
of )
c=
(
X
: ( ( ) ( )
Subset
of )
(-)
C
: ( ( ) ( )
Subset
of )
)
: ( ( ) ( )
Subset
of )
(+)
B
: ( ( ) ( )
Subset
of ) : ( ( ) ( )
Element
of
K32
( the
carrier
of
b
1
: ( ( non
empty
right_complementable
Abelian
add-associative
right_zeroed
) ( non
empty
left_complementable
right_complementable
Abelian
add-associative
right_zeroed
V153
() )
RLSStruct
) : ( ( ) ( non
empty
)
set
) ) : ( ( ) ( )
set
) ) ;
theorem
:: MATHMORP:49
for
T
being ( ( non
empty
right_complementable
Abelian
add-associative
right_zeroed
) ( non
empty
left_complementable
right_complementable
Abelian
add-associative
right_zeroed
V153
() )
RLSStruct
)
for
B
,
C
,
X
being ( ( ) ( )
Subset
of ) st
B
: ( ( ) ( )
Subset
of )
c=
C
: ( ( ) ( )
Subset
of ) holds
X
: ( ( ) ( )
Subset
of )
(o)
B
: ( ( ) ( )
Subset
of ) : ( ( ) ( )
Subset
of )
c=
(
X
: ( ( ) ( )
Subset
of )
(+)
C
: ( ( ) ( )
Subset
of )
)
: ( ( ) ( )
Element
of
K32
( the
carrier
of
b
1
: ( ( non
empty
right_complementable
Abelian
add-associative
right_zeroed
) ( non
empty
left_complementable
right_complementable
Abelian
add-associative
right_zeroed
V153
() )
RLSStruct
) : ( ( ) ( non
empty
)
set
) ) : ( ( ) ( )
set
) )
(-)
B
: ( ( ) ( )
Subset
of ) : ( ( ) ( )
Subset
of ) ;
theorem
:: MATHMORP:50
for
T
being ( ( non
empty
right_complementable
Abelian
add-associative
right_zeroed
) ( non
empty
left_complementable
right_complementable
Abelian
add-associative
right_zeroed
V153
() )
RLSStruct
)
for
X
,
Y
being ( ( ) ( )
Subset
of ) holds
(
X
: ( ( ) ( )
Subset
of )
(+)
Y
: ( ( ) ( )
Subset
of ) : ( ( ) ( )
Element
of
K32
( the
carrier
of
b
1
: ( ( non
empty
right_complementable
Abelian
add-associative
right_zeroed
) ( non
empty
left_complementable
right_complementable
Abelian
add-associative
right_zeroed
V153
() )
RLSStruct
) : ( ( ) ( non
empty
)
set
) ) : ( ( ) ( )
set
) )
=
(
X
: ( ( ) ( )
Subset
of )
(o)
Y
: ( ( ) ( )
Subset
of )
)
: ( ( ) ( )
Subset
of )
(+)
Y
: ( ( ) ( )
Subset
of ) : ( ( ) ( )
Element
of
K32
( the
carrier
of
b
1
: ( ( non
empty
right_complementable
Abelian
add-associative
right_zeroed
) ( non
empty
left_complementable
right_complementable
Abelian
add-associative
right_zeroed
V153
() )
RLSStruct
) : ( ( ) ( non
empty
)
set
) ) : ( ( ) ( )
set
) ) &
X
: ( ( ) ( )
Subset
of )
(-)
Y
: ( ( ) ( )
Subset
of ) : ( ( ) ( )
Subset
of )
=
(
X
: ( ( ) ( )
Subset
of )
(O)
Y
: ( ( ) ( )
Subset
of )
)
: ( ( ) ( )
Subset
of )
(-)
Y
: ( ( ) ( )
Subset
of ) : ( ( ) ( )
Subset
of ) ) ;
theorem
:: MATHMORP:51
for
T
being ( ( non
empty
right_complementable
Abelian
add-associative
right_zeroed
) ( non
empty
left_complementable
right_complementable
Abelian
add-associative
right_zeroed
V153
() )
RLSStruct
)
for
X
,
Y
being ( ( ) ( )
Subset
of ) holds
(
X
: ( ( ) ( )
Subset
of )
(+)
Y
: ( ( ) ( )
Subset
of ) : ( ( ) ( )
Element
of
K32
( the
carrier
of
b
1
: ( ( non
empty
right_complementable
Abelian
add-associative
right_zeroed
) ( non
empty
left_complementable
right_complementable
Abelian
add-associative
right_zeroed
V153
() )
RLSStruct
) : ( ( ) ( non
empty
)
set
) ) : ( ( ) ( )
set
) )
=
(
X
: ( ( ) ( )
Subset
of )
(+)
Y
: ( ( ) ( )
Subset
of )
)
: ( ( ) ( )
Element
of
K32
( the
carrier
of
b
1
: ( ( non
empty
right_complementable
Abelian
add-associative
right_zeroed
) ( non
empty
left_complementable
right_complementable
Abelian
add-associative
right_zeroed
V153
() )
RLSStruct
) : ( ( ) ( non
empty
)
set
) ) : ( ( ) ( )
set
) )
(O)
Y
: ( ( ) ( )
Subset
of ) : ( ( ) ( )
Subset
of ) &
X
: ( ( ) ( )
Subset
of )
(-)
Y
: ( ( ) ( )
Subset
of ) : ( ( ) ( )
Subset
of )
=
(
X
: ( ( ) ( )
Subset
of )
(-)
Y
: ( ( ) ( )
Subset
of )
)
: ( ( ) ( )
Subset
of )
(o)
Y
: ( ( ) ( )
Subset
of ) : ( ( ) ( )
Subset
of ) ) ;
theorem
:: MATHMORP:52
for
T
being ( ( non
empty
right_complementable
Abelian
add-associative
right_zeroed
) ( non
empty
left_complementable
right_complementable
Abelian
add-associative
right_zeroed
V153
() )
RLSStruct
)
for
X
,
B
being ( ( ) ( )
Subset
of ) holds
(
X
: ( ( ) ( )
Subset
of )
(O)
B
: ( ( ) ( )
Subset
of )
)
: ( ( ) ( )
Subset
of )
(O)
B
: ( ( ) ( )
Subset
of ) : ( ( ) ( )
Subset
of )
=
X
: ( ( ) ( )
Subset
of )
(O)
B
: ( ( ) ( )
Subset
of ) : ( ( ) ( )
Subset
of ) ;
theorem
:: MATHMORP:53
for
T
being ( ( non
empty
right_complementable
Abelian
add-associative
right_zeroed
) ( non
empty
left_complementable
right_complementable
Abelian
add-associative
right_zeroed
V153
() )
RLSStruct
)
for
X
,
B
being ( ( ) ( )
Subset
of ) holds
(
X
: ( ( ) ( )
Subset
of )
(o)
B
: ( ( ) ( )
Subset
of )
)
: ( ( ) ( )
Subset
of )
(o)
B
: ( ( ) ( )
Subset
of ) : ( ( ) ( )
Subset
of )
=
X
: ( ( ) ( )
Subset
of )
(o)
B
: ( ( ) ( )
Subset
of ) : ( ( ) ( )
Subset
of ) ;
theorem
:: MATHMORP:54
for
T
being ( ( non
empty
right_complementable
Abelian
add-associative
right_zeroed
) ( non
empty
left_complementable
right_complementable
Abelian
add-associative
right_zeroed
V153
() )
RLSStruct
)
for
X
,
B
,
Y
being ( ( ) ( )
Subset
of ) holds
X
: ( ( ) ( )
Subset
of )
(O)
B
: ( ( ) ( )
Subset
of ) : ( ( ) ( )
Subset
of )
c=
(
X
: ( ( ) ( )
Subset
of )
\/
Y
: ( ( ) ( )
Subset
of )
)
: ( ( ) ( )
Element
of
K32
( the
carrier
of
b
1
: ( ( non
empty
right_complementable
Abelian
add-associative
right_zeroed
) ( non
empty
left_complementable
right_complementable
Abelian
add-associative
right_zeroed
V153
() )
RLSStruct
) : ( ( ) ( non
empty
)
set
) ) : ( ( ) ( )
set
) )
(O)
B
: ( ( ) ( )
Subset
of ) : ( ( ) ( )
Subset
of ) ;
theorem
:: MATHMORP:55
for
T
being ( ( non
empty
right_complementable
Abelian
add-associative
right_zeroed
) ( non
empty
left_complementable
right_complementable
Abelian
add-associative
right_zeroed
V153
() )
RLSStruct
)
for
B
,
B1
,
X
being ( ( ) ( )
Subset
of ) st
B
: ( ( ) ( )
Subset
of )
=
B
: ( ( ) ( )
Subset
of )
(O)
B1
: ( ( ) ( )
Subset
of ) : ( ( ) ( )
Subset
of ) holds
X
: ( ( ) ( )
Subset
of )
(O)
B
: ( ( ) ( )
Subset
of ) : ( ( ) ( )
Subset
of )
c=
X
: ( ( ) ( )
Subset
of )
(O)
B1
: ( ( ) ( )
Subset
of ) : ( ( ) ( )
Subset
of ) ;
begin
definition
let
t
be ( (
real
) (
V24
()
real
ext-real
)
number
) ;
let
T
be ( ( non
empty
) ( non
empty
)
RLSStruct
) ;
let
A
be ( ( ) ( )
Subset
of ) ;
func
t
(.)
A
->
( ( ) ( )
Subset
of )
equals
:: MATHMORP:def 6
{
(
t
: ( ( ) ( )
RLTopStruct
)
*
a
: ( ( ) ( )
Point
of ( ( ) ( non
empty
)
set
) )
)
: ( ( ) ( )
Element
of the
carrier
of
T
: ( ( ) ( )
Element
of
t
: ( ( ) ( )
RLTopStruct
) ) : ( ( ) ( )
set
) ) where
a
is ( ( ) ( )
Point
of ( ( ) ( )
set
) ) :
a
: ( ( ) ( )
Point
of ( ( ) ( non
empty
)
set
) )
in
A
: ( (
V12
()
V30
(
K33
(
t
: ( ( ) ( )
RLTopStruct
) ,
t
: ( ( ) ( )
RLTopStruct
) ) : ( ( ) ( )
set
) ,
t
: ( ( ) ( )
RLTopStruct
) ) ) (
V12
()
V30
(
K33
(
t
: ( ( ) ( )
RLTopStruct
) ,
t
: ( ( ) ( )
RLTopStruct
) ) : ( ( ) ( )
set
) ,
t
: ( ( ) ( )
RLTopStruct
) ) )
Element
of
K32
(
K33
(
K33
(
t
: ( ( ) ( )
RLTopStruct
) ,
t
: ( ( ) ( )
RLTopStruct
) ) : ( ( ) ( )
set
) ,
t
: ( ( ) ( )
RLTopStruct
) ) : ( ( ) ( )
set
) ) : ( ( ) ( )
set
) )
}
;
end;
theorem
:: MATHMORP:56
for
T
being ( ( non
empty
right_complementable
Abelian
add-associative
right_zeroed
) ( non
empty
left_complementable
right_complementable
Abelian
add-associative
right_zeroed
V153
() )
RLSStruct
)
for
X
being ( ( ) ( )
Subset
of ) st
X
: ( ( ) ( )
Subset
of )
=
{}
: ( ( ) (
empty
V134
()
V135
()
V136
()
V137
()
V138
()
V139
()
V140
() )
set
) holds
0
: ( ( ) (
empty
natural
V24
()
real
ext-real
non
positive
non
negative
V86
()
V87
()
V134
()
V135
()
V136
()
V137
()
V138
()
V139
()
V140
() )
Element
of
NAT
: ( ( ) (
V134
()
V135
()
V136
()
V137
()
V138
()
V139
()
V140
() )
Element
of
K32
(
REAL
: ( ( ) (
V134
()
V135
()
V136
()
V140
() )
set
) ) : ( ( ) ( )
set
) ) )
(.)
X
: ( ( ) ( )
Subset
of ) : ( ( ) ( )
Subset
of )
=
{}
: ( ( ) (
empty
V134
()
V135
()
V136
()
V137
()
V138
()
V139
()
V140
() )
set
) ;
theorem
:: MATHMORP:57
for
n
being ( ( ) (
natural
V24
()
real
ext-real
V86
()
V87
()
V134
()
V135
()
V136
()
V137
()
V138
()
V139
() )
Element
of
NAT
: ( ( ) (
V134
()
V135
()
V136
()
V137
()
V138
()
V139
()
V140
() )
Element
of
K32
(
REAL
: ( ( ) (
V134
()
V135
()
V136
()
V140
() )
set
) ) : ( ( ) ( )
set
) ) )
for
X
being ( ( non
empty
) ( non
empty
)
Subset
of ) holds
0
: ( ( ) (
empty
natural
V24
()
real
ext-real
non
positive
non
negative
V86
()
V87
()
V134
()
V135
()
V136
()
V137
()
V138
()
V139
()
V140
() )
Element
of
NAT
: ( ( ) (
V134
()
V135
()
V136
()
V137
()
V138
()
V139
()
V140
() )
Element
of
K32
(
REAL
: ( ( ) (
V134
()
V135
()
V136
()
V140
() )
set
) ) : ( ( ) ( )
set
) ) )
(.)
X
: ( ( non
empty
) ( non
empty
)
Subset
of ) : ( ( ) ( )
Subset
of )
=
{
(
0.
(
TOP-REAL
n
: ( ( ) (
natural
V24
()
real
ext-real
V86
()
V87
()
V134
()
V135
()
V136
()
V137
()
V138
()
V139
() )
Element
of
NAT
: ( ( ) (
V134
()
V135
()
V136
()
V137
()
V138
()
V139
()
V140
() )
Element
of
K32
(
REAL
: ( ( ) (
V134
()
V135
()
V136
()
V140
() )
set
) ) : ( ( ) ( )
set
) ) )
)
: ( (
strict
) ( non
empty
TopSpace-like
left_complementable
right_complementable
Abelian
add-associative
right_zeroed
vector-distributive
scalar-distributive
scalar-associative
scalar-unital
V153
()
strict
)
RLTopStruct
)
)
: ( ( ) (
V40
(
b
1
: ( ( ) (
natural
V24
()
real
ext-real
V86
()
V87
()
V134
()
V135
()
V136
()
V137
()
V138
()
V139
() )
Element
of
NAT
: ( ( ) (
V134
()
V135
()
V136
()
V137
()
V138
()
V139
()
V140
() )
Element
of
K32
(
REAL
: ( ( ) (
V134
()
V135
()
V136
()
V140
() )
set
) ) : ( ( ) ( )
set
) ) ) )
V49
(
TOP-REAL
b
1
: ( ( ) (
natural
V24
()
real
ext-real
V86
()
V87
()
V134
()
V135
()
V136
()
V137
()
V138
()
V139
() )
Element
of
NAT
: ( ( ) (
V134
()
V135
()
V136
()
V137
()
V138
()
V139
()
V140
() )
Element
of
K32
(
REAL
: ( ( ) (
V134
()
V135
()
V136
()
V140
() )
set
) ) : ( ( ) ( )
set
) ) ) : ( (
strict
) ( non
empty
TopSpace-like
left_complementable
right_complementable
Abelian
add-associative
right_zeroed
vector-distributive
scalar-distributive
scalar-associative
scalar-unital
V153
()
strict
)
RLTopStruct
) )
V83
()
V126
() )
Element
of the
carrier
of
(
TOP-REAL
b
1
: ( ( ) (
natural
V24
()
real
ext-real
V86
()
V87
()
V134
()
V135
()
V136
()
V137
()
V138
()
V139
() )
Element
of
NAT
: ( ( ) (
V134
()
V135
()
V136
()
V137
()
V138
()
V139
()
V140
() )
Element
of
K32
(
REAL
: ( ( ) (
V134
()
V135
()
V136
()
V140
() )
set
) ) : ( ( ) ( )
set
) ) )
)
: ( (
strict
) ( non
empty
TopSpace-like
left_complementable
right_complementable
Abelian
add-associative
right_zeroed
vector-distributive
scalar-distributive
scalar-associative
scalar-unital
V153
()
strict
)
RLTopStruct
) : ( ( ) ( non
empty
)
set
) )
}
: ( ( ) ( non
empty
)
Element
of
K32
( the
carrier
of
(
TOP-REAL
b
1
: ( ( ) (
natural
V24
()
real
ext-real
V86
()
V87
()
V134
()
V135
()
V136
()
V137
()
V138
()
V139
() )
Element
of
NAT
: ( ( ) (
V134
()
V135
()
V136
()
V137
()
V138
()
V139
()
V140
() )
Element
of
K32
(
REAL
: ( ( ) (
V134
()
V135
()
V136
()
V140
() )
set
) ) : ( ( ) ( )
set
) ) )
)
: ( (
strict
) ( non
empty
TopSpace-like
left_complementable
right_complementable
Abelian
add-associative
right_zeroed
vector-distributive
scalar-distributive
scalar-associative
scalar-unital
V153
()
strict
)
RLTopStruct
) : ( ( ) ( non
empty
)
set
) ) : ( ( ) ( )
set
) ) ;
theorem
:: MATHMORP:58
for
n
being ( ( ) (
natural
V24
()
real
ext-real
V86
()
V87
()
V134
()
V135
()
V136
()
V137
()
V138
()
V139
() )
Element
of
NAT
: ( ( ) (
V134
()
V135
()
V136
()
V137
()
V138
()
V139
()
V140
() )
Element
of
K32
(
REAL
: ( ( ) (
V134
()
V135
()
V136
()
V140
() )
set
) ) : ( ( ) ( )
set
) ) )
for
X
being ( ( ) ( )
Subset
of ) holds 1 : ( ( ) ( non
empty
natural
V24
()
real
ext-real
positive
non
negative
V86
()
V87
()
V134
()
V135
()
V136
()
V137
()
V138
()
V139
() )
Element
of
NAT
: ( ( ) (
V134
()
V135
()
V136
()
V137
()
V138
()
V139
()
V140
() )
Element
of
K32
(
REAL
: ( ( ) (
V134
()
V135
()
V136
()
V140
() )
set
) ) : ( ( ) ( )
set
) ) )
(.)
X
: ( ( ) ( )
Subset
of ) : ( ( ) ( )
Subset
of )
=
X
: ( ( ) ( )
Subset
of ) ;
theorem
:: MATHMORP:59
for
n
being ( ( ) (
natural
V24
()
real
ext-real
V86
()
V87
()
V134
()
V135
()
V136
()
V137
()
V138
()
V139
() )
Element
of
NAT
: ( ( ) (
V134
()
V135
()
V136
()
V137
()
V138
()
V139
()
V140
() )
Element
of
K32
(
REAL
: ( ( ) (
V134
()
V135
()
V136
()
V140
() )
set
) ) : ( ( ) ( )
set
) ) )
for
X
being ( ( ) ( )
Subset
of ) holds 2 : ( ( ) ( non
empty
natural
V24
()
real
ext-real
positive
non
negative
V86
()
V87
()
V134
()
V135
()
V136
()
V137
()
V138
()
V139
() )
Element
of
NAT
: ( ( ) (
V134
()
V135
()
V136
()
V137
()
V138
()
V139
()
V140
() )
Element
of
K32
(
REAL
: ( ( ) (
V134
()
V135
()
V136
()
V140
() )
set
) ) : ( ( ) ( )
set
) ) )
(.)
X
: ( ( ) ( )
Subset
of ) : ( ( ) ( )
Subset
of )
c=
X
: ( ( ) ( )
Subset
of )
(+)
X
: ( ( ) ( )
Subset
of ) : ( ( ) ( )
Element
of
K32
( the
carrier
of
(
TOP-REAL
b
1
: ( ( ) (
natural
V24
()
real
ext-real
V86
()
V87
()
V134
()
V135
()
V136
()
V137
()
V138
()
V139
() )
Element
of
NAT
: ( ( ) (
V134
()
V135
()
V136
()
V137
()
V138
()
V139
()
V140
() )
Element
of
K32
(
REAL
: ( ( ) (
V134
()
V135
()
V136
()
V140
() )
set
) ) : ( ( ) ( )
set
) ) )
)
: ( (
strict
) ( non
empty
TopSpace-like
left_complementable
right_complementable
Abelian
add-associative
right_zeroed
vector-distributive
scalar-distributive
scalar-associative
scalar-unital
V153
()
strict
)
RLTopStruct
) : ( ( ) ( non
empty
)
set
) ) : ( ( ) ( )
set
) ) ;
theorem
:: MATHMORP:60
for
t
,
s
being ( (
real
) (
V24
()
real
ext-real
)
number
)
for
n
being ( ( ) (
natural
V24
()
real
ext-real
V86
()
V87
()
V134
()
V135
()
V136
()
V137
()
V138
()
V139
() )
Element
of
NAT
: ( ( ) (
V134
()
V135
()
V136
()
V137
()
V138
()
V139
()
V140
() )
Element
of
K32
(
REAL
: ( ( ) (
V134
()
V135
()
V136
()
V140
() )
set
) ) : ( ( ) ( )
set
) ) )
for
X
being ( ( ) ( )
Subset
of ) holds
(
t
: ( (
real
) (
V24
()
real
ext-real
)
number
)
*
s
: ( (
real
) (
V24
()
real
ext-real
)
number
)
)
: ( ( ) (
V24
()
real
ext-real
)
set
)
(.)
X
: ( ( ) ( )
Subset
of ) : ( ( ) ( )
Subset
of )
=
t
: ( (
real
) (
V24
()
real
ext-real
)
number
)
(.)
(
s
: ( (
real
) (
V24
()
real
ext-real
)
number
)
(.)
X
: ( ( ) ( )
Subset
of )
)
: ( ( ) ( )
Subset
of ) : ( ( ) ( )
Subset
of ) ;
theorem
:: MATHMORP:61
for
t
being ( (
real
) (
V24
()
real
ext-real
)
number
)
for
n
being ( ( ) (
natural
V24
()
real
ext-real
V86
()
V87
()
V134
()
V135
()
V136
()
V137
()
V138
()
V139
() )
Element
of
NAT
: ( ( ) (
V134
()
V135
()
V136
()
V137
()
V138
()
V139
()
V140
() )
Element
of
K32
(
REAL
: ( ( ) (
V134
()
V135
()
V136
()
V140
() )
set
) ) : ( ( ) ( )
set
) ) )
for
X
,
Y
being ( ( ) ( )
Subset
of ) st
X
: ( ( ) ( )
Subset
of )
c=
Y
: ( ( ) ( )
Subset
of ) holds
t
: ( (
real
) (
V24
()
real
ext-real
)
number
)
(.)
X
: ( ( ) ( )
Subset
of ) : ( ( ) ( )
Subset
of )
c=
t
: ( (
real
) (
V24
()
real
ext-real
)
number
)
(.)
Y
: ( ( ) ( )
Subset
of ) : ( ( ) ( )
Subset
of ) ;
theorem
:: MATHMORP:62
for
t
being ( (
real
) (
V24
()
real
ext-real
)
number
)
for
n
being ( ( ) (
natural
V24
()
real
ext-real
V86
()
V87
()
V134
()
V135
()
V136
()
V137
()
V138
()
V139
() )
Element
of
NAT
: ( ( ) (
V134
()
V135
()
V136
()
V137
()
V138
()
V139
()
V140
() )
Element
of
K32
(
REAL
: ( ( ) (
V134
()
V135
()
V136
()
V140
() )
set
) ) : ( ( ) ( )
set
) ) )
for
X
being ( ( ) ( )
Subset
of )
for
x
being ( ( ) (
V40
(
b
2
: ( ( ) (
natural
V24
()
real
ext-real
V86
()
V87
()
V134
()
V135
()
V136
()
V137
()
V138
()
V139
() )
Element
of
NAT
: ( ( ) (
V134
()
V135
()
V136
()
V137
()
V138
()
V139
()
V140
() )
Element
of
K32
(
REAL
: ( ( ) (
V134
()
V135
()
V136
()
V140
() )
set
) ) : ( ( ) ( )
set
) ) ) )
V83
()
V126
() )
Point
of ( ( ) ( non
empty
)
set
) ) holds
t
: ( (
real
) (
V24
()
real
ext-real
)
number
)
(.)
(
X
: ( ( ) ( )
Subset
of )
+
x
: ( ( ) (
V40
(
b
2
: ( ( ) (
natural
V24
()
real
ext-real
V86
()
V87
()
V134
()
V135
()
V136
()
V137
()
V138
()
V139
() )
Element
of
NAT
: ( ( ) (
V134
()
V135
()
V136
()
V137
()
V138
()
V139
()
V140
() )
Element
of
K32
(
REAL
: ( ( ) (
V134
()
V135
()
V136
()
V140
() )
set
) ) : ( ( ) ( )
set
) ) ) )
V83
()
V126
() )
Point
of ( ( ) ( non
empty
)
set
) )
)
: ( ( ) ( )
Subset
of ) : ( ( ) ( )
Subset
of )
=
(
t
: ( (
real
) (
V24
()
real
ext-real
)
number
)
(.)
X
: ( ( ) ( )
Subset
of )
)
: ( ( ) ( )
Subset
of )
+
(
t
: ( (
real
) (
V24
()
real
ext-real
)
number
)
*
x
: ( ( ) (
V40
(
b
2
: ( ( ) (
natural
V24
()
real
ext-real
V86
()
V87
()
V134
()
V135
()
V136
()
V137
()
V138
()
V139
() )
Element
of
NAT
: ( ( ) (
V134
()
V135
()
V136
()
V137
()
V138
()
V139
()
V140
() )
Element
of
K32
(
REAL
: ( ( ) (
V134
()
V135
()
V136
()
V140
() )
set
) ) : ( ( ) ( )
set
) ) ) )
V83
()
V126
() )
Point
of ( ( ) ( non
empty
)
set
) )
)
: ( ( ) (
V40
(
b
2
: ( ( ) (
natural
V24
()
real
ext-real
V86
()
V87
()
V134
()
V135
()
V136
()
V137
()
V138
()
V139
() )
Element
of
NAT
: ( ( ) (
V134
()
V135
()
V136
()
V137
()
V138
()
V139
()
V140
() )
Element
of
K32
(
REAL
: ( ( ) (
V134
()
V135
()
V136
()
V140
() )
set
) ) : ( ( ) ( )
set
) ) ) )
V83
()
V126
() )
Element
of the
carrier
of
(
TOP-REAL
b
2
: ( ( ) (
natural
V24
()
real
ext-real
V86
()
V87
()
V134
()
V135
()
V136
()
V137
()
V138
()
V139
() )
Element
of
NAT
: ( ( ) (
V134
()
V135
()
V136
()
V137
()
V138
()
V139
()
V140
() )
Element
of
K32
(
REAL
: ( ( ) (
V134
()
V135
()
V136
()
V140
() )
set
) ) : ( ( ) ( )
set
) ) )
)
: ( (
strict
) ( non
empty
TopSpace-like
left_complementable
right_complementable
Abelian
add-associative
right_zeroed
vector-distributive
scalar-distributive
scalar-associative
scalar-unital
V153
()
strict
)
RLTopStruct
) : ( ( ) ( non
empty
)
set
) ) : ( ( ) ( )
Subset
of ) ;
theorem
:: MATHMORP:63
for
t
being ( (
real
) (
V24
()
real
ext-real
)
number
)
for
n
being ( ( ) (
natural
V24
()
real
ext-real
V86
()
V87
()
V134
()
V135
()
V136
()
V137
()
V138
()
V139
() )
Element
of
NAT
: ( ( ) (
V134
()
V135
()
V136
()
V137
()
V138
()
V139
()
V140
() )
Element
of
K32
(
REAL
: ( ( ) (
V134
()
V135
()
V136
()
V140
() )
set
) ) : ( ( ) ( )
set
) ) )
for
X
,
Y
being ( ( ) ( )
Subset
of ) holds
t
: ( (
real
) (
V24
()
real
ext-real
)
number
)
(.)
(
X
: ( ( ) ( )
Subset
of )
(+)
Y
: ( ( ) ( )
Subset
of )
)
: ( ( ) ( )
Element
of
K32
( the
carrier
of
(
TOP-REAL
b
2
: ( ( ) (
natural
V24
()
real
ext-real
V86
()
V87
()
V134
()
V135
()
V136
()
V137
()
V138
()
V139
() )
Element
of
NAT
: ( ( ) (
V134
()
V135
()
V136
()
V137
()
V138
()
V139
()
V140
() )
Element
of
K32
(
REAL
: ( ( ) (
V134
()
V135
()
V136
()
V140
() )
set
) ) : ( ( ) ( )
set
) ) )
)
: ( (
strict
) ( non
empty
TopSpace-like
left_complementable
right_complementable
Abelian
add-associative
right_zeroed
vector-distributive
scalar-distributive
scalar-associative
scalar-unital
V153
()
strict
)
RLTopStruct
) : ( ( ) ( non
empty
)
set
) ) : ( ( ) ( )
set
) ) : ( ( ) ( )
Subset
of )
=
(
t
: ( (
real
) (
V24
()
real
ext-real
)
number
)
(.)
X
: ( ( ) ( )
Subset
of )
)
: ( ( ) ( )
Subset
of )
(+)
(
t
: ( (
real
) (
V24
()
real
ext-real
)
number
)
(.)
Y
: ( ( ) ( )
Subset
of )
)
: ( ( ) ( )
Subset
of ) : ( ( ) ( )
Element
of
K32
( the
carrier
of
(
TOP-REAL
b
2
: ( ( ) (
natural
V24
()
real
ext-real
V86
()
V87
()
V134
()
V135
()
V136
()
V137
()
V138
()
V139
() )
Element
of
NAT
: ( ( ) (
V134
()
V135
()
V136
()
V137
()
V138
()
V139
()
V140
() )
Element
of
K32
(
REAL
: ( ( ) (
V134
()
V135
()
V136
()
V140
() )
set
) ) : ( ( ) ( )
set
) ) )
)
: ( (
strict
) ( non
empty
TopSpace-like
left_complementable
right_complementable
Abelian
add-associative
right_zeroed
vector-distributive
scalar-distributive
scalar-associative
scalar-unital
V153
()
strict
)
RLTopStruct
) : ( ( ) ( non
empty
)
set
) ) : ( ( ) ( )
set
) ) ;
theorem
:: MATHMORP:64
for
t
being ( (
real
) (
V24
()
real
ext-real
)
number
)
for
n
being ( ( ) (
natural
V24
()
real
ext-real
V86
()
V87
()
V134
()
V135
()
V136
()
V137
()
V138
()
V139
() )
Element
of
NAT
: ( ( ) (
V134
()
V135
()
V136
()
V137
()
V138
()
V139
()
V140
() )
Element
of
K32
(
REAL
: ( ( ) (
V134
()
V135
()
V136
()
V140
() )
set
) ) : ( ( ) ( )
set
) ) )
for
X
,
Y
being ( ( ) ( )
Subset
of ) st
t
: ( (
real
) (
V24
()
real
ext-real
)
number
)
<>
0
: ( ( ) (
empty
natural
V24
()
real
ext-real
non
positive
non
negative
V86
()
V87
()
V134
()
V135
()
V136
()
V137
()
V138
()
V139
()
V140
() )
Element
of
NAT
: ( ( ) (
V134
()
V135
()
V136
()
V137
()
V138
()
V139
()
V140
() )
Element
of
K32
(
REAL
: ( ( ) (
V134
()
V135
()
V136
()
V140
() )
set
) ) : ( ( ) ( )
set
) ) ) holds
t
: ( (
real
) (
V24
()
real
ext-real
)
number
)
(.)
(
X
: ( ( ) ( )
Subset
of )
(-)
Y
: ( ( ) ( )
Subset
of )
)
: ( ( ) ( )
Subset
of ) : ( ( ) ( )
Subset
of )
=
(
t
: ( (
real
) (
V24
()
real
ext-real
)
number
)
(.)
X
: ( ( ) ( )
Subset
of )
)
: ( ( ) ( )
Subset
of )
(-)
(
t
: ( (
real
) (
V24
()
real
ext-real
)
number
)
(.)
Y
: ( ( ) ( )
Subset
of )
)
: ( ( ) ( )
Subset
of ) : ( ( ) ( )
Subset
of ) ;
theorem
:: MATHMORP:65
for
t
being ( (
real
) (
V24
()
real
ext-real
)
number
)
for
n
being ( ( ) (
natural
V24
()
real
ext-real
V86
()
V87
()
V134
()
V135
()
V136
()
V137
()
V138
()
V139
() )
Element
of
NAT
: ( ( ) (
V134
()
V135
()
V136
()
V137
()
V138
()
V139
()
V140
() )
Element
of
K32
(
REAL
: ( ( ) (
V134
()
V135
()
V136
()
V140
() )
set
) ) : ( ( ) ( )
set
) ) )
for
X
,
Y
being ( ( ) ( )
Subset
of ) st
t
: ( (
real
) (
V24
()
real
ext-real
)
number
)
<>
0
: ( ( ) (
empty
natural
V24
()
real
ext-real
non
positive
non
negative
V86
()
V87
()
V134
()
V135
()
V136
()
V137
()
V138
()
V139
()
V140
() )
Element
of
NAT
: ( ( ) (
V134
()
V135
()
V136
()
V137
()
V138
()
V139
()
V140
() )
Element
of
K32
(
REAL
: ( ( ) (
V134
()
V135
()
V136
()
V140
() )
set
) ) : ( ( ) ( )
set
) ) ) holds
t
: ( (
real
) (
V24
()
real
ext-real
)
number
)
(.)
(
X
: ( ( ) ( )
Subset
of )
(O)
Y
: ( ( ) ( )
Subset
of )
)
: ( ( ) ( )
Subset
of ) : ( ( ) ( )
Subset
of )
=
(
t
: ( (
real
) (
V24
()
real
ext-real
)
number
)
(.)
X
: ( ( ) ( )
Subset
of )
)
: ( ( ) ( )
Subset
of )
(O)
(
t
: ( (
real
) (
V24
()
real
ext-real
)
number
)
(.)
Y
: ( ( ) ( )
Subset
of )
)
: ( ( ) ( )
Subset
of ) : ( ( ) ( )
Subset
of ) ;
theorem
:: MATHMORP:66
for
t
being ( (
real
) (
V24
()
real
ext-real
)
number
)
for
n
being ( ( ) (
natural
V24
()
real
ext-real
V86
()
V87
()
V134
()
V135
()
V136
()
V137
()
V138
()
V139
() )
Element
of
NAT
: ( ( ) (
V134
()
V135
()
V136
()
V137
()
V138
()
V139
()
V140
() )
Element
of
K32
(
REAL
: ( ( ) (
V134
()
V135
()
V136
()
V140
() )
set
) ) : ( ( ) ( )
set
) ) )
for
X
,
Y
being ( ( ) ( )
Subset
of ) st
t
: ( (
real
) (
V24
()
real
ext-real
)
number
)
<>
0
: ( ( ) (
empty
natural
V24
()
real
ext-real
non
positive
non
negative
V86
()
V87
()
V134
()
V135
()
V136
()
V137
()
V138
()
V139
()
V140
() )
Element
of
NAT
: ( ( ) (
V134
()
V135
()
V136
()
V137
()
V138
()
V139
()
V140
() )
Element
of
K32
(
REAL
: ( ( ) (
V134
()
V135
()
V136
()
V140
() )
set
) ) : ( ( ) ( )
set
) ) ) holds
t
: ( (
real
) (
V24
()
real
ext-real
)
number
)
(.)
(
X
: ( ( ) ( )
Subset
of )
(o)
Y
: ( ( ) ( )
Subset
of )
)
: ( ( ) ( )
Subset
of ) : ( ( ) ( )
Subset
of )
=
(
t
: ( (
real
) (
V24
()
real
ext-real
)
number
)
(.)
X
: ( ( ) ( )
Subset
of )
)
: ( ( ) ( )
Subset
of )
(o)
(
t
: ( (
real
) (
V24
()
real
ext-real
)
number
)
(.)
Y
: ( ( ) ( )
Subset
of )
)
: ( ( ) ( )
Subset
of ) : ( ( ) ( )
Subset
of ) ;
begin
definition
let
T
be ( ( non
empty
) ( non
empty
)
RLSStruct
) ;
let
X
,
B1
,
B2
be ( ( ) ( )
Subset
of ) ;
func
X
(*)
(
B1
,
B2
)
->
( ( ) ( )
Subset
of )
equals
:: MATHMORP:def 7
(
X
: ( ( ) ( )
Element
of
T
: ( ( ) ( )
RLTopStruct
) )
(-)
B1
: ( (
V12
()
V30
(
K33
(
T
: ( ( ) ( )
RLTopStruct
) ,
T
: ( ( ) ( )
RLTopStruct
) ) : ( ( ) ( )
set
) ,
T
: ( ( ) ( )
RLTopStruct
) ) ) (
V12
()
V30
(
K33
(
T
: ( ( ) ( )
RLTopStruct
) ,
T
: ( ( ) ( )
RLTopStruct
) ) : ( ( ) ( )
set
) ,
T
: ( ( ) ( )
RLTopStruct
) ) )
Element
of
K32
(
K33
(
K33
(
T
: ( ( ) ( )
RLTopStruct
) ,
T
: ( ( ) ( )
RLTopStruct
) ) : ( ( ) ( )
set
) ,
T
: ( ( ) ( )
RLTopStruct
) ) : ( ( ) ( )
set
) ) : ( ( ) ( )
set
) )
)
: ( ( ) ( )
Subset
of )
/\
(
(
X
: ( ( ) ( )
Element
of
T
: ( ( ) ( )
RLTopStruct
) )
`
)
: ( ( ) ( )
Element
of
K32
( the
carrier
of
T
: ( ( ) ( )
RLTopStruct
) : ( ( ) ( )
set
) ) : ( ( ) ( )
set
) )
(-)
B2
: ( (
V12
()
V30
(
K33
(
REAL
: ( ( ) (
V134
()
V135
()
V136
()
V140
() )
set
) ,
T
: ( ( ) ( )
RLTopStruct
) ) : ( ( ) ( )
set
) ,
T
: ( ( ) ( )
RLTopStruct
) ) ) (
V12
()
V30
(
K33
(
REAL
: ( ( ) (
V134
()
V135
()
V136
()
V140
() )
set
) ,
T
: ( ( ) ( )
RLTopStruct
) ) : ( ( ) ( )
set
) ,
T
: ( ( ) ( )
RLTopStruct
) ) )
Element
of
K32
(
K33
(
K33
(
REAL
: ( ( ) (
V134
()
V135
()
V136
()
V140
() )
set
) ,
T
: ( ( ) ( )
RLTopStruct
) ) : ( ( ) ( )
set
) ,
T
: ( ( ) ( )
RLTopStruct
) ) : ( ( ) ( )
set
) ) : ( ( ) ( )
set
) )
)
: ( ( ) ( )
Subset
of ) : ( ( ) ( )
Element
of
K32
( the
carrier
of
T
: ( ( ) ( )
RLTopStruct
) : ( ( ) ( )
set
) ) : ( ( ) ( )
set
) ) ;
end;
definition
let
T
be ( ( non
empty
) ( non
empty
)
RLSStruct
) ;
let
X
,
B1
,
B2
be ( ( ) ( )
Subset
of ) ;
func
X
(&)
(
B1
,
B2
)
->
( ( ) ( )
Subset
of )
equals
:: MATHMORP:def 8
X
: ( ( ) ( )
Element
of
T
: ( ( ) ( )
RLTopStruct
) )
\/
(
X
: ( ( ) ( )
Element
of
T
: ( ( ) ( )
RLTopStruct
) )
(*)
(
B1
: ( (
V12
()
V30
(
K33
(
T
: ( ( ) ( )
RLTopStruct
) ,
T
: ( ( ) ( )
RLTopStruct
) ) : ( ( ) ( )
set
) ,
T
: ( ( ) ( )
RLTopStruct
) ) ) (
V12
()
V30
(
K33
(
T
: ( ( ) ( )
RLTopStruct
) ,
T
: ( ( ) ( )
RLTopStruct
) ) : ( ( ) ( )
set
) ,
T
: ( ( ) ( )
RLTopStruct
) ) )
Element
of
K32
(
K33
(
K33
(
T
: ( ( ) ( )
RLTopStruct
) ,
T
: ( ( ) ( )
RLTopStruct
) ) : ( ( ) ( )
set
) ,
T
: ( ( ) ( )
RLTopStruct
) ) : ( ( ) ( )
set
) ) : ( ( ) ( )
set
) ) ,
B2
: ( (
V12
()
V30
(
K33
(
REAL
: ( ( ) (
V134
()
V135
()
V136
()
V140
() )
set
) ,
T
: ( ( ) ( )
RLTopStruct
) ) : ( ( ) ( )
set
) ,
T
: ( ( ) ( )
RLTopStruct
) ) ) (
V12
()
V30
(
K33
(
REAL
: ( ( ) (
V134
()
V135
()
V136
()
V140
() )
set
) ,
T
: ( ( ) ( )
RLTopStruct
) ) : ( ( ) ( )
set
) ,
T
: ( ( ) ( )
RLTopStruct
) ) )
Element
of
K32
(
K33
(
K33
(
REAL
: ( ( ) (
V134
()
V135
()
V136
()
V140
() )
set
) ,
T
: ( ( ) ( )
RLTopStruct
) ) : ( ( ) ( )
set
) ,
T
: ( ( ) ( )
RLTopStruct
) ) : ( ( ) ( )
set
) ) : ( ( ) ( )
set
) ) )
)
: ( ( ) ( )
Subset
of ) : ( ( ) ( )
Element
of
K32
( the
carrier
of
T
: ( ( ) ( )
RLTopStruct
) : ( ( ) ( )
set
) ) : ( ( ) ( )
set
) ) ;
end;
definition
let
T
be ( ( non
empty
) ( non
empty
)
RLSStruct
) ;
let
X
,
B1
,
B2
be ( ( ) ( )
Subset
of ) ;
func
X
(@)
(
B1
,
B2
)
->
( ( ) ( )
Subset
of )
equals
:: MATHMORP:def 9
X
: ( ( ) ( )
Element
of
T
: ( ( ) ( )
RLTopStruct
) )
\
(
X
: ( ( ) ( )
Element
of
T
: ( ( ) ( )
RLTopStruct
) )
(*)
(
B1
: ( (
V12
()
V30
(
K33
(
T
: ( ( ) ( )
RLTopStruct
) ,
T
: ( ( ) ( )
RLTopStruct
) ) : ( ( ) ( )
set
) ,
T
: ( ( ) ( )
RLTopStruct
) ) ) (
V12
()
V30
(
K33
(
T
: ( ( ) ( )
RLTopStruct
) ,
T
: ( ( ) ( )
RLTopStruct
) ) : ( ( ) ( )
set
) ,
T
: ( ( ) ( )
RLTopStruct
) ) )
Element
of
K32
(
K33
(
K33
(
T
: ( ( ) ( )
RLTopStruct
) ,
T
: ( ( ) ( )
RLTopStruct
) ) : ( ( ) ( )
set
) ,
T
: ( ( ) ( )
RLTopStruct
) ) : ( ( ) ( )
set
) ) : ( ( ) ( )
set
) ) ,
B2
: ( (
V12
()
V30
(
K33
(
REAL
: ( ( ) (
V134
()
V135
()
V136
()
V140
() )
set
) ,
T
: ( ( ) ( )
RLTopStruct
) ) : ( ( ) ( )
set
) ,
T
: ( ( ) ( )
RLTopStruct
) ) ) (
V12
()
V30
(
K33
(
REAL
: ( ( ) (
V134
()
V135
()
V136
()
V140
() )
set
) ,
T
: ( ( ) ( )
RLTopStruct
) ) : ( ( ) ( )
set
) ,
T
: ( ( ) ( )
RLTopStruct
) ) )
Element
of
K32
(
K33
(
K33
(
REAL
: ( ( ) (
V134
()
V135
()
V136
()
V140
() )
set
) ,
T
: ( ( ) ( )
RLTopStruct
) ) : ( ( ) ( )
set
) ,
T
: ( ( ) ( )
RLTopStruct
) ) : ( ( ) ( )
set
) ) : ( ( ) ( )
set
) ) )
)
: ( ( ) ( )
Subset
of ) : ( ( ) ( )
Element
of
K32
( the
carrier
of
T
: ( ( ) ( )
RLTopStruct
) : ( ( ) ( )
set
) ) : ( ( ) ( )
set
) ) ;
end;
theorem
:: MATHMORP:67
for
n
being ( ( ) (
natural
V24
()
real
ext-real
V86
()
V87
()
V134
()
V135
()
V136
()
V137
()
V138
()
V139
() )
Element
of
NAT
: ( ( ) (
V134
()
V135
()
V136
()
V137
()
V138
()
V139
()
V140
() )
Element
of
K32
(
REAL
: ( ( ) (
V134
()
V135
()
V136
()
V140
() )
set
) ) : ( ( ) ( )
set
) ) )
for
B1
,
X
,
B2
being ( ( ) ( )
Subset
of ) st
B1
: ( ( ) ( )
Subset
of )
=
{}
: ( ( ) (
empty
V134
()
V135
()
V136
()
V137
()
V138
()
V139
()
V140
() )
set
) holds
X
: ( ( ) ( )
Subset
of )
(*)
(
B1
: ( ( ) ( )
Subset
of ) ,
B2
: ( ( ) ( )
Subset
of ) ) : ( ( ) ( )
Subset
of )
=
(
X
: ( ( ) ( )
Subset
of )
`
)
: ( ( ) ( )
Element
of
K32
( the
carrier
of
(
TOP-REAL
b
1
: ( ( ) (
natural
V24
()
real
ext-real
V86
()
V87
()
V134
()
V135
()
V136
()
V137
()
V138
()
V139
() )
Element
of
NAT
: ( ( ) (
V134
()
V135
()
V136
()
V137
()
V138
()
V139
()
V140
() )
Element
of
K32
(
REAL
: ( ( ) (
V134
()
V135
()
V136
()
V140
() )
set
) ) : ( ( ) ( )
set
) ) )
)
: ( (
strict
) ( non
empty
TopSpace-like
left_complementable
right_complementable
Abelian
add-associative
right_zeroed
vector-distributive
scalar-distributive
scalar-associative
scalar-unital
V153
()
strict
)
RLTopStruct
) : ( ( ) ( non
empty
)
set
) ) : ( ( ) ( )
set
) )
(-)
B2
: ( ( ) ( )
Subset
of ) : ( ( ) ( )
Subset
of ) ;
theorem
:: MATHMORP:68
for
n
being ( ( ) (
natural
V24
()
real
ext-real
V86
()
V87
()
V134
()
V135
()
V136
()
V137
()
V138
()
V139
() )
Element
of
NAT
: ( ( ) (
V134
()
V135
()
V136
()
V137
()
V138
()
V139
()
V140
() )
Element
of
K32
(
REAL
: ( ( ) (
V134
()
V135
()
V136
()
V140
() )
set
) ) : ( ( ) ( )
set
) ) )
for
B2
,
X
,
B1
being ( ( ) ( )
Subset
of ) st
B2
: ( ( ) ( )
Subset
of )
=
{}
: ( ( ) (
empty
V134
()
V135
()
V136
()
V137
()
V138
()
V139
()
V140
() )
set
) holds
X
: ( ( ) ( )
Subset
of )
(*)
(
B1
: ( ( ) ( )
Subset
of ) ,
B2
: ( ( ) ( )
Subset
of ) ) : ( ( ) ( )
Subset
of )
=
X
: ( ( ) ( )
Subset
of )
(-)
B1
: ( ( ) ( )
Subset
of ) : ( ( ) ( )
Subset
of ) ;
theorem
:: MATHMORP:69
for
n
being ( ( ) (
natural
V24
()
real
ext-real
V86
()
V87
()
V134
()
V135
()
V136
()
V137
()
V138
()
V139
() )
Element
of
NAT
: ( ( ) (
V134
()
V135
()
V136
()
V137
()
V138
()
V139
()
V140
() )
Element
of
K32
(
REAL
: ( ( ) (
V134
()
V135
()
V136
()
V140
() )
set
) ) : ( ( ) ( )
set
) ) )
for
B1
,
X
,
B2
being ( ( ) ( )
Subset
of ) st
0.
(
TOP-REAL
n
: ( ( ) (
natural
V24
()
real
ext-real
V86
()
V87
()
V134
()
V135
()
V136
()
V137
()
V138
()
V139
() )
Element
of
NAT
: ( ( ) (
V134
()
V135
()
V136
()
V137
()
V138
()
V139
()
V140
() )
Element
of
K32
(
REAL
: ( ( ) (
V134
()
V135
()
V136
()
V140
() )
set
) ) : ( ( ) ( )
set
) ) )
)
: ( (
strict
) ( non
empty
TopSpace-like
left_complementable
right_complementable
Abelian
add-associative
right_zeroed
vector-distributive
scalar-distributive
scalar-associative
scalar-unital
V153
()
strict
)
RLTopStruct
) : ( ( ) (
V40
(
b
1
: ( ( ) (
natural
V24
()
real
ext-real
V86
()
V87
()
V134
()
V135
()
V136
()
V137
()
V138
()
V139
() )
Element
of
NAT
: ( ( ) (
V134
()
V135
()
V136
()
V137
()
V138
()
V139
()
V140
() )
Element
of
K32
(
REAL
: ( ( ) (
V134
()
V135
()
V136
()
V140
() )
set
) ) : ( ( ) ( )
set
) ) ) )
V49
(
TOP-REAL
b
1
: ( ( ) (
natural
V24
()
real
ext-real
V86
()
V87
()
V134
()
V135
()
V136
()
V137
()
V138
()
V139
() )
Element
of
NAT
: ( ( ) (
V134
()
V135
()
V136
()
V137
()
V138
()
V139
()
V140
() )
Element
of
K32
(
REAL
: ( ( ) (
V134
()
V135
()
V136
()
V140
() )
set
) ) : ( ( ) ( )
set
) ) ) : ( (
strict
) ( non
empty
TopSpace-like
left_complementable
right_complementable
Abelian
add-associative
right_zeroed
vector-distributive
scalar-distributive
scalar-associative
scalar-unital
V153
()
strict
)
RLTopStruct
) )
V83
()
V126
() )
Element
of the
carrier
of
(
TOP-REAL
b
1
: ( ( ) (
natural
V24
()
real
ext-real
V86
()
V87
()
V134
()
V135
()
V136
()
V137
()
V138
()
V139
() )
Element
of
NAT
: ( ( ) (
V134
()
V135
()
V136
()
V137
()
V138
()
V139
()
V140
() )
Element
of
K32
(
REAL
: ( ( ) (
V134
()
V135
()
V136
()
V140
() )
set
) ) : ( ( ) ( )
set
) ) )
)
: ( (
strict
) ( non
empty
TopSpace-like
left_complementable
right_complementable
Abelian
add-associative
right_zeroed
vector-distributive
scalar-distributive
scalar-associative
scalar-unital
V153
()
strict
)
RLTopStruct
) : ( ( ) ( non
empty
)
set
) )
in
B1
: ( ( ) ( )
Subset
of ) holds
X
: ( ( ) ( )
Subset
of )
(*)
(
B1
: ( ( ) ( )
Subset
of ) ,
B2
: ( ( ) ( )
Subset
of ) ) : ( ( ) ( )
Subset
of )
c=
X
: ( ( ) ( )
Subset
of ) ;
theorem
:: MATHMORP:70
for
n
being ( ( ) (
natural
V24
()
real
ext-real
V86
()
V87
()
V134
()
V135
()
V136
()
V137
()
V138
()
V139
() )
Element
of
NAT
: ( ( ) (
V134
()
V135
()
V136
()
V137
()
V138
()
V139
()
V140
() )
Element
of
K32
(
REAL
: ( ( ) (
V134
()
V135
()
V136
()
V140
() )
set
) ) : ( ( ) ( )
set
) ) )
for
B2
,
X
,
B1
being ( ( ) ( )
Subset
of ) st
0.
(
TOP-REAL
n
: ( ( ) (
natural
V24
()
real
ext-real
V86
()
V87
()
V134
()
V135
()
V136
()
V137
()
V138
()
V139
() )
Element
of
NAT
: ( ( ) (
V134
()
V135
()
V136
()
V137
()
V138
()
V139
()
V140
() )
Element
of
K32
(
REAL
: ( ( ) (
V134
()
V135
()
V136
()
V140
() )
set
) ) : ( ( ) ( )
set
) ) )
)
: ( (
strict
) ( non
empty
TopSpace-like
left_complementable
right_complementable
Abelian
add-associative
right_zeroed
vector-distributive
scalar-distributive
scalar-associative
scalar-unital
V153
()
strict
)
RLTopStruct
) : ( ( ) (
V40
(
b
1
: ( ( ) (
natural
V24
()
real
ext-real
V86
()
V87
()
V134
()
V135
()
V136
()
V137
()
V138
()
V139
() )
Element
of
NAT
: ( ( ) (
V134
()
V135
()
V136
()
V137
()
V138
()
V139
()
V140
() )
Element
of
K32
(
REAL
: ( ( ) (
V134
()
V135
()
V136
()
V140
() )
set
) ) : ( ( ) ( )
set
) ) ) )
V49
(
TOP-REAL
b
1
: ( ( ) (
natural
V24
()
real
ext-real
V86
()
V87
()
V134
()
V135
()
V136
()
V137
()
V138
()
V139
() )
Element
of
NAT
: ( ( ) (
V134
()
V135
()
V136
()
V137
()
V138
()
V139
()
V140
() )
Element
of
K32
(
REAL
: ( ( ) (
V134
()
V135
()
V136
()
V140
() )
set
) ) : ( ( ) ( )
set
) ) ) : ( (
strict
) ( non
empty
TopSpace-like
left_complementable
right_complementable
Abelian
add-associative
right_zeroed
vector-distributive
scalar-distributive
scalar-associative
scalar-unital
V153
()
strict
)
RLTopStruct
) )
V83
()
V126
() )
Element
of the
carrier
of
(
TOP-REAL
b
1
: ( ( ) (
natural
V24
()
real
ext-real
V86
()
V87
()
V134
()
V135
()
V136
()
V137
()
V138
()
V139
() )
Element
of
NAT
: ( ( ) (
V134
()
V135
()
V136
()
V137
()
V138
()
V139
()
V140
() )
Element
of
K32
(
REAL
: ( ( ) (
V134
()
V135
()
V136
()
V140
() )
set
) ) : ( ( ) ( )
set
) ) )
)
: ( (
strict
) ( non
empty
TopSpace-like
left_complementable
right_complementable
Abelian
add-associative
right_zeroed
vector-distributive
scalar-distributive
scalar-associative
scalar-unital
V153
()
strict
)
RLTopStruct
) : ( ( ) ( non
empty
)
set
) )
in
B2
: ( ( ) ( )
Subset
of ) holds
(
X
: ( ( ) ( )
Subset
of )
(*)
(
B1
: ( ( ) ( )
Subset
of ) ,
B2
: ( ( ) ( )
Subset
of ) )
)
: ( ( ) ( )
Subset
of )
/\
X
: ( ( ) ( )
Subset
of ) : ( ( ) ( )
Element
of
K32
( the
carrier
of
(
TOP-REAL
b
1
: ( ( ) (
natural
V24
()
real
ext-real
V86
()
V87
()
V134
()
V135
()
V136
()
V137
()
V138
()
V139
() )
Element
of
NAT
: ( ( ) (
V134
()
V135
()
V136
()
V137
()
V138
()
V139
()
V140
() )
Element
of
K32
(
REAL
: ( ( ) (
V134
()
V135
()
V136
()
V140
() )
set
) ) : ( ( ) ( )
set
) ) )
)
: ( (
strict
) ( non
empty
TopSpace-like
left_complementable
right_complementable
Abelian
add-associative
right_zeroed
vector-distributive
scalar-distributive
scalar-associative
scalar-unital
V153
()
strict
)
RLTopStruct
) : ( ( ) ( non
empty
)
set
) ) : ( ( ) ( )
set
) )
=
{}
: ( ( ) (
empty
V134
()
V135
()
V136
()
V137
()
V138
()
V139
()
V140
() )
set
) ;
theorem
:: MATHMORP:71
for
n
being ( ( ) (
natural
V24
()
real
ext-real
V86
()
V87
()
V134
()
V135
()
V136
()
V137
()
V138
()
V139
() )
Element
of
NAT
: ( ( ) (
V134
()
V135
()
V136
()
V137
()
V138
()
V139
()
V140
() )
Element
of
K32
(
REAL
: ( ( ) (
V134
()
V135
()
V136
()
V140
() )
set
) ) : ( ( ) ( )
set
) ) )
for
B1
,
X
,
B2
being ( ( ) ( )
Subset
of ) st
0.
(
TOP-REAL
n
: ( ( ) (
natural
V24
()
real
ext-real
V86
()
V87
()
V134
()
V135
()
V136
()
V137
()
V138
()
V139
() )
Element
of
NAT
: ( ( ) (
V134
()
V135
()
V136
()
V137
()
V138
()
V139
()
V140
() )
Element
of
K32
(
REAL
: ( ( ) (
V134
()
V135
()
V136
()
V140
() )
set
) ) : ( ( ) ( )
set
) ) )
)
: ( (
strict
) ( non
empty
TopSpace-like
left_complementable
right_complementable
Abelian
add-associative
right_zeroed
vector-distributive
scalar-distributive
scalar-associative
scalar-unital
V153
()
strict
)
RLTopStruct
) : ( ( ) (
V40
(
b
1
: ( ( ) (
natural
V24
()
real
ext-real
V86
()
V87
()
V134
()
V135
()
V136
()
V137
()
V138
()
V139
() )
Element
of
NAT
: ( ( ) (
V134
()
V135
()
V136
()
V137
()
V138
()
V139
()
V140
() )
Element
of
K32
(
REAL
: ( ( ) (
V134
()
V135
()
V136
()
V140
() )
set
) ) : ( ( ) ( )
set
) ) ) )
V49
(
TOP-REAL
b
1
: ( ( ) (
natural
V24
()
real
ext-real
V86
()
V87
()
V134
()
V135
()
V136
()
V137
()
V138
()
V139
() )
Element
of
NAT
: ( ( ) (
V134
()
V135
()
V136
()
V137
()
V138
()
V139
()
V140
() )
Element
of
K32
(
REAL
: ( ( ) (
V134
()
V135
()
V136
()
V140
() )
set
) ) : ( ( ) ( )
set
) ) ) : ( (
strict
) ( non
empty
TopSpace-like
left_complementable
right_complementable
Abelian
add-associative
right_zeroed
vector-distributive
scalar-distributive
scalar-associative
scalar-unital
V153
()
strict
)
RLTopStruct
) )
V83
()
V126
() )
Element
of the
carrier
of
(
TOP-REAL
b
1
: ( ( ) (
natural
V24
()
real
ext-real
V86
()
V87
()
V134
()
V135
()
V136
()
V137
()
V138
()
V139
() )
Element
of
NAT
: ( ( ) (
V134
()
V135
()
V136
()
V137
()
V138
()
V139
()
V140
() )
Element
of
K32
(
REAL
: ( ( ) (
V134
()
V135
()
V136
()
V140
() )
set
) ) : ( ( ) ( )
set
) ) )
)
: ( (
strict
) ( non
empty
TopSpace-like
left_complementable
right_complementable
Abelian
add-associative
right_zeroed
vector-distributive
scalar-distributive
scalar-associative
scalar-unital
V153
()
strict
)
RLTopStruct
) : ( ( ) ( non
empty
)
set
) )
in
B1
: ( ( ) ( )
Subset
of ) holds
X
: ( ( ) ( )
Subset
of )
(&)
(
B1
: ( ( ) ( )
Subset
of ) ,
B2
: ( ( ) ( )
Subset
of ) ) : ( ( ) ( )
Subset
of )
=
X
: ( ( ) ( )
Subset
of ) ;
theorem
:: MATHMORP:72
for
n
being ( ( ) (
natural
V24
()
real
ext-real
V86
()
V87
()
V134
()
V135
()
V136
()
V137
()
V138
()
V139
() )
Element
of
NAT
: ( ( ) (
V134
()
V135
()
V136
()
V137
()
V138
()
V139
()
V140
() )
Element
of
K32
(
REAL
: ( ( ) (
V134
()
V135
()
V136
()
V140
() )
set
) ) : ( ( ) ( )
set
) ) )
for
B2
,
X
,
B1
being ( ( ) ( )
Subset
of ) st
0.
(
TOP-REAL
n
: ( ( ) (
natural
V24
()
real
ext-real
V86
()
V87
()
V134
()
V135
()
V136
()
V137
()
V138
()
V139
() )
Element
of
NAT
: ( ( ) (
V134
()
V135
()
V136
()
V137
()
V138
()
V139
()
V140
() )
Element
of
K32
(
REAL
: ( ( ) (
V134
()
V135
()
V136
()
V140
() )
set
) ) : ( ( ) ( )
set
) ) )
)
: ( (
strict
) ( non
empty
TopSpace-like
left_complementable
right_complementable
Abelian
add-associative
right_zeroed
vector-distributive
scalar-distributive
scalar-associative
scalar-unital
V153
()
strict
)
RLTopStruct
) : ( ( ) (
V40
(
b
1
: ( ( ) (
natural
V24
()
real
ext-real
V86
()
V87
()
V134
()
V135
()
V136
()
V137
()
V138
()
V139
() )
Element
of
NAT
: ( ( ) (
V134
()
V135
()
V136
()
V137
()
V138
()
V139
()
V140
() )
Element
of
K32
(
REAL
: ( ( ) (
V134
()
V135
()
V136
()
V140
() )
set
) ) : ( ( ) ( )
set
) ) ) )
V49
(
TOP-REAL
b
1
: ( ( ) (
natural
V24
()
real
ext-real
V86
()
V87
()
V134
()
V135
()
V136
()
V137
()
V138
()
V139
() )
Element
of
NAT
: ( ( ) (
V134
()
V135
()
V136
()
V137
()
V138
()
V139
()
V140
() )
Element
of
K32
(
REAL
: ( ( ) (
V134
()
V135
()
V136
()
V140
() )
set
) ) : ( ( ) ( )
set
) ) ) : ( (
strict
) ( non
empty
TopSpace-like
left_complementable
right_complementable
Abelian
add-associative
right_zeroed
vector-distributive
scalar-distributive
scalar-associative
scalar-unital
V153
()
strict
)
RLTopStruct
) )
V83
()
V126
() )
Element
of the
carrier
of
(
TOP-REAL
b
1
: ( ( ) (
natural
V24
()
real
ext-real
V86
()
V87
()
V134
()
V135
()
V136
()
V137
()
V138
()
V139
() )
Element
of
NAT
: ( ( ) (
V134
()
V135
()
V136
()
V137
()
V138
()
V139
()
V140
() )
Element
of
K32
(
REAL
: ( ( ) (
V134
()
V135
()
V136
()
V140
() )
set
) ) : ( ( ) ( )
set
) ) )
)
: ( (
strict
) ( non
empty
TopSpace-like
left_complementable
right_complementable
Abelian
add-associative
right_zeroed
vector-distributive
scalar-distributive
scalar-associative
scalar-unital
V153
()
strict
)
RLTopStruct
) : ( ( ) ( non
empty
)
set
) )
in
B2
: ( ( ) ( )
Subset
of ) holds
X
: ( ( ) ( )
Subset
of )
(@)
(
B1
: ( ( ) ( )
Subset
of ) ,
B2
: ( ( ) ( )
Subset
of ) ) : ( ( ) ( )
Subset
of )
=
X
: ( ( ) ( )
Subset
of ) ;
theorem
:: MATHMORP:73
for
n
being ( ( ) (
natural
V24
()
real
ext-real
V86
()
V87
()
V134
()
V135
()
V136
()
V137
()
V138
()
V139
() )
Element
of
NAT
: ( ( ) (
V134
()
V135
()
V136
()
V137
()
V138
()
V139
()
V140
() )
Element
of
K32
(
REAL
: ( ( ) (
V134
()
V135
()
V136
()
V140
() )
set
) ) : ( ( ) ( )
set
) ) )
for
X
,
B2
,
B1
being ( ( ) ( )
Subset
of ) holds
X
: ( ( ) ( )
Subset
of )
(@)
(
B2
: ( ( ) ( )
Subset
of ) ,
B1
: ( ( ) ( )
Subset
of ) ) : ( ( ) ( )
Subset
of )
=
(
(
X
: ( ( ) ( )
Subset
of )
`
)
: ( ( ) ( )
Element
of
K32
( the
carrier
of
(
TOP-REAL
b
1
: ( ( ) (
natural
V24
()
real
ext-real
V86
()
V87
()
V134
()
V135
()
V136
()
V137
()
V138
()
V139
() )
Element
of
NAT
: ( ( ) (
V134
()
V135
()
V136
()
V137
()
V138
()
V139
()
V140
() )
Element
of
K32
(
REAL
: ( ( ) (
V134
()
V135
()
V136
()
V140
() )
set
) ) : ( ( ) ( )
set
) ) )
)
: ( (
strict
) ( non
empty
TopSpace-like
left_complementable
right_complementable
Abelian
add-associative
right_zeroed
vector-distributive
scalar-distributive
scalar-associative
scalar-unital
V153
()
strict
)
RLTopStruct
) : ( ( ) ( non
empty
)
set
) ) : ( ( ) ( )
set
) )
(&)
(
B1
: ( ( ) ( )
Subset
of ) ,
B2
: ( ( ) ( )
Subset
of ) )
)
: ( ( ) ( )
Subset
of )
`
: ( ( ) ( )
Element
of
K32
( the
carrier
of
(
TOP-REAL
b
1
: ( ( ) (
natural
V24
()
real
ext-real
V86
()
V87
()
V134
()
V135
()
V136
()
V137
()
V138
()
V139
() )
Element
of
NAT
: ( ( ) (
V134
()
V135
()
V136
()
V137
()
V138
()
V139
()
V140
() )
Element
of
K32
(
REAL
: ( ( ) (
V134
()
V135
()
V136
()
V140
() )
set
) ) : ( ( ) ( )
set
) ) )
)
: ( (
strict
) ( non
empty
TopSpace-like
left_complementable
right_complementable
Abelian
add-associative
right_zeroed
vector-distributive
scalar-distributive
scalar-associative
scalar-unital
V153
()
strict
)
RLTopStruct
) : ( ( ) ( non
empty
)
set
) ) : ( ( ) ( )
set
) ) ;
begin
theorem
:: MATHMORP:74
for
V
being ( ( non
empty
right_complementable
Abelian
add-associative
right_zeroed
vector-distributive
scalar-distributive
scalar-associative
scalar-unital
) ( non
empty
left_complementable
right_complementable
Abelian
add-associative
right_zeroed
vector-distributive
scalar-distributive
scalar-associative
scalar-unital
V153
() )
RealLinearSpace
)
for
B
being ( ( ) ( )
Subset
of ) holds
(
B
: ( ( ) ( )
Subset
of ) is
convex
iff for
x
,
y
being ( ( ) ( )
Point
of ( ( ) ( non
empty
)
set
) )
for
r
being ( (
real
) (
V24
()
real
ext-real
)
number
) st
0
: ( ( ) (
empty
natural
V24
()
real
ext-real
non
positive
non
negative
V86
()
V87
()
V134
()
V135
()
V136
()
V137
()
V138
()
V139
()
V140
() )
Element
of
NAT
: ( ( ) (
V134
()
V135
()
V136
()
V137
()
V138
()
V139
()
V140
() )
Element
of
K32
(
REAL
: ( ( ) (
V134
()
V135
()
V136
()
V140
() )
set
) ) : ( ( ) ( )
set
) ) )
<=
r
: ( (
real
) (
V24
()
real
ext-real
)
number
) &
r
: ( (
real
) (
V24
()
real
ext-real
)
number
)
<=
1 : ( ( ) ( non
empty
natural
V24
()
real
ext-real
positive
non
negative
V86
()
V87
()
V134
()
V135
()
V136
()
V137
()
V138
()
V139
() )
Element
of
NAT
: ( ( ) (
V134
()
V135
()
V136
()
V137
()
V138
()
V139
()
V140
() )
Element
of
K32
(
REAL
: ( ( ) (
V134
()
V135
()
V136
()
V140
() )
set
) ) : ( ( ) ( )
set
) ) ) &
x
: ( ( ) ( )
Point
of ( ( ) ( non
empty
)
set
) )
in
B
: ( ( ) ( )
Subset
of ) &
y
: ( ( ) ( )
Point
of ( ( ) ( non
empty
)
set
) )
in
B
: ( ( ) ( )
Subset
of ) holds
(
r
: ( (
real
) (
V24
()
real
ext-real
)
number
)
*
x
: ( ( ) ( )
Point
of ( ( ) ( non
empty
)
set
) )
)
: ( ( ) ( )
Element
of the
carrier
of
b
1
: ( ( non
empty
right_complementable
Abelian
add-associative
right_zeroed
vector-distributive
scalar-distributive
scalar-associative
scalar-unital
) ( non
empty
left_complementable
right_complementable
Abelian
add-associative
right_zeroed
vector-distributive
scalar-distributive
scalar-associative
scalar-unital
V153
() )
RealLinearSpace
) : ( ( ) ( non
empty
)
set
) )
+
(
(
1 : ( ( ) ( non
empty
natural
V24
()
real
ext-real
positive
non
negative
V86
()
V87
()
V134
()
V135
()
V136
()
V137
()
V138
()
V139
() )
Element
of
NAT
: ( ( ) (
V134
()
V135
()
V136
()
V137
()
V138
()
V139
()
V140
() )
Element
of
K32
(
REAL
: ( ( ) (
V134
()
V135
()
V136
()
V140
() )
set
) ) : ( ( ) ( )
set
) ) )
-
r
: ( (
real
) (
V24
()
real
ext-real
)
number
)
)
: ( ( ) (
V24
()
real
ext-real
)
Element
of
REAL
: ( ( ) (
V134
()
V135
()
V136
()
V140
() )
set
) )
*
y
: ( ( ) ( )
Point
of ( ( ) ( non
empty
)
set
) )
)
: ( ( ) ( )
Element
of the
carrier
of
b
1
: ( ( non
empty
right_complementable
Abelian
add-associative
right_zeroed
vector-distributive
scalar-distributive
scalar-associative
scalar-unital
) ( non
empty
left_complementable
right_complementable
Abelian
add-associative
right_zeroed
vector-distributive
scalar-distributive
scalar-associative
scalar-unital
V153
() )
RealLinearSpace
) : ( ( ) ( non
empty
)
set
) ) : ( ( ) ( )
Element
of the
carrier
of
b
1
: ( ( non
empty
right_complementable
Abelian
add-associative
right_zeroed
vector-distributive
scalar-distributive
scalar-associative
scalar-unital
) ( non
empty
left_complementable
right_complementable
Abelian
add-associative
right_zeroed
vector-distributive
scalar-distributive
scalar-associative
scalar-unital
V153
() )
RealLinearSpace
) : ( ( ) ( non
empty
)
set
) )
in
B
: ( ( ) ( )
Subset
of ) ) ;
definition
let
V
be ( ( non
empty
right_complementable
Abelian
add-associative
right_zeroed
vector-distributive
scalar-distributive
scalar-associative
scalar-unital
) ( non
empty
left_complementable
right_complementable
Abelian
add-associative
right_zeroed
vector-distributive
scalar-distributive
scalar-associative
scalar-unital
V153
() )
RealLinearSpace
) ;
let
B
be ( ( ) ( )
Subset
of ) ;
redefine
attr
B
is
convex
means
:: MATHMORP:def 10
for
x
,
y
being ( ( ) ( )
Point
of ( ( ) ( )
set
) )
for
r
being ( (
real
) (
V24
()
real
ext-real
)
number
) st
0
: ( ( ) (
empty
natural
V24
()
real
ext-real
non
positive
non
negative
V86
()
V87
()
V134
()
V135
()
V136
()
V137
()
V138
()
V139
()
V140
() )
Element
of
NAT
: ( ( ) (
V134
()
V135
()
V136
()
V137
()
V138
()
V139
()
V140
() )
Element
of
K32
(
REAL
: ( ( ) (
V134
()
V135
()
V136
()
V140
() )
set
) ) : ( ( ) ( )
set
) ) )
<=
r
: ( (
real
) (
V24
()
real
ext-real
)
number
) &
r
: ( (
real
) (
V24
()
real
ext-real
)
number
)
<=
1 : ( ( ) ( non
empty
natural
V24
()
real
ext-real
positive
non
negative
V86
()
V87
()
V134
()
V135
()
V136
()
V137
()
V138
()
V139
() )
Element
of
NAT
: ( ( ) (
V134
()
V135
()
V136
()
V137
()
V138
()
V139
()
V140
() )
Element
of
K32
(
REAL
: ( ( ) (
V134
()
V135
()
V136
()
V140
() )
set
) ) : ( ( ) ( )
set
) ) ) &
x
: ( ( ) ( )
Point
of ( ( ) ( non
empty
)
set
) )
in
B
: ( ( ) ( )
Element
of
V
: ( ( ) ( )
RLTopStruct
) ) &
y
: ( ( ) ( )
Point
of ( ( ) ( non
empty
)
set
) )
in
B
: ( ( ) ( )
Element
of
V
: ( ( ) ( )
RLTopStruct
) ) holds
(
r
: ( (
real
) (
V24
()
real
ext-real
)
number
)
*
x
: ( ( ) ( )
Point
of ( ( ) ( non
empty
)
set
) )
)
: ( ( ) ( )
Element
of the
carrier
of
V
: ( ( ) ( )
RLTopStruct
) : ( ( ) ( )
set
) )
+
(
(
1 : ( ( ) ( non
empty
natural
V24
()
real
ext-real
positive
non
negative
V86
()
V87
()
V134
()
V135
()
V136
()
V137
()
V138
()
V139
() )
Element
of
NAT
: ( ( ) (
V134
()
V135
()
V136
()
V137
()
V138
()
V139
()
V140
() )
Element
of
K32
(
REAL
: ( ( ) (
V134
()
V135
()
V136
()
V140
() )
set
) ) : ( ( ) ( )
set
) ) )
-
r
: ( (
real
) (
V24
()
real
ext-real
)
number
)
)
: ( ( ) (
V24
()
real
ext-real
)
Element
of
REAL
: ( ( ) (
V134
()
V135
()
V136
()
V140
() )
set
) )
*
y
: ( ( ) ( )
Point
of ( ( ) ( non
empty
)
set
) )
)
: ( ( ) ( )
Element
of the
carrier
of
V
: ( ( ) ( )
RLTopStruct
) : ( ( ) ( )
set
) ) : ( ( ) ( )
Element
of the
carrier
of
V
: ( ( ) ( )
RLTopStruct
) : ( ( ) ( )
set
) )
in
B
: ( ( ) ( )
Element
of
V
: ( ( ) ( )
RLTopStruct
) ) ;
end;
theorem
:: MATHMORP:75
for
n
being ( ( ) (
natural
V24
()
real
ext-real
V86
()
V87
()
V134
()
V135
()
V136
()
V137
()
V138
()
V139
() )
Element
of
NAT
: ( ( ) (
V134
()
V135
()
V136
()
V137
()
V138
()
V139
()
V140
() )
Element
of
K32
(
REAL
: ( ( ) (
V134
()
V135
()
V136
()
V140
() )
set
) ) : ( ( ) ( )
set
) ) )
for
X
being ( ( ) ( )
Subset
of ) st
X
: ( ( ) ( )
Subset
of ) is
convex
holds
X
: ( ( ) ( )
Subset
of )
!
: ( ( ) ( )
Subset
of ) is
convex
;
theorem
:: MATHMORP:76
for
n
being ( ( ) (
natural
V24
()
real
ext-real
V86
()
V87
()
V134
()
V135
()
V136
()
V137
()
V138
()
V139
() )
Element
of
NAT
: ( ( ) (
V134
()
V135
()
V136
()
V137
()
V138
()
V139
()
V140
() )
Element
of
K32
(
REAL
: ( ( ) (
V134
()
V135
()
V136
()
V140
() )
set
) ) : ( ( ) ( )
set
) ) )
for
X
,
B
being ( ( ) ( )
Subset
of ) st
X
: ( ( ) ( )
Subset
of ) is
convex
&
B
: ( ( ) ( )
Subset
of ) is
convex
holds
(
X
: ( ( ) ( )
Subset
of )
(+)
B
: ( ( ) ( )
Subset
of ) : ( ( ) ( )
Element
of
K32
( the
carrier
of
(
TOP-REAL
b
1
: ( ( ) (
natural
V24
()
real
ext-real
V86
()
V87
()
V134
()
V135
()
V136
()
V137
()
V138
()
V139
() )
Element
of
NAT
: ( ( ) (
V134
()
V135
()
V136
()
V137
()
V138
()
V139
()
V140
() )
Element
of
K32
(
REAL
: ( ( ) (
V134
()
V135
()
V136
()
V140
() )
set
) ) : ( ( ) ( )
set
) ) )
)
: ( (
strict
) ( non
empty
TopSpace-like
left_complementable
right_complementable
Abelian
add-associative
right_zeroed
vector-distributive
scalar-distributive
scalar-associative
scalar-unital
V153
()
strict
)
RLTopStruct
) : ( ( ) ( non
empty
)
set
) ) : ( ( ) ( )
set
) ) is
convex
&
X
: ( ( ) ( )
Subset
of )
(-)
B
: ( ( ) ( )
Subset
of ) : ( ( ) ( )
Subset
of ) is
convex
) ;
theorem
:: MATHMORP:77
for
n
being ( ( ) (
natural
V24
()
real
ext-real
V86
()
V87
()
V134
()
V135
()
V136
()
V137
()
V138
()
V139
() )
Element
of
NAT
: ( ( ) (
V134
()
V135
()
V136
()
V137
()
V138
()
V139
()
V140
() )
Element
of
K32
(
REAL
: ( ( ) (
V134
()
V135
()
V136
()
V140
() )
set
) ) : ( ( ) ( )
set
) ) )
for
X
,
B
being ( ( ) ( )
Subset
of ) st
X
: ( ( ) ( )
Subset
of ) is
convex
&
B
: ( ( ) ( )
Subset
of ) is
convex
holds
(
X
: ( ( ) ( )
Subset
of )
(O)
B
: ( ( ) ( )
Subset
of ) : ( ( ) ( )
Subset
of ) is
convex
&
X
: ( ( ) ( )
Subset
of )
(o)
B
: ( ( ) ( )
Subset
of ) : ( ( ) ( )
Subset
of ) is
convex
) ;
theorem
:: MATHMORP:78
for
t
,
s
being ( (
real
) (
V24
()
real
ext-real
)
number
)
for
n
being ( ( ) (
natural
V24
()
real
ext-real
V86
()
V87
()
V134
()
V135
()
V136
()
V137
()
V138
()
V139
() )
Element
of
NAT
: ( ( ) (
V134
()
V135
()
V136
()
V137
()
V138
()
V139
()
V140
() )
Element
of
K32
(
REAL
: ( ( ) (
V134
()
V135
()
V136
()
V140
() )
set
) ) : ( ( ) ( )
set
) ) )
for
B
being ( ( ) ( )
Subset
of ) st
B
: ( ( ) ( )
Subset
of ) is
convex
&
0
: ( ( ) (
empty
natural
V24
()
real
ext-real
non
positive
non
negative
V86
()
V87
()
V134
()
V135
()
V136
()
V137
()
V138
()
V139
()
V140
() )
Element
of
NAT
: ( ( ) (
V134
()
V135
()
V136
()
V137
()
V138
()
V139
()
V140
() )
Element
of
K32
(
REAL
: ( ( ) (
V134
()
V135
()
V136
()
V140
() )
set
) ) : ( ( ) ( )
set
) ) )
<
t
: ( (
real
) (
V24
()
real
ext-real
)
number
) &
0
: ( ( ) (
empty
natural
V24
()
real
ext-real
non
positive
non
negative
V86
()
V87
()
V134
()
V135
()
V136
()
V137
()
V138
()
V139
()
V140
() )
Element
of
NAT
: ( ( ) (
V134
()
V135
()
V136
()
V137
()
V138
()
V139
()
V140
() )
Element
of
K32
(
REAL
: ( ( ) (
V134
()
V135
()
V136
()
V140
() )
set
) ) : ( ( ) ( )
set
) ) )
<
s
: ( (
real
) (
V24
()
real
ext-real
)
number
) holds
(
s
: ( (
real
) (
V24
()
real
ext-real
)
number
)
+
t
: ( (
real
) (
V24
()
real
ext-real
)
number
)
)
: ( ( ) (
V24
()
real
ext-real
)
set
)
(.)
B
: ( ( ) ( )
Subset
of ) : ( ( ) ( )
Subset
of )
=
(
s
: ( (
real
) (
V24
()
real
ext-real
)
number
)
(.)
B
: ( ( ) ( )
Subset
of )
)
: ( ( ) ( )
Subset
of )
(+)
(
t
: ( (
real
) (
V24
()
real
ext-real
)
number
)
(.)
B
: ( ( ) ( )
Subset
of )
)
: ( ( ) ( )
Subset
of ) : ( ( ) ( )
Element
of
K32
( the
carrier
of
(
TOP-REAL
b
3
: ( ( ) (
natural
V24
()
real
ext-real
V86
()
V87
()
V134
()
V135
()
V136
()
V137
()
V138
()
V139
() )
Element
of
NAT
: ( ( ) (
V134
()
V135
()
V136
()
V137
()
V138
()
V139
()
V140
() )
Element
of
K32
(
REAL
: ( ( ) (
V134
()
V135
()
V136
()
V140
() )
set
) ) : ( ( ) ( )
set
) ) )
)
: ( (
strict
) ( non
empty
TopSpace-like
left_complementable
right_complementable
Abelian
add-associative
right_zeroed
vector-distributive
scalar-distributive
scalar-associative
scalar-unital
V153
()
strict
)
RLTopStruct
) : ( ( ) ( non
empty
)
set
) ) : ( ( ) ( )
set
) ) ;