:: BCIALG_1 semantic presentation
begin
definition
attr
c
1
is
strict
;
struct
BCIStr
->
( ( ) ( )
1-sorted
) ;
aggr
BCIStr
(#
carrier
,
InternalDiff
#)
->
( (
strict
) (
strict
)
BCIStr
) ;
sel
InternalDiff
c
1
->
( (
V6
()
V18
(
[:
the
carrier
of
c
1
: ( ( ) ( )
2-sorted
) : ( ( ) ( )
set
) , the
carrier
of
c
1
: ( ( ) ( )
2-sorted
) : ( ( ) ( )
set
)
:]
: ( ( ) (
Relation-like
)
set
) , the
carrier
of
c
1
: ( ( ) ( )
2-sorted
) : ( ( ) ( )
set
) ) ) (
Relation-like
V6
()
V18
(
[:
the
carrier
of
c
1
: ( ( ) ( )
2-sorted
) : ( ( ) ( )
set
) , the
carrier
of
c
1
: ( ( ) ( )
2-sorted
) : ( ( ) ( )
set
)
:]
: ( ( ) (
Relation-like
)
set
) , the
carrier
of
c
1
: ( ( ) ( )
2-sorted
) : ( ( ) ( )
set
) ) )
BinOp
of the
carrier
of
c
1
: ( ( ) ( )
2-sorted
) : ( ( ) ( )
set
) ) ;
end;
registration
cluster
non
empty
strict
for ( ( ) ( )
BCIStr
) ;
end;
definition
let
A
be ( ( ) ( )
BCIStr
) ;
let
x
,
y
be ( ( ) ( )
Element
of ( ( ) ( )
set
) ) ;
func
x
\
y
->
( ( ) ( )
Element
of ( ( ) ( )
set
) )
equals
:: BCIALG_1:def 1
the
InternalDiff
of
A
: ( ( ) ( )
2-sorted
) : ( (
V6
()
V18
(
[:
the
carrier
of
A
: ( ( ) ( )
2-sorted
) : ( ( ) ( )
set
) , the
carrier
of
A
: ( ( ) ( )
2-sorted
) : ( ( ) ( )
set
)
:]
: ( ( ) (
Relation-like
)
set
) , the
carrier
of
A
: ( ( ) ( )
2-sorted
) : ( ( ) ( )
set
) ) ) (
Relation-like
V6
()
V18
(
[:
the
carrier
of
A
: ( ( ) ( )
2-sorted
) : ( ( ) ( )
set
) , the
carrier
of
A
: ( ( ) ( )
2-sorted
) : ( ( ) ( )
set
)
:]
: ( ( ) (
Relation-like
)
set
) , the
carrier
of
A
: ( ( ) ( )
2-sorted
) : ( ( ) ( )
set
) ) )
BinOp
of the
carrier
of
A
: ( ( ) ( )
2-sorted
) : ( ( ) ( )
set
) )
.
(
x
: ( ( ) ( )
set
) ,
y
: ( ( ) ( )
Element
of
A
: ( ( ) ( )
2-sorted
) ) ) : ( ( ) ( )
Element
of the
carrier
of
A
: ( ( ) ( )
2-sorted
) : ( ( ) ( )
set
) ) ;
end;
definition
attr
c
1
is
strict
;
struct
BCIStr_0
->
( ( ) ( )
BCIStr
) , ( ( ) ( )
ZeroStr
) ;
aggr
BCIStr_0
(#
carrier
,
InternalDiff
,
ZeroF
#)
->
( (
strict
) (
strict
)
BCIStr_0
) ;
end;
registration
cluster
non
empty
strict
for ( ( ) ( )
BCIStr_0
) ;
end;
definition
let
IT
be ( ( non
empty
) ( non
empty
)
BCIStr_0
) ;
let
x
be ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) ) ;
func
x
`
->
( ( ) ( )
Element
of ( ( ) ( )
set
) )
equals
:: BCIALG_1:def 2
(
0.
IT
: ( ( ) ( )
2-sorted
)
)
: ( ( ) ( )
Element
of the
carrier
of
IT
: ( ( ) ( )
2-sorted
) : ( ( ) ( )
set
) )
\
x
: ( ( ) ( )
set
) : ( ( ) ( )
Element
of ( ( ) ( )
set
) ) ;
end;
definition
let
IT
be ( ( non
empty
) ( non
empty
)
BCIStr_0
) ;
attr
IT
is
being_B
means
:: BCIALG_1:def 3
for
x
,
y
,
z
being ( ( ) ( )
Element
of ( ( ) ( )
set
) ) holds
(
(
x
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) )
\
y
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) )
)
: ( ( ) ( )
Element
of ( ( ) ( )
set
) )
\
(
z
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) )
\
y
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) )
)
: ( ( ) ( )
Element
of ( ( ) ( )
set
) )
)
: ( ( ) ( )
Element
of ( ( ) ( )
set
) )
\
(
x
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) )
\
z
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) )
)
: ( ( ) ( )
Element
of ( ( ) ( )
set
) ) : ( ( ) ( )
Element
of ( ( ) ( )
set
) )
=
0.
IT
: ( ( ) ( )
2-sorted
) : ( ( ) ( )
Element
of the
carrier
of
IT
: ( ( ) ( )
2-sorted
) : ( ( ) ( )
set
) ) ;
attr
IT
is
being_C
means
:: BCIALG_1:def 4
for
x
,
y
,
z
being ( ( ) ( )
Element
of ( ( ) ( )
set
) ) holds
(
(
x
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) )
\
y
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) )
)
: ( ( ) ( )
Element
of ( ( ) ( )
set
) )
\
z
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) )
)
: ( ( ) ( )
Element
of ( ( ) ( )
set
) )
\
(
(
x
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) )
\
z
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) )
)
: ( ( ) ( )
Element
of ( ( ) ( )
set
) )
\
y
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) )
)
: ( ( ) ( )
Element
of ( ( ) ( )
set
) ) : ( ( ) ( )
Element
of ( ( ) ( )
set
) )
=
0.
IT
: ( ( ) ( )
2-sorted
) : ( ( ) ( )
Element
of the
carrier
of
IT
: ( ( ) ( )
2-sorted
) : ( ( ) ( )
set
) ) ;
attr
IT
is
being_I
means
:: BCIALG_1:def 5
for
x
being ( ( ) ( )
Element
of ( ( ) ( )
set
) ) holds
x
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) )
\
x
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) ) : ( ( ) ( )
Element
of ( ( ) ( )
set
) )
=
0.
IT
: ( ( ) ( )
2-sorted
) : ( ( ) ( )
Element
of the
carrier
of
IT
: ( ( ) ( )
2-sorted
) : ( ( ) ( )
set
) ) ;
attr
IT
is
being_K
means
:: BCIALG_1:def 6
for
x
,
y
being ( ( ) ( )
Element
of ( ( ) ( )
set
) ) holds
(
x
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) )
\
y
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) )
)
: ( ( ) ( )
Element
of ( ( ) ( )
set
) )
\
x
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) ) : ( ( ) ( )
Element
of ( ( ) ( )
set
) )
=
0.
IT
: ( ( ) ( )
2-sorted
) : ( ( ) ( )
Element
of the
carrier
of
IT
: ( ( ) ( )
2-sorted
) : ( ( ) ( )
set
) ) ;
attr
IT
is
being_BCI-4
means
:: BCIALG_1:def 7
for
x
,
y
being ( ( ) ( )
Element
of ( ( ) ( )
set
) ) st
x
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) )
\
y
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) ) : ( ( ) ( )
Element
of ( ( ) ( )
set
) )
=
0.
IT
: ( ( ) ( )
2-sorted
) : ( ( ) ( )
Element
of the
carrier
of
IT
: ( ( ) ( )
2-sorted
) : ( ( ) ( )
set
) ) &
y
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) )
\
x
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) ) : ( ( ) ( )
Element
of ( ( ) ( )
set
) )
=
0.
IT
: ( ( ) ( )
2-sorted
) : ( ( ) ( )
Element
of the
carrier
of
IT
: ( ( ) ( )
2-sorted
) : ( ( ) ( )
set
) ) holds
x
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) )
=
y
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) ) ;
attr
IT
is
being_BCK-5
means
:: BCIALG_1:def 8
for
x
being ( ( ) ( )
Element
of ( ( ) ( )
set
) ) holds
x
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) )
`
: ( ( ) ( )
Element
of ( ( ) ( )
set
) )
=
0.
IT
: ( ( ) ( )
2-sorted
) : ( ( ) ( )
Element
of the
carrier
of
IT
: ( ( ) ( )
2-sorted
) : ( ( ) ( )
set
) ) ;
end;
definition
func
BCI-EXAMPLE
->
( ( ) ( )
BCIStr_0
)
equals
:: BCIALG_1:def 9
BCIStr_0
(# 1 : ( ( ) ( non
empty
)
set
) ,
op2
: ( (
V6
()
V18
(
[:
1 : ( ( ) ( non
empty
)
set
) ,1 : ( ( ) ( non
empty
)
set
)
:]
: ( ( ) (
Relation-like
)
set
) ,1 : ( ( ) ( non
empty
)
set
) ) ) (
Relation-like
V6
()
V18
(
[:
1 : ( ( ) ( non
empty
)
set
) ,1 : ( ( ) ( non
empty
)
set
)
:]
: ( ( ) (
Relation-like
)
set
) ,1 : ( ( ) ( non
empty
)
set
) ) )
Element
of
bool
[:
[:
1 : ( ( ) ( non
empty
)
set
) ,1 : ( ( ) ( non
empty
)
set
)
:]
: ( ( ) (
Relation-like
)
set
) ,1 : ( ( ) ( non
empty
)
set
)
:]
: ( ( ) (
Relation-like
)
set
) : ( ( ) ( )
set
) ) ,
op0
: ( ( ) ( )
Element
of 1 : ( ( ) ( non
empty
)
set
) ) #) : ( (
strict
) (
strict
)
BCIStr_0
) ;
end;
registration
cluster
BCI-EXAMPLE
: ( ( ) ( )
BCIStr_0
)
->
1 : ( ( ) ( non
empty
)
set
)
-element
strict
;
end;
registration
cluster
BCI-EXAMPLE
: ( ( ) ( non
empty
trivial
V46
() 1 : ( ( ) ( non
empty
)
set
)
-element
strict
)
BCIStr_0
)
->
being_B
being_C
being_I
being_BCI-4
being_BCK-5
;
end;
registration
cluster
non
empty
strict
being_B
being_C
being_I
being_BCI-4
being_BCK-5
for ( ( ) ( )
BCIStr_0
) ;
end;
definition
mode
BCI-algebra
is
( ( non
empty
being_B
being_C
being_I
being_BCI-4
) ( non
empty
being_B
being_C
being_I
being_BCI-4
)
BCIStr_0
) ;
end;
definition
mode
BCK-algebra
is
( ( non
empty
being_B
being_C
being_I
being_BCI-4
being_BCK-5
) ( non
empty
being_B
being_C
being_I
being_BCI-4
being_BCK-5
)
BCI-algebra
) ;
end;
definition
let
X
be ( ( non
empty
being_B
being_C
being_I
being_BCI-4
) ( non
empty
being_B
being_C
being_I
being_BCI-4
)
BCI-algebra
) ;
mode
SubAlgebra
of
X
->
( ( non
empty
being_B
being_C
being_I
being_BCI-4
) ( non
empty
being_B
being_C
being_I
being_BCI-4
)
BCI-algebra
)
means
:: BCIALG_1:def 10
(
0.
it
: ( ( ) ( )
set
) : ( ( ) ( )
Element
of the
carrier
of
it
: ( ( ) ( )
set
) : ( ( ) ( )
set
) )
=
0.
X
: ( ( non
empty
) ( non
empty
)
set
) : ( ( ) ( )
Element
of the
carrier
of
X
: ( ( non
empty
) ( non
empty
)
set
) : ( ( ) ( )
set
) ) & the
carrier
of
it
: ( ( ) ( )
set
) : ( ( ) ( )
set
)
c=
the
carrier
of
X
: ( ( non
empty
) ( non
empty
)
set
) : ( ( ) ( )
set
) & the
InternalDiff
of
it
: ( ( ) ( )
set
) : ( (
V6
()
V18
(
[:
the
carrier
of
it
: ( ( ) ( )
set
) : ( ( ) ( )
set
) , the
carrier
of
it
: ( ( ) ( )
set
) : ( ( ) ( )
set
)
:]
: ( ( ) (
Relation-like
)
set
) , the
carrier
of
it
: ( ( ) ( )
set
) : ( ( ) ( )
set
) ) ) (
Relation-like
V6
()
V18
(
[:
the
carrier
of
it
: ( ( ) ( )
set
) : ( ( ) ( )
set
) , the
carrier
of
it
: ( ( ) ( )
set
) : ( ( ) ( )
set
)
:]
: ( ( ) (
Relation-like
)
set
) , the
carrier
of
it
: ( ( ) ( )
set
) : ( ( ) ( )
set
) ) )
BinOp
of the
carrier
of
it
: ( ( ) ( )
set
) : ( ( ) ( )
set
) )
=
the
InternalDiff
of
X
: ( ( non
empty
) ( non
empty
)
set
) : ( (
V6
()
V18
(
[:
the
carrier
of
X
: ( ( non
empty
) ( non
empty
)
set
) : ( ( ) ( )
set
) , the
carrier
of
X
: ( ( non
empty
) ( non
empty
)
set
) : ( ( ) ( )
set
)
:]
: ( ( ) (
Relation-like
)
set
) , the
carrier
of
X
: ( ( non
empty
) ( non
empty
)
set
) : ( ( ) ( )
set
) ) ) (
Relation-like
V6
()
V18
(
[:
the
carrier
of
X
: ( ( non
empty
) ( non
empty
)
set
) : ( ( ) ( )
set
) , the
carrier
of
X
: ( ( non
empty
) ( non
empty
)
set
) : ( ( ) ( )
set
)
:]
: ( ( ) (
Relation-like
)
set
) , the
carrier
of
X
: ( ( non
empty
) ( non
empty
)
set
) : ( ( ) ( )
set
) ) )
BinOp
of the
carrier
of
X
: ( ( non
empty
) ( non
empty
)
set
) : ( ( ) ( )
set
) )
||
the
carrier
of
it
: ( ( ) ( )
set
) : ( ( ) ( )
set
) : ( ( ) ( )
set
) );
end;
theorem
:: BCIALG_1:1
for
X
being ( ( non
empty
) ( non
empty
)
BCIStr_0
) holds
(
X
: ( ( non
empty
) ( non
empty
)
BCIStr_0
) is ( ( non
empty
being_B
being_C
being_I
being_BCI-4
) ( non
empty
being_B
being_C
being_I
being_BCI-4
)
BCI-algebra
) iff (
X
: ( ( non
empty
) ( non
empty
)
BCIStr_0
) is
being_I
&
X
: ( ( non
empty
) ( non
empty
)
BCIStr_0
) is
being_BCI-4
& ( for
x
,
y
,
z
being ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) ) holds
(
(
(
x
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) )
\
y
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) )
)
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) )
\
(
x
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) )
\
z
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) )
)
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) )
)
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) )
\
(
z
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) )
\
y
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) )
)
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) ) : ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) )
=
0.
X
: ( ( non
empty
) ( non
empty
)
BCIStr_0
) : ( ( ) (
V47
(
b
1
: ( ( non
empty
) ( non
empty
)
BCIStr_0
) ) )
Element
of the
carrier
of
b
1
: ( ( non
empty
) ( non
empty
)
BCIStr_0
) : ( ( ) ( non
empty
)
set
) ) &
(
x
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) )
\
(
x
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) )
\
y
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) )
)
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) )
)
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) )
\
y
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) ) : ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) )
=
0.
X
: ( ( non
empty
) ( non
empty
)
BCIStr_0
) : ( ( ) (
V47
(
b
1
: ( ( non
empty
) ( non
empty
)
BCIStr_0
) ) )
Element
of the
carrier
of
b
1
: ( ( non
empty
) ( non
empty
)
BCIStr_0
) : ( ( ) ( non
empty
)
set
) ) ) ) ) ) ;
definition
let
IT
be ( ( non
empty
) ( non
empty
)
BCIStr_0
) ;
let
x
,
y
be ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) ) ;
pred
x
<=
y
means
:: BCIALG_1:def 11
x
: ( ( ) ( )
set
)
\
y
: ( ( ) ( )
Element
of
IT
: ( ( non
empty
) ( non
empty
)
set
) ) : ( ( ) ( )
Element
of ( ( ) ( )
set
) )
=
0.
IT
: ( ( non
empty
) ( non
empty
)
set
) : ( ( ) ( )
Element
of the
carrier
of
IT
: ( ( non
empty
) ( non
empty
)
set
) : ( ( ) ( )
set
) ) ;
end;
theorem
:: BCIALG_1:2
for
X
being ( ( non
empty
being_B
being_C
being_I
being_BCI-4
) ( non
empty
being_B
being_C
being_I
being_BCI-4
)
BCI-algebra
)
for
x
being ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) ) holds
x
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) )
\
(
0.
X
: ( ( non
empty
being_B
being_C
being_I
being_BCI-4
) ( non
empty
being_B
being_C
being_I
being_BCI-4
)
BCI-algebra
)
)
: ( ( ) (
V47
(
b
1
: ( ( non
empty
being_B
being_C
being_I
being_BCI-4
) ( non
empty
being_B
being_C
being_I
being_BCI-4
)
BCI-algebra
) ) )
Element
of the
carrier
of
b
1
: ( ( non
empty
being_B
being_C
being_I
being_BCI-4
) ( non
empty
being_B
being_C
being_I
being_BCI-4
)
BCI-algebra
) : ( ( ) ( non
empty
)
set
) ) : ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) )
=
x
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) ) ;
theorem
:: BCIALG_1:3
for
X
being ( ( non
empty
being_B
being_C
being_I
being_BCI-4
) ( non
empty
being_B
being_C
being_I
being_BCI-4
)
BCI-algebra
)
for
x
,
y
,
z
being ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) ) st
x
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) )
\
y
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) ) : ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) )
=
0.
X
: ( ( non
empty
being_B
being_C
being_I
being_BCI-4
) ( non
empty
being_B
being_C
being_I
being_BCI-4
)
BCI-algebra
) : ( ( ) (
V47
(
b
1
: ( ( non
empty
being_B
being_C
being_I
being_BCI-4
) ( non
empty
being_B
being_C
being_I
being_BCI-4
)
BCI-algebra
) ) )
Element
of the
carrier
of
b
1
: ( ( non
empty
being_B
being_C
being_I
being_BCI-4
) ( non
empty
being_B
being_C
being_I
being_BCI-4
)
BCI-algebra
) : ( ( ) ( non
empty
)
set
) ) &
y
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) )
\
z
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) ) : ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) )
=
0.
X
: ( ( non
empty
being_B
being_C
being_I
being_BCI-4
) ( non
empty
being_B
being_C
being_I
being_BCI-4
)
BCI-algebra
) : ( ( ) (
V47
(
b
1
: ( ( non
empty
being_B
being_C
being_I
being_BCI-4
) ( non
empty
being_B
being_C
being_I
being_BCI-4
)
BCI-algebra
) ) )
Element
of the
carrier
of
b
1
: ( ( non
empty
being_B
being_C
being_I
being_BCI-4
) ( non
empty
being_B
being_C
being_I
being_BCI-4
)
BCI-algebra
) : ( ( ) ( non
empty
)
set
) ) holds
x
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) )
\
z
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) ) : ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) )
=
0.
X
: ( ( non
empty
being_B
being_C
being_I
being_BCI-4
) ( non
empty
being_B
being_C
being_I
being_BCI-4
)
BCI-algebra
) : ( ( ) (
V47
(
b
1
: ( ( non
empty
being_B
being_C
being_I
being_BCI-4
) ( non
empty
being_B
being_C
being_I
being_BCI-4
)
BCI-algebra
) ) )
Element
of the
carrier
of
b
1
: ( ( non
empty
being_B
being_C
being_I
being_BCI-4
) ( non
empty
being_B
being_C
being_I
being_BCI-4
)
BCI-algebra
) : ( ( ) ( non
empty
)
set
) ) ;
theorem
:: BCIALG_1:4
for
X
being ( ( non
empty
being_B
being_C
being_I
being_BCI-4
) ( non
empty
being_B
being_C
being_I
being_BCI-4
)
BCI-algebra
)
for
x
,
y
,
z
being ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) ) st
x
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) )
\
y
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) ) : ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) )
=
0.
X
: ( ( non
empty
being_B
being_C
being_I
being_BCI-4
) ( non
empty
being_B
being_C
being_I
being_BCI-4
)
BCI-algebra
) : ( ( ) (
V47
(
b
1
: ( ( non
empty
being_B
being_C
being_I
being_BCI-4
) ( non
empty
being_B
being_C
being_I
being_BCI-4
)
BCI-algebra
) ) )
Element
of the
carrier
of
b
1
: ( ( non
empty
being_B
being_C
being_I
being_BCI-4
) ( non
empty
being_B
being_C
being_I
being_BCI-4
)
BCI-algebra
) : ( ( ) ( non
empty
)
set
) ) holds
(
(
x
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) )
\
z
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) )
)
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) )
\
(
y
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) )
\
z
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) )
)
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) ) : ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) )
=
0.
X
: ( ( non
empty
being_B
being_C
being_I
being_BCI-4
) ( non
empty
being_B
being_C
being_I
being_BCI-4
)
BCI-algebra
) : ( ( ) (
V47
(
b
1
: ( ( non
empty
being_B
being_C
being_I
being_BCI-4
) ( non
empty
being_B
being_C
being_I
being_BCI-4
)
BCI-algebra
) ) )
Element
of the
carrier
of
b
1
: ( ( non
empty
being_B
being_C
being_I
being_BCI-4
) ( non
empty
being_B
being_C
being_I
being_BCI-4
)
BCI-algebra
) : ( ( ) ( non
empty
)
set
) ) &
(
z
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) )
\
y
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) )
)
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) )
\
(
z
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) )
\
x
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) )
)
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) ) : ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) )
=
0.
X
: ( ( non
empty
being_B
being_C
being_I
being_BCI-4
) ( non
empty
being_B
being_C
being_I
being_BCI-4
)
BCI-algebra
) : ( ( ) (
V47
(
b
1
: ( ( non
empty
being_B
being_C
being_I
being_BCI-4
) ( non
empty
being_B
being_C
being_I
being_BCI-4
)
BCI-algebra
) ) )
Element
of the
carrier
of
b
1
: ( ( non
empty
being_B
being_C
being_I
being_BCI-4
) ( non
empty
being_B
being_C
being_I
being_BCI-4
)
BCI-algebra
) : ( ( ) ( non
empty
)
set
) ) ) ;
theorem
:: BCIALG_1:5
for
X
being ( ( non
empty
being_B
being_C
being_I
being_BCI-4
) ( non
empty
being_B
being_C
being_I
being_BCI-4
)
BCI-algebra
)
for
x
,
y
,
z
being ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) ) st
x
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) )
<=
y
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) ) holds
(
x
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) )
\
z
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) ) : ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) )
<=
y
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) )
\
z
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) ) : ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) ) &
z
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) )
\
y
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) ) : ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) )
<=
z
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) )
\
x
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) ) : ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) ) ) ;
theorem
:: BCIALG_1:6
for
X
being ( ( non
empty
being_B
being_C
being_I
being_BCI-4
) ( non
empty
being_B
being_C
being_I
being_BCI-4
)
BCI-algebra
)
for
x
,
y
being ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) ) st
x
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) )
\
y
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) ) : ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) )
=
0.
X
: ( ( non
empty
being_B
being_C
being_I
being_BCI-4
) ( non
empty
being_B
being_C
being_I
being_BCI-4
)
BCI-algebra
) : ( ( ) (
V47
(
b
1
: ( ( non
empty
being_B
being_C
being_I
being_BCI-4
) ( non
empty
being_B
being_C
being_I
being_BCI-4
)
BCI-algebra
) ) )
Element
of the
carrier
of
b
1
: ( ( non
empty
being_B
being_C
being_I
being_BCI-4
) ( non
empty
being_B
being_C
being_I
being_BCI-4
)
BCI-algebra
) : ( ( ) ( non
empty
)
set
) ) holds
(
y
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) )
\
x
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) )
)
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) )
`
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) )
=
0.
X
: ( ( non
empty
being_B
being_C
being_I
being_BCI-4
) ( non
empty
being_B
being_C
being_I
being_BCI-4
)
BCI-algebra
) : ( ( ) (
V47
(
b
1
: ( ( non
empty
being_B
being_C
being_I
being_BCI-4
) ( non
empty
being_B
being_C
being_I
being_BCI-4
)
BCI-algebra
) ) )
Element
of the
carrier
of
b
1
: ( ( non
empty
being_B
being_C
being_I
being_BCI-4
) ( non
empty
being_B
being_C
being_I
being_BCI-4
)
BCI-algebra
) : ( ( ) ( non
empty
)
set
) ) ;
theorem
:: BCIALG_1:7
for
X
being ( ( non
empty
being_B
being_C
being_I
being_BCI-4
) ( non
empty
being_B
being_C
being_I
being_BCI-4
)
BCI-algebra
)
for
x
,
y
,
z
being ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) ) holds
(
x
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) )
\
y
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) )
)
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) )
\
z
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) ) : ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) )
=
(
x
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) )
\
z
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) )
)
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) )
\
y
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) ) : ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) ) ;
theorem
:: BCIALG_1:8
for
X
being ( ( non
empty
being_B
being_C
being_I
being_BCI-4
) ( non
empty
being_B
being_C
being_I
being_BCI-4
)
BCI-algebra
)
for
x
,
y
being ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) ) holds
x
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) )
\
(
x
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) )
\
(
x
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) )
\
y
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) )
)
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) )
)
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) ) : ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) )
=
x
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) )
\
y
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) ) : ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) ) ;
theorem
:: BCIALG_1:9
for
X
being ( ( non
empty
being_B
being_C
being_I
being_BCI-4
) ( non
empty
being_B
being_C
being_I
being_BCI-4
)
BCI-algebra
)
for
x
,
y
being ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) ) holds
(
x
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) )
\
y
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) )
)
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) )
`
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) )
=
(
x
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) )
`
)
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) )
\
(
y
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) )
`
)
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) ) : ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) ) ;
theorem
:: BCIALG_1:10
for
X
being ( ( non
empty
being_B
being_C
being_I
being_BCI-4
) ( non
empty
being_B
being_C
being_I
being_BCI-4
)
BCI-algebra
)
for
x
,
y
being ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) ) holds
(
(
x
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) )
\
(
x
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) )
\
y
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) )
)
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) )
)
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) )
\
(
y
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) )
\
x
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) )
)
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) )
)
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) )
\
(
x
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) )
\
(
x
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) )
\
(
y
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) )
\
(
y
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) )
\
x
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) )
)
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) )
)
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) )
)
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) )
)
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) ) : ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) )
=
0.
X
: ( ( non
empty
being_B
being_C
being_I
being_BCI-4
) ( non
empty
being_B
being_C
being_I
being_BCI-4
)
BCI-algebra
) : ( ( ) (
V47
(
b
1
: ( ( non
empty
being_B
being_C
being_I
being_BCI-4
) ( non
empty
being_B
being_C
being_I
being_BCI-4
)
BCI-algebra
) ) )
Element
of the
carrier
of
b
1
: ( ( non
empty
being_B
being_C
being_I
being_BCI-4
) ( non
empty
being_B
being_C
being_I
being_BCI-4
)
BCI-algebra
) : ( ( ) ( non
empty
)
set
) ) ;
theorem
:: BCIALG_1:11
for
X
being ( ( non
empty
) ( non
empty
)
BCIStr_0
) holds
(
X
: ( ( non
empty
) ( non
empty
)
BCIStr_0
) is ( ( non
empty
being_B
being_C
being_I
being_BCI-4
) ( non
empty
being_B
being_C
being_I
being_BCI-4
)
BCI-algebra
) iff (
X
: ( ( non
empty
) ( non
empty
)
BCIStr_0
) is
being_BCI-4
& ( for
x
,
y
,
z
being ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) ) holds
(
(
(
x
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) )
\
y
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) )
)
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) )
\
(
x
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) )
\
z
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) )
)
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) )
)
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) )
\
(
z
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) )
\
y
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) )
)
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) ) : ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) )
=
0.
X
: ( ( non
empty
) ( non
empty
)
BCIStr_0
) : ( ( ) (
V47
(
b
1
: ( ( non
empty
) ( non
empty
)
BCIStr_0
) ) )
Element
of the
carrier
of
b
1
: ( ( non
empty
) ( non
empty
)
BCIStr_0
) : ( ( ) ( non
empty
)
set
) ) &
x
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) )
\
(
0.
X
: ( ( non
empty
) ( non
empty
)
BCIStr_0
)
)
: ( ( ) (
V47
(
b
1
: ( ( non
empty
) ( non
empty
)
BCIStr_0
) ) )
Element
of the
carrier
of
b
1
: ( ( non
empty
) ( non
empty
)
BCIStr_0
) : ( ( ) ( non
empty
)
set
) ) : ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) )
=
x
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) ) ) ) ) ) ;
theorem
:: BCIALG_1:12
for
X
being ( ( non
empty
being_B
being_C
being_I
being_BCI-4
) ( non
empty
being_B
being_C
being_I
being_BCI-4
)
BCI-algebra
) st ( for
X
being ( ( non
empty
being_B
being_C
being_I
being_BCI-4
) ( non
empty
being_B
being_C
being_I
being_BCI-4
)
BCI-algebra
)
for
x
,
y
being ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) ) holds
x
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) )
\
(
x
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) )
\
y
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) )
)
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) ) : ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) )
=
y
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) )
\
(
y
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) )
\
x
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) )
)
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) ) : ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) ) ) holds
X
: ( ( non
empty
being_B
being_C
being_I
being_BCI-4
) ( non
empty
being_B
being_C
being_I
being_BCI-4
)
BCI-algebra
) is ( ( non
empty
being_B
being_C
being_I
being_BCI-4
being_BCK-5
) ( non
empty
being_B
being_C
being_I
being_BCI-4
being_BCK-5
)
BCK-algebra
) ;
theorem
:: BCIALG_1:13
for
X
being ( ( non
empty
being_B
being_C
being_I
being_BCI-4
) ( non
empty
being_B
being_C
being_I
being_BCI-4
)
BCI-algebra
) st ( for
X
being ( ( non
empty
being_B
being_C
being_I
being_BCI-4
) ( non
empty
being_B
being_C
being_I
being_BCI-4
)
BCI-algebra
)
for
x
,
y
being ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) ) holds
(
x
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) )
\
y
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) )
)
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) )
\
y
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) ) : ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) )
=
x
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) )
\
y
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) ) : ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) ) ) holds
X
: ( ( non
empty
being_B
being_C
being_I
being_BCI-4
) ( non
empty
being_B
being_C
being_I
being_BCI-4
)
BCI-algebra
) is ( ( non
empty
being_B
being_C
being_I
being_BCI-4
being_BCK-5
) ( non
empty
being_B
being_C
being_I
being_BCI-4
being_BCK-5
)
BCK-algebra
) ;
theorem
:: BCIALG_1:14
for
X
being ( ( non
empty
being_B
being_C
being_I
being_BCI-4
) ( non
empty
being_B
being_C
being_I
being_BCI-4
)
BCI-algebra
) st ( for
X
being ( ( non
empty
being_B
being_C
being_I
being_BCI-4
) ( non
empty
being_B
being_C
being_I
being_BCI-4
)
BCI-algebra
)
for
x
,
y
being ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) ) holds
x
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) )
\
(
y
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) )
\
x
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) )
)
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) ) : ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) )
=
x
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) ) ) holds
X
: ( ( non
empty
being_B
being_C
being_I
being_BCI-4
) ( non
empty
being_B
being_C
being_I
being_BCI-4
)
BCI-algebra
) is ( ( non
empty
being_B
being_C
being_I
being_BCI-4
being_BCK-5
) ( non
empty
being_B
being_C
being_I
being_BCI-4
being_BCK-5
)
BCK-algebra
) ;
theorem
:: BCIALG_1:15
for
X
being ( ( non
empty
being_B
being_C
being_I
being_BCI-4
) ( non
empty
being_B
being_C
being_I
being_BCI-4
)
BCI-algebra
) st ( for
X
being ( ( non
empty
being_B
being_C
being_I
being_BCI-4
) ( non
empty
being_B
being_C
being_I
being_BCI-4
)
BCI-algebra
)
for
x
,
y
,
z
being ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) ) holds
(
x
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) )
\
y
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) )
)
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) )
\
y
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) ) : ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) )
=
(
x
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) )
\
z
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) )
)
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) )
\
(
y
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) )
\
z
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) )
)
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) ) : ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) ) ) holds
X
: ( ( non
empty
being_B
being_C
being_I
being_BCI-4
) ( non
empty
being_B
being_C
being_I
being_BCI-4
)
BCI-algebra
) is ( ( non
empty
being_B
being_C
being_I
being_BCI-4
being_BCK-5
) ( non
empty
being_B
being_C
being_I
being_BCI-4
being_BCK-5
)
BCK-algebra
) ;
theorem
:: BCIALG_1:16
for
X
being ( ( non
empty
being_B
being_C
being_I
being_BCI-4
) ( non
empty
being_B
being_C
being_I
being_BCI-4
)
BCI-algebra
) st ( for
X
being ( ( non
empty
being_B
being_C
being_I
being_BCI-4
) ( non
empty
being_B
being_C
being_I
being_BCI-4
)
BCI-algebra
)
for
x
,
y
being ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) ) holds
(
x
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) )
\
y
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) )
)
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) )
\
(
y
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) )
\
x
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) )
)
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) ) : ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) )
=
x
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) )
\
y
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) ) : ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) ) ) holds
X
: ( ( non
empty
being_B
being_C
being_I
being_BCI-4
) ( non
empty
being_B
being_C
being_I
being_BCI-4
)
BCI-algebra
) is ( ( non
empty
being_B
being_C
being_I
being_BCI-4
being_BCK-5
) ( non
empty
being_B
being_C
being_I
being_BCI-4
being_BCK-5
)
BCK-algebra
) ;
theorem
:: BCIALG_1:17
for
X
being ( ( non
empty
being_B
being_C
being_I
being_BCI-4
) ( non
empty
being_B
being_C
being_I
being_BCI-4
)
BCI-algebra
) st ( for
X
being ( ( non
empty
being_B
being_C
being_I
being_BCI-4
) ( non
empty
being_B
being_C
being_I
being_BCI-4
)
BCI-algebra
)
for
x
,
y
being ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) ) holds
(
x
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) )
\
y
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) )
)
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) )
\
(
(
x
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) )
\
y
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) )
)
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) )
\
(
y
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) )
\
x
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) )
)
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) )
)
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) ) : ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) )
=
0.
X
: ( ( non
empty
being_B
being_C
being_I
being_BCI-4
) ( non
empty
being_B
being_C
being_I
being_BCI-4
)
BCI-algebra
) : ( ( ) (
V47
(
b
2
: ( ( non
empty
being_B
being_C
being_I
being_BCI-4
) ( non
empty
being_B
being_C
being_I
being_BCI-4
)
BCI-algebra
) ) )
Element
of the
carrier
of
b
2
: ( ( non
empty
being_B
being_C
being_I
being_BCI-4
) ( non
empty
being_B
being_C
being_I
being_BCI-4
)
BCI-algebra
) : ( ( ) ( non
empty
)
set
) ) ) holds
X
: ( ( non
empty
being_B
being_C
being_I
being_BCI-4
) ( non
empty
being_B
being_C
being_I
being_BCI-4
)
BCI-algebra
) is ( ( non
empty
being_B
being_C
being_I
being_BCI-4
being_BCK-5
) ( non
empty
being_B
being_C
being_I
being_BCI-4
being_BCK-5
)
BCK-algebra
) ;
theorem
:: BCIALG_1:18
for
X
being ( ( non
empty
being_B
being_C
being_I
being_BCI-4
) ( non
empty
being_B
being_C
being_I
being_BCI-4
)
BCI-algebra
) holds
(
X
: ( ( non
empty
being_B
being_C
being_I
being_BCI-4
) ( non
empty
being_B
being_C
being_I
being_BCI-4
)
BCI-algebra
) is
being_K
iff
X
: ( ( non
empty
being_B
being_C
being_I
being_BCI-4
) ( non
empty
being_B
being_C
being_I
being_BCI-4
)
BCI-algebra
) is ( ( non
empty
being_B
being_C
being_I
being_BCI-4
being_BCK-5
) ( non
empty
being_B
being_C
being_I
being_BCI-4
being_BCK-5
)
BCK-algebra
) ) ;
definition
let
X
be ( ( non
empty
being_B
being_C
being_I
being_BCI-4
) ( non
empty
being_B
being_C
being_I
being_BCI-4
)
BCI-algebra
) ;
func
BCK-part
X
->
( ( non
empty
) ( non
empty
)
Subset
of )
equals
:: BCIALG_1:def 12
{
x
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) ) where
x
is ( ( ) ( )
Element
of ( ( ) ( )
set
) ) :
0.
X
: ( ( non
empty
) ( non
empty
)
set
) : ( ( ) ( )
Element
of the
carrier
of
X
: ( ( non
empty
) ( non
empty
)
set
) : ( ( ) ( )
set
) )
<=
x
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) )
}
;
end;
theorem
:: BCIALG_1:19
for
X
being ( ( non
empty
being_B
being_C
being_I
being_BCI-4
) ( non
empty
being_B
being_C
being_I
being_BCI-4
)
BCI-algebra
) holds
0.
X
: ( ( non
empty
being_B
being_C
being_I
being_BCI-4
) ( non
empty
being_B
being_C
being_I
being_BCI-4
)
BCI-algebra
) : ( ( ) (
V47
(
b
1
: ( ( non
empty
being_B
being_C
being_I
being_BCI-4
) ( non
empty
being_B
being_C
being_I
being_BCI-4
)
BCI-algebra
) ) )
Element
of the
carrier
of
b
1
: ( ( non
empty
being_B
being_C
being_I
being_BCI-4
) ( non
empty
being_B
being_C
being_I
being_BCI-4
)
BCI-algebra
) : ( ( ) ( non
empty
)
set
) )
in
BCK-part
X
: ( ( non
empty
being_B
being_C
being_I
being_BCI-4
) ( non
empty
being_B
being_C
being_I
being_BCI-4
)
BCI-algebra
) : ( ( non
empty
) ( non
empty
)
Subset
of ) ;
theorem
:: BCIALG_1:20
for
X
being ( ( non
empty
being_B
being_C
being_I
being_BCI-4
) ( non
empty
being_B
being_C
being_I
being_BCI-4
)
BCI-algebra
)
for
x
,
y
being ( ( ) ( )
Element
of
BCK-part
X
: ( ( non
empty
being_B
being_C
being_I
being_BCI-4
) ( non
empty
being_B
being_C
being_I
being_BCI-4
)
BCI-algebra
) : ( ( non
empty
) ( non
empty
)
Subset
of ) ) holds
x
: ( ( ) ( )
Element
of
BCK-part
b
1
: ( ( non
empty
being_B
being_C
being_I
being_BCI-4
) ( non
empty
being_B
being_C
being_I
being_BCI-4
)
BCI-algebra
) : ( ( non
empty
) ( non
empty
)
Subset
of ) )
\
y
: ( ( ) ( )
Element
of
BCK-part
b
1
: ( ( non
empty
being_B
being_C
being_I
being_BCI-4
) ( non
empty
being_B
being_C
being_I
being_BCI-4
)
BCI-algebra
) : ( ( non
empty
) ( non
empty
)
Subset
of ) ) : ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) )
in
BCK-part
X
: ( ( non
empty
being_B
being_C
being_I
being_BCI-4
) ( non
empty
being_B
being_C
being_I
being_BCI-4
)
BCI-algebra
) : ( ( non
empty
) ( non
empty
)
Subset
of ) ;
theorem
:: BCIALG_1:21
for
X
being ( ( non
empty
being_B
being_C
being_I
being_BCI-4
) ( non
empty
being_B
being_C
being_I
being_BCI-4
)
BCI-algebra
)
for
x
being ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) )
for
y
being ( ( ) ( )
Element
of
BCK-part
X
: ( ( non
empty
being_B
being_C
being_I
being_BCI-4
) ( non
empty
being_B
being_C
being_I
being_BCI-4
)
BCI-algebra
) : ( ( non
empty
) ( non
empty
)
Subset
of ) ) holds
x
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) )
\
y
: ( ( ) ( )
Element
of
BCK-part
b
1
: ( ( non
empty
being_B
being_C
being_I
being_BCI-4
) ( non
empty
being_B
being_C
being_I
being_BCI-4
)
BCI-algebra
) : ( ( non
empty
) ( non
empty
)
Subset
of ) ) : ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) )
<=
x
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) ) ;
theorem
:: BCIALG_1:22
for
X
being ( ( non
empty
being_B
being_C
being_I
being_BCI-4
) ( non
empty
being_B
being_C
being_I
being_BCI-4
)
BCI-algebra
) holds
X
: ( ( non
empty
being_B
being_C
being_I
being_BCI-4
) ( non
empty
being_B
being_C
being_I
being_BCI-4
)
BCI-algebra
) is ( ( ) ( non
empty
being_B
being_C
being_I
being_BCI-4
)
SubAlgebra
of
X
: ( ( non
empty
being_B
being_C
being_I
being_BCI-4
) ( non
empty
being_B
being_C
being_I
being_BCI-4
)
BCI-algebra
) ) ;
definition
let
X
be ( ( non
empty
being_B
being_C
being_I
being_BCI-4
) ( non
empty
being_B
being_C
being_I
being_BCI-4
)
BCI-algebra
) ;
let
IT
be ( ( ) ( non
empty
being_B
being_C
being_I
being_BCI-4
)
SubAlgebra
of
X
: ( ( non
empty
being_B
being_C
being_I
being_BCI-4
) ( non
empty
being_B
being_C
being_I
being_BCI-4
)
BCI-algebra
) ) ;
attr
IT
is
proper
means
:: BCIALG_1:def 13
IT
: ( ( ) ( )
set
)
<>
X
: ( ( non
empty
) ( non
empty
)
set
) ;
end;
registration
let
X
be ( ( non
empty
being_B
being_C
being_I
being_BCI-4
) ( non
empty
being_B
being_C
being_I
being_BCI-4
)
BCI-algebra
) ;
cluster
non
empty
being_B
being_C
being_I
being_BCI-4
non
proper
for ( ( ) ( )
SubAlgebra
of
X
: ( ( non
empty
being_B
being_C
being_I
being_BCI-4
) ( non
empty
being_B
being_C
being_I
being_BCI-4
)
BCIStr_0
) ) ;
end;
definition
let
X
be ( ( non
empty
being_B
being_C
being_I
being_BCI-4
) ( non
empty
being_B
being_C
being_I
being_BCI-4
)
BCI-algebra
) ;
let
IT
be ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) ) ;
attr
IT
is
atom
means
:: BCIALG_1:def 14
for
z
being ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) ) st
z
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) )
\
IT
: ( ( ) ( )
set
) : ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) )
=
0.
X
: ( ( non
empty
being_B
being_C
being_I
being_BCI-4
) ( non
empty
being_B
being_C
being_I
being_BCI-4
)
BCIStr_0
) : ( ( ) (
V47
(
X
: ( ( non
empty
being_B
being_C
being_I
being_BCI-4
) ( non
empty
being_B
being_C
being_I
being_BCI-4
)
BCIStr_0
) ) )
Element
of the
carrier
of
X
: ( ( non
empty
being_B
being_C
being_I
being_BCI-4
) ( non
empty
being_B
being_C
being_I
being_BCI-4
)
BCIStr_0
) : ( ( ) ( non
empty
)
set
) ) holds
z
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) )
=
IT
: ( ( ) ( )
set
) ;
end;
definition
let
X
be ( ( non
empty
being_B
being_C
being_I
being_BCI-4
) ( non
empty
being_B
being_C
being_I
being_BCI-4
)
BCI-algebra
) ;
func
AtomSet
X
->
( ( non
empty
) ( non
empty
)
Subset
of )
equals
:: BCIALG_1:def 15
{
x
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) ) where
x
is ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) ) :
x
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) ) is
atom
}
;
end;
theorem
:: BCIALG_1:23
for
X
being ( ( non
empty
being_B
being_C
being_I
being_BCI-4
) ( non
empty
being_B
being_C
being_I
being_BCI-4
)
BCI-algebra
) holds
0.
X
: ( ( non
empty
being_B
being_C
being_I
being_BCI-4
) ( non
empty
being_B
being_C
being_I
being_BCI-4
)
BCI-algebra
) : ( ( ) (
V47
(
b
1
: ( ( non
empty
being_B
being_C
being_I
being_BCI-4
) ( non
empty
being_B
being_C
being_I
being_BCI-4
)
BCI-algebra
) ) )
Element
of the
carrier
of
b
1
: ( ( non
empty
being_B
being_C
being_I
being_BCI-4
) ( non
empty
being_B
being_C
being_I
being_BCI-4
)
BCI-algebra
) : ( ( ) ( non
empty
)
set
) )
in
AtomSet
X
: ( ( non
empty
being_B
being_C
being_I
being_BCI-4
) ( non
empty
being_B
being_C
being_I
being_BCI-4
)
BCI-algebra
) : ( ( non
empty
) ( non
empty
)
Subset
of ) ;
theorem
:: BCIALG_1:24
for
X
being ( ( non
empty
being_B
being_C
being_I
being_BCI-4
) ( non
empty
being_B
being_C
being_I
being_BCI-4
)
BCI-algebra
)
for
x
being ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) ) holds
(
x
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) )
in
AtomSet
X
: ( ( non
empty
being_B
being_C
being_I
being_BCI-4
) ( non
empty
being_B
being_C
being_I
being_BCI-4
)
BCI-algebra
) : ( ( non
empty
) ( non
empty
)
Subset
of ) iff for
z
being ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) ) holds
z
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) )
\
(
z
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) )
\
x
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) )
)
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) ) : ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) )
=
x
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) ) ) ;
theorem
:: BCIALG_1:25
for
X
being ( ( non
empty
being_B
being_C
being_I
being_BCI-4
) ( non
empty
being_B
being_C
being_I
being_BCI-4
)
BCI-algebra
)
for
x
being ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) ) holds
(
x
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) )
in
AtomSet
X
: ( ( non
empty
being_B
being_C
being_I
being_BCI-4
) ( non
empty
being_B
being_C
being_I
being_BCI-4
)
BCI-algebra
) : ( ( non
empty
) ( non
empty
)
Subset
of ) iff for
u
,
z
being ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) ) holds
(
z
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) )
\
u
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) )
)
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) )
\
(
z
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) )
\
x
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) )
)
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) ) : ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) )
=
x
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) )
\
u
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) ) : ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) ) ) ;
theorem
:: BCIALG_1:26
for
X
being ( ( non
empty
being_B
being_C
being_I
being_BCI-4
) ( non
empty
being_B
being_C
being_I
being_BCI-4
)
BCI-algebra
)
for
x
being ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) ) holds
(
x
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) )
in
AtomSet
X
: ( ( non
empty
being_B
being_C
being_I
being_BCI-4
) ( non
empty
being_B
being_C
being_I
being_BCI-4
)
BCI-algebra
) : ( ( non
empty
) ( non
empty
)
Subset
of ) iff for
y
,
z
being ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) ) holds
x
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) )
\
(
z
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) )
\
y
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) )
)
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) ) : ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) )
<=
y
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) )
\
(
z
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) )
\
x
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) )
)
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) ) : ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) ) ) ;
theorem
:: BCIALG_1:27
for
X
being ( ( non
empty
being_B
being_C
being_I
being_BCI-4
) ( non
empty
being_B
being_C
being_I
being_BCI-4
)
BCI-algebra
)
for
x
being ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) ) holds
(
x
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) )
in
AtomSet
X
: ( ( non
empty
being_B
being_C
being_I
being_BCI-4
) ( non
empty
being_B
being_C
being_I
being_BCI-4
)
BCI-algebra
) : ( ( non
empty
) ( non
empty
)
Subset
of ) iff for
y
,
z
,
u
being ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) ) holds
(
x
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) )
\
u
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) )
)
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) )
\
(
z
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) )
\
y
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) )
)
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) ) : ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) )
<=
(
y
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) )
\
u
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) )
)
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) )
\
(
z
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) )
\
x
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) )
)
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) ) : ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) ) ) ;
theorem
:: BCIALG_1:28
for
X
being ( ( non
empty
being_B
being_C
being_I
being_BCI-4
) ( non
empty
being_B
being_C
being_I
being_BCI-4
)
BCI-algebra
)
for
x
being ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) ) holds
(
x
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) )
in
AtomSet
X
: ( ( non
empty
being_B
being_C
being_I
being_BCI-4
) ( non
empty
being_B
being_C
being_I
being_BCI-4
)
BCI-algebra
) : ( ( non
empty
) ( non
empty
)
Subset
of ) iff for
z
being ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) ) holds
(
z
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) )
`
)
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) )
\
(
x
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) )
`
)
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) ) : ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) )
=
x
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) )
\
z
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) ) : ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) ) ) ;
theorem
:: BCIALG_1:29
for
X
being ( ( non
empty
being_B
being_C
being_I
being_BCI-4
) ( non
empty
being_B
being_C
being_I
being_BCI-4
)
BCI-algebra
)
for
x
being ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) ) holds
(
x
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) )
in
AtomSet
X
: ( ( non
empty
being_B
being_C
being_I
being_BCI-4
) ( non
empty
being_B
being_C
being_I
being_BCI-4
)
BCI-algebra
) : ( ( non
empty
) ( non
empty
)
Subset
of ) iff
(
x
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) )
`
)
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) )
`
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) )
=
x
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) ) ) ;
theorem
:: BCIALG_1:30
for
X
being ( ( non
empty
being_B
being_C
being_I
being_BCI-4
) ( non
empty
being_B
being_C
being_I
being_BCI-4
)
BCI-algebra
)
for
x
being ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) ) holds
(
x
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) )
in
AtomSet
X
: ( ( non
empty
being_B
being_C
being_I
being_BCI-4
) ( non
empty
being_B
being_C
being_I
being_BCI-4
)
BCI-algebra
) : ( ( non
empty
) ( non
empty
)
Subset
of ) iff for
z
being ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) ) holds
(
z
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) )
\
x
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) )
)
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) )
`
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) )
=
x
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) )
\
z
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) ) : ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) ) ) ;
theorem
:: BCIALG_1:31
for
X
being ( ( non
empty
being_B
being_C
being_I
being_BCI-4
) ( non
empty
being_B
being_C
being_I
being_BCI-4
)
BCI-algebra
)
for
x
being ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) ) holds
(
x
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) )
in
AtomSet
X
: ( ( non
empty
being_B
being_C
being_I
being_BCI-4
) ( non
empty
being_B
being_C
being_I
being_BCI-4
)
BCI-algebra
) : ( ( non
empty
) ( non
empty
)
Subset
of ) iff for
z
being ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) ) holds
(
(
x
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) )
\
z
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) )
)
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) )
`
)
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) )
`
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) )
=
x
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) )
\
z
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) ) : ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) ) ) ;
theorem
:: BCIALG_1:32
for
X
being ( ( non
empty
being_B
being_C
being_I
being_BCI-4
) ( non
empty
being_B
being_C
being_I
being_BCI-4
)
BCI-algebra
)
for
x
being ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) ) holds
(
x
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) )
in
AtomSet
X
: ( ( non
empty
being_B
being_C
being_I
being_BCI-4
) ( non
empty
being_B
being_C
being_I
being_BCI-4
)
BCI-algebra
) : ( ( non
empty
) ( non
empty
)
Subset
of ) iff for
z
,
u
being ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) ) holds
z
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) )
\
(
z
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) )
\
(
x
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) )
\
u
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) )
)
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) )
)
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) ) : ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) )
=
x
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) )
\
u
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) ) : ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) ) ) ;
theorem
:: BCIALG_1:33
for
X
being ( ( non
empty
being_B
being_C
being_I
being_BCI-4
) ( non
empty
being_B
being_C
being_I
being_BCI-4
)
BCI-algebra
)
for
a
being ( ( ) ( )
Element
of
AtomSet
X
: ( ( non
empty
being_B
being_C
being_I
being_BCI-4
) ( non
empty
being_B
being_C
being_I
being_BCI-4
)
BCI-algebra
) : ( ( non
empty
) ( non
empty
)
Subset
of ) )
for
x
being ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) ) holds
a
: ( ( ) ( )
Element
of
AtomSet
b
1
: ( ( non
empty
being_B
being_C
being_I
being_BCI-4
) ( non
empty
being_B
being_C
being_I
being_BCI-4
)
BCI-algebra
) : ( ( non
empty
) ( non
empty
)
Subset
of ) )
\
x
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) ) : ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) )
in
AtomSet
X
: ( ( non
empty
being_B
being_C
being_I
being_BCI-4
) ( non
empty
being_B
being_C
being_I
being_BCI-4
)
BCI-algebra
) : ( ( non
empty
) ( non
empty
)
Subset
of ) ;
definition
let
X
be ( ( non
empty
being_B
being_C
being_I
being_BCI-4
) ( non
empty
being_B
being_C
being_I
being_BCI-4
)
BCI-algebra
) ;
let
a
,
b
be ( ( ) ( )
Element
of
AtomSet
X
: ( ( non
empty
being_B
being_C
being_I
being_BCI-4
) ( non
empty
being_B
being_C
being_I
being_BCI-4
)
BCI-algebra
) : ( ( non
empty
) ( non
empty
)
Subset
of ) ) ;
:: original:
\
redefine
func
a
\
b
->
( ( ) ( )
Element
of
AtomSet
X
: ( ( non
empty
being_B
being_C
being_I
being_BCI-4
) ( non
empty
being_B
being_C
being_I
being_BCI-4
)
BCIStr_0
) : ( ( non
empty
) ( non
empty
)
Subset
of ) ) ;
end;
theorem
:: BCIALG_1:34
for
X
being ( ( non
empty
being_B
being_C
being_I
being_BCI-4
) ( non
empty
being_B
being_C
being_I
being_BCI-4
)
BCI-algebra
)
for
x
being ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) ) holds
x
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) )
`
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) )
in
AtomSet
X
: ( ( non
empty
being_B
being_C
being_I
being_BCI-4
) ( non
empty
being_B
being_C
being_I
being_BCI-4
)
BCI-algebra
) : ( ( non
empty
) ( non
empty
)
Subset
of ) ;
theorem
:: BCIALG_1:35
for
X
being ( ( non
empty
being_B
being_C
being_I
being_BCI-4
) ( non
empty
being_B
being_C
being_I
being_BCI-4
)
BCI-algebra
)
for
x
being ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) ) ex
a
being ( ( ) ( )
Element
of
AtomSet
X
: ( ( non
empty
being_B
being_C
being_I
being_BCI-4
) ( non
empty
being_B
being_C
being_I
being_BCI-4
)
BCI-algebra
) : ( ( non
empty
) ( non
empty
)
Subset
of ) ) st
a
: ( ( ) ( )
Element
of
AtomSet
b
1
: ( ( non
empty
being_B
being_C
being_I
being_BCI-4
) ( non
empty
being_B
being_C
being_I
being_BCI-4
)
BCI-algebra
) : ( ( non
empty
) ( non
empty
)
Subset
of ) )
<=
x
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) ) ;
definition
let
X
be ( ( non
empty
being_B
being_C
being_I
being_BCI-4
) ( non
empty
being_B
being_C
being_I
being_BCI-4
)
BCI-algebra
) ;
attr
X
is
generated_by_atom
means
:: BCIALG_1:def 16
for
x
being ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) ) ex
a
being ( ( ) ( )
Element
of
AtomSet
X
: ( ( non
empty
being_B
being_C
being_I
being_BCI-4
) ( non
empty
being_B
being_C
being_I
being_BCI-4
)
BCIStr_0
) : ( ( non
empty
) ( non
empty
)
Subset
of ) ) st
a
: ( ( ) ( )
Element
of
AtomSet
X
: ( ( non
empty
being_B
being_C
being_I
being_BCI-4
) ( non
empty
being_B
being_C
being_I
being_BCI-4
)
BCI-algebra
) : ( ( non
empty
) ( non
empty
)
Subset
of ) )
<=
x
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) ) ;
end;
definition
let
X
be ( ( non
empty
being_B
being_C
being_I
being_BCI-4
) ( non
empty
being_B
being_C
being_I
being_BCI-4
)
BCI-algebra
) ;
let
a
be ( ( ) ( )
Element
of
AtomSet
X
: ( ( non
empty
being_B
being_C
being_I
being_BCI-4
) ( non
empty
being_B
being_C
being_I
being_BCI-4
)
BCI-algebra
) : ( ( non
empty
) ( non
empty
)
Subset
of ) ) ;
func
BranchV
a
->
( ( non
empty
) ( non
empty
)
Subset
of )
equals
:: BCIALG_1:def 17
{
x
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) ) where
x
is ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) ) :
a
: ( ( ) ( )
set
)
<=
x
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) )
}
;
end;
theorem
:: BCIALG_1:36
for
X
being ( ( non
empty
being_B
being_C
being_I
being_BCI-4
) ( non
empty
being_B
being_C
being_I
being_BCI-4
)
BCI-algebra
) holds
X
: ( ( non
empty
being_B
being_C
being_I
being_BCI-4
) ( non
empty
being_B
being_C
being_I
being_BCI-4
)
BCI-algebra
) is
generated_by_atom
;
theorem
:: BCIALG_1:37
for
X
being ( ( non
empty
being_B
being_C
being_I
being_BCI-4
) ( non
empty
being_B
being_C
being_I
being_BCI-4
)
BCI-algebra
)
for
a
,
b
being ( ( ) ( )
Element
of
AtomSet
X
: ( ( non
empty
being_B
being_C
being_I
being_BCI-4
) ( non
empty
being_B
being_C
being_I
being_BCI-4
)
BCI-algebra
) : ( ( non
empty
) ( non
empty
)
Subset
of ) )
for
x
being ( ( ) ( )
Element
of
BranchV
b
: ( ( ) ( )
Element
of
AtomSet
b
1
: ( ( non
empty
being_B
being_C
being_I
being_BCI-4
) ( non
empty
being_B
being_C
being_I
being_BCI-4
)
BCI-algebra
) : ( ( non
empty
) ( non
empty
)
Subset
of ) ) : ( ( non
empty
) ( non
empty
)
Subset
of ) ) holds
a
: ( ( ) ( )
Element
of
AtomSet
b
1
: ( ( non
empty
being_B
being_C
being_I
being_BCI-4
) ( non
empty
being_B
being_C
being_I
being_BCI-4
)
BCI-algebra
) : ( ( non
empty
) ( non
empty
)
Subset
of ) )
\
x
: ( ( ) ( )
Element
of
BranchV
b
3
: ( ( ) ( )
Element
of
AtomSet
b
1
: ( ( non
empty
being_B
being_C
being_I
being_BCI-4
) ( non
empty
being_B
being_C
being_I
being_BCI-4
)
BCI-algebra
) : ( ( non
empty
) ( non
empty
)
Subset
of ) ) : ( ( non
empty
) ( non
empty
)
Subset
of ) ) : ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) )
=
a
: ( ( ) ( )
Element
of
AtomSet
b
1
: ( ( non
empty
being_B
being_C
being_I
being_BCI-4
) ( non
empty
being_B
being_C
being_I
being_BCI-4
)
BCI-algebra
) : ( ( non
empty
) ( non
empty
)
Subset
of ) )
\
b
: ( ( ) ( )
Element
of
AtomSet
b
1
: ( ( non
empty
being_B
being_C
being_I
being_BCI-4
) ( non
empty
being_B
being_C
being_I
being_BCI-4
)
BCI-algebra
) : ( ( non
empty
) ( non
empty
)
Subset
of ) ) : ( ( ) ( )
Element
of
AtomSet
b
1
: ( ( non
empty
being_B
being_C
being_I
being_BCI-4
) ( non
empty
being_B
being_C
being_I
being_BCI-4
)
BCI-algebra
) : ( ( non
empty
) ( non
empty
)
Subset
of ) ) ;
theorem
:: BCIALG_1:38
for
X
being ( ( non
empty
being_B
being_C
being_I
being_BCI-4
) ( non
empty
being_B
being_C
being_I
being_BCI-4
)
BCI-algebra
)
for
a
being ( ( ) ( )
Element
of
AtomSet
X
: ( ( non
empty
being_B
being_C
being_I
being_BCI-4
) ( non
empty
being_B
being_C
being_I
being_BCI-4
)
BCI-algebra
) : ( ( non
empty
) ( non
empty
)
Subset
of ) )
for
x
being ( ( ) ( )
Element
of
BCK-part
X
: ( ( non
empty
being_B
being_C
being_I
being_BCI-4
) ( non
empty
being_B
being_C
being_I
being_BCI-4
)
BCI-algebra
) : ( ( non
empty
) ( non
empty
)
Subset
of ) ) holds
a
: ( ( ) ( )
Element
of
AtomSet
b
1
: ( ( non
empty
being_B
being_C
being_I
being_BCI-4
) ( non
empty
being_B
being_C
being_I
being_BCI-4
)
BCI-algebra
) : ( ( non
empty
) ( non
empty
)
Subset
of ) )
\
x
: ( ( ) ( )
Element
of
BCK-part
b
1
: ( ( non
empty
being_B
being_C
being_I
being_BCI-4
) ( non
empty
being_B
being_C
being_I
being_BCI-4
)
BCI-algebra
) : ( ( non
empty
) ( non
empty
)
Subset
of ) ) : ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) )
=
a
: ( ( ) ( )
Element
of
AtomSet
b
1
: ( ( non
empty
being_B
being_C
being_I
being_BCI-4
) ( non
empty
being_B
being_C
being_I
being_BCI-4
)
BCI-algebra
) : ( ( non
empty
) ( non
empty
)
Subset
of ) ) ;
theorem
:: BCIALG_1:39
for
X
being ( ( non
empty
being_B
being_C
being_I
being_BCI-4
) ( non
empty
being_B
being_C
being_I
being_BCI-4
)
BCI-algebra
)
for
a
,
b
being ( ( ) ( )
Element
of
AtomSet
X
: ( ( non
empty
being_B
being_C
being_I
being_BCI-4
) ( non
empty
being_B
being_C
being_I
being_BCI-4
)
BCI-algebra
) : ( ( non
empty
) ( non
empty
)
Subset
of ) )
for
x
being ( ( ) ( )
Element
of
BranchV
a
: ( ( ) ( )
Element
of
AtomSet
b
1
: ( ( non
empty
being_B
being_C
being_I
being_BCI-4
) ( non
empty
being_B
being_C
being_I
being_BCI-4
)
BCI-algebra
) : ( ( non
empty
) ( non
empty
)
Subset
of ) ) : ( ( non
empty
) ( non
empty
)
Subset
of ) )
for
y
being ( ( ) ( )
Element
of
BranchV
b
: ( ( ) ( )
Element
of
AtomSet
b
1
: ( ( non
empty
being_B
being_C
being_I
being_BCI-4
) ( non
empty
being_B
being_C
being_I
being_BCI-4
)
BCI-algebra
) : ( ( non
empty
) ( non
empty
)
Subset
of ) ) : ( ( non
empty
) ( non
empty
)
Subset
of ) ) holds
x
: ( ( ) ( )
Element
of
BranchV
b
2
: ( ( ) ( )
Element
of
AtomSet
b
1
: ( ( non
empty
being_B
being_C
being_I
being_BCI-4
) ( non
empty
being_B
being_C
being_I
being_BCI-4
)
BCI-algebra
) : ( ( non
empty
) ( non
empty
)
Subset
of ) ) : ( ( non
empty
) ( non
empty
)
Subset
of ) )
\
y
: ( ( ) ( )
Element
of
BranchV
b
3
: ( ( ) ( )
Element
of
AtomSet
b
1
: ( ( non
empty
being_B
being_C
being_I
being_BCI-4
) ( non
empty
being_B
being_C
being_I
being_BCI-4
)
BCI-algebra
) : ( ( non
empty
) ( non
empty
)
Subset
of ) ) : ( ( non
empty
) ( non
empty
)
Subset
of ) ) : ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) )
in
BranchV
(
a
: ( ( ) ( )
Element
of
AtomSet
b
1
: ( ( non
empty
being_B
being_C
being_I
being_BCI-4
) ( non
empty
being_B
being_C
being_I
being_BCI-4
)
BCI-algebra
) : ( ( non
empty
) ( non
empty
)
Subset
of ) )
\
b
: ( ( ) ( )
Element
of
AtomSet
b
1
: ( ( non
empty
being_B
being_C
being_I
being_BCI-4
) ( non
empty
being_B
being_C
being_I
being_BCI-4
)
BCI-algebra
) : ( ( non
empty
) ( non
empty
)
Subset
of ) )
)
: ( ( ) ( )
Element
of
AtomSet
b
1
: ( ( non
empty
being_B
being_C
being_I
being_BCI-4
) ( non
empty
being_B
being_C
being_I
being_BCI-4
)
BCI-algebra
) : ( ( non
empty
) ( non
empty
)
Subset
of ) ) : ( ( non
empty
) ( non
empty
)
Subset
of ) ;
theorem
:: BCIALG_1:40
for
X
being ( ( non
empty
being_B
being_C
being_I
being_BCI-4
) ( non
empty
being_B
being_C
being_I
being_BCI-4
)
BCI-algebra
)
for
a
being ( ( ) ( )
Element
of
AtomSet
X
: ( ( non
empty
being_B
being_C
being_I
being_BCI-4
) ( non
empty
being_B
being_C
being_I
being_BCI-4
)
BCI-algebra
) : ( ( non
empty
) ( non
empty
)
Subset
of ) )
for
x
,
y
being ( ( ) ( )
Element
of
BranchV
a
: ( ( ) ( )
Element
of
AtomSet
b
1
: ( ( non
empty
being_B
being_C
being_I
being_BCI-4
) ( non
empty
being_B
being_C
being_I
being_BCI-4
)
BCI-algebra
) : ( ( non
empty
) ( non
empty
)
Subset
of ) ) : ( ( non
empty
) ( non
empty
)
Subset
of ) ) holds
x
: ( ( ) ( )
Element
of
BranchV
b
2
: ( ( ) ( )
Element
of
AtomSet
b
1
: ( ( non
empty
being_B
being_C
being_I
being_BCI-4
) ( non
empty
being_B
being_C
being_I
being_BCI-4
)
BCI-algebra
) : ( ( non
empty
) ( non
empty
)
Subset
of ) ) : ( ( non
empty
) ( non
empty
)
Subset
of ) )
\
y
: ( ( ) ( )
Element
of
BranchV
b
2
: ( ( ) ( )
Element
of
AtomSet
b
1
: ( ( non
empty
being_B
being_C
being_I
being_BCI-4
) ( non
empty
being_B
being_C
being_I
being_BCI-4
)
BCI-algebra
) : ( ( non
empty
) ( non
empty
)
Subset
of ) ) : ( ( non
empty
) ( non
empty
)
Subset
of ) ) : ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) )
in
BCK-part
X
: ( ( non
empty
being_B
being_C
being_I
being_BCI-4
) ( non
empty
being_B
being_C
being_I
being_BCI-4
)
BCI-algebra
) : ( ( non
empty
) ( non
empty
)
Subset
of ) ;
theorem
:: BCIALG_1:41
for
X
being ( ( non
empty
being_B
being_C
being_I
being_BCI-4
) ( non
empty
being_B
being_C
being_I
being_BCI-4
)
BCI-algebra
)
for
a
,
b
being ( ( ) ( )
Element
of
AtomSet
X
: ( ( non
empty
being_B
being_C
being_I
being_BCI-4
) ( non
empty
being_B
being_C
being_I
being_BCI-4
)
BCI-algebra
) : ( ( non
empty
) ( non
empty
)
Subset
of ) )
for
x
being ( ( ) ( )
Element
of
BranchV
a
: ( ( ) ( )
Element
of
AtomSet
b
1
: ( ( non
empty
being_B
being_C
being_I
being_BCI-4
) ( non
empty
being_B
being_C
being_I
being_BCI-4
)
BCI-algebra
) : ( ( non
empty
) ( non
empty
)
Subset
of ) ) : ( ( non
empty
) ( non
empty
)
Subset
of ) )
for
y
being ( ( ) ( )
Element
of
BranchV
b
: ( ( ) ( )
Element
of
AtomSet
b
1
: ( ( non
empty
being_B
being_C
being_I
being_BCI-4
) ( non
empty
being_B
being_C
being_I
being_BCI-4
)
BCI-algebra
) : ( ( non
empty
) ( non
empty
)
Subset
of ) ) : ( ( non
empty
) ( non
empty
)
Subset
of ) ) st
a
: ( ( ) ( )
Element
of
AtomSet
b
1
: ( ( non
empty
being_B
being_C
being_I
being_BCI-4
) ( non
empty
being_B
being_C
being_I
being_BCI-4
)
BCI-algebra
) : ( ( non
empty
) ( non
empty
)
Subset
of ) )
<>
b
: ( ( ) ( )
Element
of
AtomSet
b
1
: ( ( non
empty
being_B
being_C
being_I
being_BCI-4
) ( non
empty
being_B
being_C
being_I
being_BCI-4
)
BCI-algebra
) : ( ( non
empty
) ( non
empty
)
Subset
of ) ) holds
not
x
: ( ( ) ( )
Element
of
BranchV
b
2
: ( ( ) ( )
Element
of
AtomSet
b
1
: ( ( non
empty
being_B
being_C
being_I
being_BCI-4
) ( non
empty
being_B
being_C
being_I
being_BCI-4
)
BCI-algebra
) : ( ( non
empty
) ( non
empty
)
Subset
of ) ) : ( ( non
empty
) ( non
empty
)
Subset
of ) )
\
y
: ( ( ) ( )
Element
of
BranchV
b
3
: ( ( ) ( )
Element
of
AtomSet
b
1
: ( ( non
empty
being_B
being_C
being_I
being_BCI-4
) ( non
empty
being_B
being_C
being_I
being_BCI-4
)
BCI-algebra
) : ( ( non
empty
) ( non
empty
)
Subset
of ) ) : ( ( non
empty
) ( non
empty
)
Subset
of ) ) : ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) )
in
BCK-part
X
: ( ( non
empty
being_B
being_C
being_I
being_BCI-4
) ( non
empty
being_B
being_C
being_I
being_BCI-4
)
BCI-algebra
) : ( ( non
empty
) ( non
empty
)
Subset
of ) ;
theorem
:: BCIALG_1:42
for
X
being ( ( non
empty
being_B
being_C
being_I
being_BCI-4
) ( non
empty
being_B
being_C
being_I
being_BCI-4
)
BCI-algebra
)
for
a
,
b
being ( ( ) ( )
Element
of
AtomSet
X
: ( ( non
empty
being_B
being_C
being_I
being_BCI-4
) ( non
empty
being_B
being_C
being_I
being_BCI-4
)
BCI-algebra
) : ( ( non
empty
) ( non
empty
)
Subset
of ) ) st
a
: ( ( ) ( )
Element
of
AtomSet
b
1
: ( ( non
empty
being_B
being_C
being_I
being_BCI-4
) ( non
empty
being_B
being_C
being_I
being_BCI-4
)
BCI-algebra
) : ( ( non
empty
) ( non
empty
)
Subset
of ) )
<>
b
: ( ( ) ( )
Element
of
AtomSet
b
1
: ( ( non
empty
being_B
being_C
being_I
being_BCI-4
) ( non
empty
being_B
being_C
being_I
being_BCI-4
)
BCI-algebra
) : ( ( non
empty
) ( non
empty
)
Subset
of ) ) holds
(
BranchV
a
: ( ( ) ( )
Element
of
AtomSet
b
1
: ( ( non
empty
being_B
being_C
being_I
being_BCI-4
) ( non
empty
being_B
being_C
being_I
being_BCI-4
)
BCI-algebra
) : ( ( non
empty
) ( non
empty
)
Subset
of ) )
)
: ( ( non
empty
) ( non
empty
)
Subset
of )
/\
(
BranchV
b
: ( ( ) ( )
Element
of
AtomSet
b
1
: ( ( non
empty
being_B
being_C
being_I
being_BCI-4
) ( non
empty
being_B
being_C
being_I
being_BCI-4
)
BCI-algebra
) : ( ( non
empty
) ( non
empty
)
Subset
of ) )
)
: ( ( non
empty
) ( non
empty
)
Subset
of ) : ( ( ) ( )
Element
of
bool
the
carrier
of
b
1
: ( ( non
empty
being_B
being_C
being_I
being_BCI-4
) ( non
empty
being_B
being_C
being_I
being_BCI-4
)
BCI-algebra
) : ( ( ) ( non
empty
)
set
) : ( ( ) ( )
set
) )
=
{}
: ( ( ) ( )
set
) ;
definition
let
X
be ( ( non
empty
being_B
being_C
being_I
being_BCI-4
) ( non
empty
being_B
being_C
being_I
being_BCI-4
)
BCI-algebra
) ;
mode
Ideal
of
X
->
( ( non
empty
) ( non
empty
)
Subset
of )
means
:: BCIALG_1:def 18
(
0.
X
: ( ( non
empty
being_B
being_C
being_I
being_BCI-4
) ( non
empty
being_B
being_C
being_I
being_BCI-4
)
BCIStr_0
) : ( ( ) (
V47
(
X
: ( ( non
empty
being_B
being_C
being_I
being_BCI-4
) ( non
empty
being_B
being_C
being_I
being_BCI-4
)
BCIStr_0
) ) )
Element
of the
carrier
of
X
: ( ( non
empty
being_B
being_C
being_I
being_BCI-4
) ( non
empty
being_B
being_C
being_I
being_BCI-4
)
BCIStr_0
) : ( ( ) ( non
empty
)
set
) )
in
it
: ( ( ) ( )
set
) & ( for
x
,
y
being ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) ) st
x
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) )
\
y
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) ) : ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) )
in
it
: ( ( ) ( )
set
) &
y
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) )
in
it
: ( ( ) ( )
set
) holds
x
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) )
in
it
: ( ( ) ( )
set
) ) );
end;
definition
let
X
be ( ( non
empty
being_B
being_C
being_I
being_BCI-4
) ( non
empty
being_B
being_C
being_I
being_BCI-4
)
BCI-algebra
) ;
let
IT
be ( ( ) ( non
empty
)
Ideal
of
X
: ( ( non
empty
being_B
being_C
being_I
being_BCI-4
) ( non
empty
being_B
being_C
being_I
being_BCI-4
)
BCI-algebra
) ) ;
attr
IT
is
closed
means
:: BCIALG_1:def 19
for
x
being ( ( ) ( )
Element
of
IT
: ( ( ) ( )
set
) ) holds
x
: ( ( ) ( )
Element
of
IT
: ( ( ) ( non
empty
)
Ideal
of
X
: ( ( non
empty
being_B
being_C
being_I
being_BCI-4
) ( non
empty
being_B
being_C
being_I
being_BCI-4
)
BCI-algebra
) ) )
`
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) )
in
IT
: ( ( ) ( )
set
) ;
end;
registration
let
X
be ( ( non
empty
being_B
being_C
being_I
being_BCI-4
) ( non
empty
being_B
being_C
being_I
being_BCI-4
)
BCI-algebra
) ;
cluster
non
empty
closed
for ( ( ) ( )
Ideal
of
X
: ( ( non
empty
being_B
being_C
being_I
being_BCI-4
) ( non
empty
being_B
being_C
being_I
being_BCI-4
)
BCIStr_0
) ) ;
end;
theorem
:: BCIALG_1:43
for
X
being ( ( non
empty
being_B
being_C
being_I
being_BCI-4
) ( non
empty
being_B
being_C
being_I
being_BCI-4
)
BCI-algebra
) holds
{
(
0.
X
: ( ( non
empty
being_B
being_C
being_I
being_BCI-4
) ( non
empty
being_B
being_C
being_I
being_BCI-4
)
BCI-algebra
)
)
: ( ( ) (
V47
(
b
1
: ( ( non
empty
being_B
being_C
being_I
being_BCI-4
) ( non
empty
being_B
being_C
being_I
being_BCI-4
)
BCI-algebra
) ) )
Element
of the
carrier
of
b
1
: ( ( non
empty
being_B
being_C
being_I
being_BCI-4
) ( non
empty
being_B
being_C
being_I
being_BCI-4
)
BCI-algebra
) : ( ( ) ( non
empty
)
set
) )
}
: ( ( ) ( non
empty
trivial
V38
(1 : ( ( ) ( non
empty
)
set
) ) )
set
) is ( (
closed
) ( non
empty
closed
)
Ideal
of
X
: ( ( non
empty
being_B
being_C
being_I
being_BCI-4
) ( non
empty
being_B
being_C
being_I
being_BCI-4
)
BCI-algebra
) ) ;
theorem
:: BCIALG_1:44
for
X
being ( ( non
empty
being_B
being_C
being_I
being_BCI-4
) ( non
empty
being_B
being_C
being_I
being_BCI-4
)
BCI-algebra
) holds the
carrier
of
X
: ( ( non
empty
being_B
being_C
being_I
being_BCI-4
) ( non
empty
being_B
being_C
being_I
being_BCI-4
)
BCI-algebra
) : ( ( ) ( non
empty
)
set
) is ( (
closed
) ( non
empty
closed
)
Ideal
of
X
: ( ( non
empty
being_B
being_C
being_I
being_BCI-4
) ( non
empty
being_B
being_C
being_I
being_BCI-4
)
BCI-algebra
) ) ;
theorem
:: BCIALG_1:45
for
X
being ( ( non
empty
being_B
being_C
being_I
being_BCI-4
) ( non
empty
being_B
being_C
being_I
being_BCI-4
)
BCI-algebra
) holds
BCK-part
X
: ( ( non
empty
being_B
being_C
being_I
being_BCI-4
) ( non
empty
being_B
being_C
being_I
being_BCI-4
)
BCI-algebra
) : ( ( non
empty
) ( non
empty
)
Subset
of ) is ( (
closed
) ( non
empty
closed
)
Ideal
of
X
: ( ( non
empty
being_B
being_C
being_I
being_BCI-4
) ( non
empty
being_B
being_C
being_I
being_BCI-4
)
BCI-algebra
) ) ;
theorem
:: BCIALG_1:46
for
X
being ( ( non
empty
being_B
being_C
being_I
being_BCI-4
) ( non
empty
being_B
being_C
being_I
being_BCI-4
)
BCI-algebra
)
for
IT
being ( ( non
empty
) ( non
empty
)
Subset
of ) st
IT
: ( ( non
empty
) ( non
empty
)
Subset
of ) is ( ( ) ( non
empty
)
Ideal
of
X
: ( ( non
empty
being_B
being_C
being_I
being_BCI-4
) ( non
empty
being_B
being_C
being_I
being_BCI-4
)
BCI-algebra
) ) holds
for
x
,
y
being ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) ) st
x
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) )
in
IT
: ( ( non
empty
) ( non
empty
)
Subset
of ) &
y
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) )
<=
x
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) ) holds
y
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) )
in
IT
: ( ( non
empty
) ( non
empty
)
Subset
of ) ;
begin
definition
let
IT
be ( ( non
empty
being_B
being_C
being_I
being_BCI-4
) ( non
empty
being_B
being_C
being_I
being_BCI-4
)
BCI-algebra
) ;
attr
IT
is
associative
means
:: BCIALG_1:def 20
for
x
,
y
,
z
being ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) ) holds
(
x
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) )
\
y
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) )
)
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) )
\
z
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) ) : ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) )
=
x
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) )
\
(
y
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) )
\
z
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) )
)
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) ) : ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) ) ;
attr
IT
is
quasi-associative
means
:: BCIALG_1:def 21
for
x
being ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) ) holds
(
x
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) )
`
)
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) )
`
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) )
=
x
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) )
`
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) ) ;
attr
IT
is
positive-implicative
means
:: BCIALG_1:def 22
for
x
,
y
being ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) ) holds
(
x
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) )
\
(
x
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) )
\
y
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) )
)
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) )
)
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) )
\
(
y
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) )
\
x
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) )
)
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) ) : ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) )
=
x
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) )
\
(
x
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) )
\
(
y
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) )
\
(
y
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) )
\
x
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) )
)
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) )
)
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) )
)
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) ) : ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) ) ;
attr
IT
is
weakly-positive-implicative
means
:: BCIALG_1:def 23
for
x
,
y
,
z
being ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) ) holds
(
x
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) )
\
y
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) )
)
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) )
\
z
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) ) : ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) )
=
(
(
x
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) )
\
z
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) )
)
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) )
\
z
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) )
)
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) )
\
(
y
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) )
\
z
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) )
)
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) ) : ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) ) ;
attr
IT
is
implicative
means
:: BCIALG_1:def 24
for
x
,
y
being ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) ) holds
(
x
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) )
\
(
x
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) )
\
y
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) )
)
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) )
)
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) )
\
(
y
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) )
\
x
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) )
)
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) ) : ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) )
=
y
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) )
\
(
y
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) )
\
x
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) )
)
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) ) : ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) ) ;
attr
IT
is
weakly-implicative
means
:: BCIALG_1:def 25
for
x
,
y
being ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) ) holds
(
x
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) )
\
(
y
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) )
\
x
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) )
)
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) )
)
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) )
\
(
(
y
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) )
\
x
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) )
)
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) )
`
)
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) ) : ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) )
=
x
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) ) ;
attr
IT
is
p-Semisimple
means
:: BCIALG_1:def 26
for
x
,
y
being ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) ) holds
x
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) )
\
(
x
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) )
\
y
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) )
)
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) ) : ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) )
=
y
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) ) ;
attr
IT
is
alternative
means
:: BCIALG_1:def 27
for
x
,
y
being ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) ) holds
(
x
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) )
\
(
x
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) )
\
y
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) )
)
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) ) : ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) )
=
(
x
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) )
\
x
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) )
)
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) )
\
y
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) ) : ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) ) &
(
x
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) )
\
y
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) )
)
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) )
\
y
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) ) : ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) )
=
x
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) )
\
(
y
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) )
\
y
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) )
)
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) ) : ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) ) );
end;
registration
cluster
BCI-EXAMPLE
: ( ( ) ( non
empty
trivial
V46
() 1 : ( ( ) ( non
empty
)
set
)
-element
strict
being_B
being_C
being_I
being_BCI-4
being_BCK-5
)
BCIStr_0
)
->
associative
positive-implicative
weakly-positive-implicative
implicative
weakly-implicative
p-Semisimple
;
end;
registration
cluster
non
empty
being_B
being_C
being_I
being_BCI-4
associative
positive-implicative
weakly-positive-implicative
implicative
weakly-implicative
p-Semisimple
for ( ( ) ( )
BCIStr_0
) ;
end;
theorem
:: BCIALG_1:47
for
X
being ( ( non
empty
being_B
being_C
being_I
being_BCI-4
) ( non
empty
being_B
being_C
being_I
being_BCI-4
)
BCI-algebra
) holds
(
X
: ( ( non
empty
being_B
being_C
being_I
being_BCI-4
) ( non
empty
being_B
being_C
being_I
being_BCI-4
)
BCI-algebra
) is
associative
iff for
x
being ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) ) holds
x
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) )
`
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) )
=
x
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) ) ) ;
theorem
:: BCIALG_1:48
for
X
being ( ( non
empty
being_B
being_C
being_I
being_BCI-4
) ( non
empty
being_B
being_C
being_I
being_BCI-4
)
BCI-algebra
) holds
( ( for
x
,
y
being ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) ) holds
y
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) )
\
x
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) ) : ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) )
=
x
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) )
\
y
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) ) : ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) ) ) iff
X
: ( ( non
empty
being_B
being_C
being_I
being_BCI-4
) ( non
empty
being_B
being_C
being_I
being_BCI-4
)
BCI-algebra
) is
associative
) ;
theorem
:: BCIALG_1:49
for
X
being ( ( non
empty
) ( non
empty
)
BCIStr_0
) holds
(
X
: ( ( non
empty
) ( non
empty
)
BCIStr_0
) is ( ( non
empty
being_B
being_C
being_I
being_BCI-4
associative
) ( non
empty
being_B
being_C
being_I
being_BCI-4
associative
)
BCI-algebra
) iff for
x
,
y
,
z
being ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) ) holds
(
(
y
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) )
\
x
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) )
)
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) )
\
(
z
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) )
\
x
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) )
)
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) ) : ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) )
=
z
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) )
\
y
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) ) : ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) ) &
x
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) )
\
(
0.
X
: ( ( non
empty
) ( non
empty
)
BCIStr_0
)
)
: ( ( ) (
V47
(
b
1
: ( ( non
empty
) ( non
empty
)
BCIStr_0
) ) )
Element
of the
carrier
of
b
1
: ( ( non
empty
) ( non
empty
)
BCIStr_0
) : ( ( ) ( non
empty
)
set
) ) : ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) )
=
x
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) ) ) ) ;
theorem
:: BCIALG_1:50
for
X
being ( ( non
empty
) ( non
empty
)
BCIStr_0
) holds
(
X
: ( ( non
empty
) ( non
empty
)
BCIStr_0
) is ( ( non
empty
being_B
being_C
being_I
being_BCI-4
associative
) ( non
empty
being_B
being_C
being_I
being_BCI-4
associative
)
BCI-algebra
) iff for
x
,
y
,
z
being ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) ) holds
(
(
x
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) )
\
y
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) )
)
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) )
\
(
x
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) )
\
z
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) )
)
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) ) : ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) )
=
z
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) )
\
y
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) ) : ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) ) &
x
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) )
`
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) )
=
x
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) ) ) ) ;
theorem
:: BCIALG_1:51
for
X
being ( ( non
empty
) ( non
empty
)
BCIStr_0
) holds
(
X
: ( ( non
empty
) ( non
empty
)
BCIStr_0
) is ( ( non
empty
being_B
being_C
being_I
being_BCI-4
associative
) ( non
empty
being_B
being_C
being_I
being_BCI-4
associative
)
BCI-algebra
) iff for
x
,
y
,
z
being ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) ) holds
(
(
x
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) )
\
y
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) )
)
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) )
\
(
x
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) )
\
z
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) )
)
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) ) : ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) )
=
y
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) )
\
z
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) ) : ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) ) &
x
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) )
\
(
0.
X
: ( ( non
empty
) ( non
empty
)
BCIStr_0
)
)
: ( ( ) (
V47
(
b
1
: ( ( non
empty
) ( non
empty
)
BCIStr_0
) ) )
Element
of the
carrier
of
b
1
: ( ( non
empty
) ( non
empty
)
BCIStr_0
) : ( ( ) ( non
empty
)
set
) ) : ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) )
=
x
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) ) ) ) ;
begin
theorem
:: BCIALG_1:52
for
X
being ( ( non
empty
being_B
being_C
being_I
being_BCI-4
) ( non
empty
being_B
being_C
being_I
being_BCI-4
)
BCI-algebra
) holds
(
X
: ( ( non
empty
being_B
being_C
being_I
being_BCI-4
) ( non
empty
being_B
being_C
being_I
being_BCI-4
)
BCI-algebra
) is
p-Semisimple
iff for
x
being ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) ) holds
x
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) ) is
atom
) ;
theorem
:: BCIALG_1:53
for
X
being ( ( non
empty
being_B
being_C
being_I
being_BCI-4
) ( non
empty
being_B
being_C
being_I
being_BCI-4
)
BCI-algebra
) st
X
: ( ( non
empty
being_B
being_C
being_I
being_BCI-4
) ( non
empty
being_B
being_C
being_I
being_BCI-4
)
BCI-algebra
) is
p-Semisimple
holds
BCK-part
X
: ( ( non
empty
being_B
being_C
being_I
being_BCI-4
) ( non
empty
being_B
being_C
being_I
being_BCI-4
)
BCI-algebra
) : ( ( non
empty
) ( non
empty
)
Subset
of )
=
{
(
0.
X
: ( ( non
empty
being_B
being_C
being_I
being_BCI-4
) ( non
empty
being_B
being_C
being_I
being_BCI-4
)
BCI-algebra
)
)
: ( ( ) (
V47
(
b
1
: ( ( non
empty
being_B
being_C
being_I
being_BCI-4
) ( non
empty
being_B
being_C
being_I
being_BCI-4
)
BCI-algebra
) ) )
Element
of the
carrier
of
b
1
: ( ( non
empty
being_B
being_C
being_I
being_BCI-4
) ( non
empty
being_B
being_C
being_I
being_BCI-4
)
BCI-algebra
) : ( ( ) ( non
empty
)
set
) )
}
: ( ( ) ( non
empty
trivial
V38
(1 : ( ( ) ( non
empty
)
set
) ) )
set
) ;
theorem
:: BCIALG_1:54
for
X
being ( ( non
empty
being_B
being_C
being_I
being_BCI-4
) ( non
empty
being_B
being_C
being_I
being_BCI-4
)
BCI-algebra
) holds
(
X
: ( ( non
empty
being_B
being_C
being_I
being_BCI-4
) ( non
empty
being_B
being_C
being_I
being_BCI-4
)
BCI-algebra
) is
p-Semisimple
iff for
x
being ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) ) holds
(
x
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) )
`
)
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) )
`
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) )
=
x
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) ) ) ;
theorem
:: BCIALG_1:55
for
X
being ( ( non
empty
being_B
being_C
being_I
being_BCI-4
) ( non
empty
being_B
being_C
being_I
being_BCI-4
)
BCI-algebra
) holds
(
X
: ( ( non
empty
being_B
being_C
being_I
being_BCI-4
) ( non
empty
being_B
being_C
being_I
being_BCI-4
)
BCI-algebra
) is
p-Semisimple
iff for
x
,
y
being ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) ) holds
y
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) )
\
(
y
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) )
\
x
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) )
)
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) ) : ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) )
=
x
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) ) ) ;
theorem
:: BCIALG_1:56
for
X
being ( ( non
empty
being_B
being_C
being_I
being_BCI-4
) ( non
empty
being_B
being_C
being_I
being_BCI-4
)
BCI-algebra
) holds
(
X
: ( ( non
empty
being_B
being_C
being_I
being_BCI-4
) ( non
empty
being_B
being_C
being_I
being_BCI-4
)
BCI-algebra
) is
p-Semisimple
iff for
x
,
y
,
z
being ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) ) holds
(
z
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) )
\
y
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) )
)
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) )
\
(
z
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) )
\
x
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) )
)
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) ) : ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) )
=
x
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) )
\
y
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) ) : ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) ) ) ;
theorem
:: BCIALG_1:57
for
X
being ( ( non
empty
being_B
being_C
being_I
being_BCI-4
) ( non
empty
being_B
being_C
being_I
being_BCI-4
)
BCI-algebra
) holds
(
X
: ( ( non
empty
being_B
being_C
being_I
being_BCI-4
) ( non
empty
being_B
being_C
being_I
being_BCI-4
)
BCI-algebra
) is
p-Semisimple
iff for
x
,
y
,
z
being ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) ) holds
x
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) )
\
(
z
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) )
\
y
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) )
)
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) ) : ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) )
=
y
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) )
\
(
z
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) )
\
x
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) )
)
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) ) : ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) ) ) ;
theorem
:: BCIALG_1:58
for
X
being ( ( non
empty
being_B
being_C
being_I
being_BCI-4
) ( non
empty
being_B
being_C
being_I
being_BCI-4
)
BCI-algebra
) holds
(
X
: ( ( non
empty
being_B
being_C
being_I
being_BCI-4
) ( non
empty
being_B
being_C
being_I
being_BCI-4
)
BCI-algebra
) is
p-Semisimple
iff for
x
,
y
,
z
,
u
being ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) ) holds
(
x
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) )
\
u
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) )
)
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) )
\
(
z
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) )
\
y
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) )
)
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) ) : ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) )
=
(
y
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) )
\
u
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) )
)
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) )
\
(
z
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) )
\
x
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) )
)
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) ) : ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) ) ) ;
theorem
:: BCIALG_1:59
for
X
being ( ( non
empty
being_B
being_C
being_I
being_BCI-4
) ( non
empty
being_B
being_C
being_I
being_BCI-4
)
BCI-algebra
) holds
(
X
: ( ( non
empty
being_B
being_C
being_I
being_BCI-4
) ( non
empty
being_B
being_C
being_I
being_BCI-4
)
BCI-algebra
) is
p-Semisimple
iff for
x
,
z
being ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) ) holds
(
z
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) )
`
)
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) )
\
(
x
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) )
`
)
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) ) : ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) )
=
x
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) )
\
z
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) ) : ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) ) ) ;
theorem
:: BCIALG_1:60
for
X
being ( ( non
empty
being_B
being_C
being_I
being_BCI-4
) ( non
empty
being_B
being_C
being_I
being_BCI-4
)
BCI-algebra
) holds
(
X
: ( ( non
empty
being_B
being_C
being_I
being_BCI-4
) ( non
empty
being_B
being_C
being_I
being_BCI-4
)
BCI-algebra
) is
p-Semisimple
iff for
x
,
z
being ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) ) holds
(
(
x
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) )
\
z
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) )
)
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) )
`
)
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) )
`
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) )
=
x
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) )
\
z
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) ) : ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) ) ) ;
theorem
:: BCIALG_1:61
for
X
being ( ( non
empty
being_B
being_C
being_I
being_BCI-4
) ( non
empty
being_B
being_C
being_I
being_BCI-4
)
BCI-algebra
) holds
(
X
: ( ( non
empty
being_B
being_C
being_I
being_BCI-4
) ( non
empty
being_B
being_C
being_I
being_BCI-4
)
BCI-algebra
) is
p-Semisimple
iff for
x
,
u
,
z
being ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) ) holds
z
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) )
\
(
z
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) )
\
(
x
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) )
\
u
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) )
)
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) )
)
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) ) : ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) )
=
x
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) )
\
u
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) ) : ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) ) ) ;
theorem
:: BCIALG_1:62
for
X
being ( ( non
empty
being_B
being_C
being_I
being_BCI-4
) ( non
empty
being_B
being_C
being_I
being_BCI-4
)
BCI-algebra
) holds
(
X
: ( ( non
empty
being_B
being_C
being_I
being_BCI-4
) ( non
empty
being_B
being_C
being_I
being_BCI-4
)
BCI-algebra
) is
p-Semisimple
iff for
x
being ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) ) st
x
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) )
`
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) )
=
0.
X
: ( ( non
empty
being_B
being_C
being_I
being_BCI-4
) ( non
empty
being_B
being_C
being_I
being_BCI-4
)
BCI-algebra
) : ( ( ) (
V47
(
b
1
: ( ( non
empty
being_B
being_C
being_I
being_BCI-4
) ( non
empty
being_B
being_C
being_I
being_BCI-4
)
BCI-algebra
) ) )
Element
of the
carrier
of
b
1
: ( ( non
empty
being_B
being_C
being_I
being_BCI-4
) ( non
empty
being_B
being_C
being_I
being_BCI-4
)
BCI-algebra
) : ( ( ) ( non
empty
)
set
) ) holds
x
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) )
=
0.
X
: ( ( non
empty
being_B
being_C
being_I
being_BCI-4
) ( non
empty
being_B
being_C
being_I
being_BCI-4
)
BCI-algebra
) : ( ( ) (
V47
(
b
1
: ( ( non
empty
being_B
being_C
being_I
being_BCI-4
) ( non
empty
being_B
being_C
being_I
being_BCI-4
)
BCI-algebra
) ) )
Element
of the
carrier
of
b
1
: ( ( non
empty
being_B
being_C
being_I
being_BCI-4
) ( non
empty
being_B
being_C
being_I
being_BCI-4
)
BCI-algebra
) : ( ( ) ( non
empty
)
set
) ) ) ;
theorem
:: BCIALG_1:63
for
X
being ( ( non
empty
being_B
being_C
being_I
being_BCI-4
) ( non
empty
being_B
being_C
being_I
being_BCI-4
)
BCI-algebra
) holds
(
X
: ( ( non
empty
being_B
being_C
being_I
being_BCI-4
) ( non
empty
being_B
being_C
being_I
being_BCI-4
)
BCI-algebra
) is
p-Semisimple
iff for
x
,
y
being ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) ) holds
x
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) )
\
(
y
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) )
`
)
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) ) : ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) )
=
y
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) )
\
(
x
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) )
`
)
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) ) : ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) ) ) ;
theorem
:: BCIALG_1:64
for
X
being ( ( non
empty
being_B
being_C
being_I
being_BCI-4
) ( non
empty
being_B
being_C
being_I
being_BCI-4
)
BCI-algebra
) holds
(
X
: ( ( non
empty
being_B
being_C
being_I
being_BCI-4
) ( non
empty
being_B
being_C
being_I
being_BCI-4
)
BCI-algebra
) is
p-Semisimple
iff for
x
,
y
,
z
,
u
being ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) ) holds
(
x
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) )
\
y
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) )
)
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) )
\
(
z
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) )
\
u
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) )
)
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) ) : ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) )
=
(
x
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) )
\
z
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) )
)
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) )
\
(
y
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) )
\
u
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) )
)
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) ) : ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) ) ) ;
theorem
:: BCIALG_1:65
for
X
being ( ( non
empty
being_B
being_C
being_I
being_BCI-4
) ( non
empty
being_B
being_C
being_I
being_BCI-4
)
BCI-algebra
) holds
(
X
: ( ( non
empty
being_B
being_C
being_I
being_BCI-4
) ( non
empty
being_B
being_C
being_I
being_BCI-4
)
BCI-algebra
) is
p-Semisimple
iff for
x
,
y
,
z
being ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) ) holds
(
x
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) )
\
y
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) )
)
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) )
\
(
z
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) )
\
y
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) )
)
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) ) : ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) )
=
x
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) )
\
z
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) ) : ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) ) ) ;
theorem
:: BCIALG_1:66
for
X
being ( ( non
empty
being_B
being_C
being_I
being_BCI-4
) ( non
empty
being_B
being_C
being_I
being_BCI-4
)
BCI-algebra
) holds
(
X
: ( ( non
empty
being_B
being_C
being_I
being_BCI-4
) ( non
empty
being_B
being_C
being_I
being_BCI-4
)
BCI-algebra
) is
p-Semisimple
iff for
x
,
y
,
z
being ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) ) holds
x
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) )
\
(
y
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) )
\
z
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) )
)
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) ) : ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) )
=
(
z
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) )
\
y
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) )
)
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) )
\
(
x
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) )
`
)
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) ) : ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) ) ) ;
theorem
:: BCIALG_1:67
for
X
being ( ( non
empty
being_B
being_C
being_I
being_BCI-4
) ( non
empty
being_B
being_C
being_I
being_BCI-4
)
BCI-algebra
) holds
(
X
: ( ( non
empty
being_B
being_C
being_I
being_BCI-4
) ( non
empty
being_B
being_C
being_I
being_BCI-4
)
BCI-algebra
) is
p-Semisimple
iff for
x
,
y
,
z
being ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) ) st
y
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) )
\
x
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) ) : ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) )
=
z
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) )
\
x
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) ) : ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) ) holds
y
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) )
=
z
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) ) ) ;
theorem
:: BCIALG_1:68
for
X
being ( ( non
empty
being_B
being_C
being_I
being_BCI-4
) ( non
empty
being_B
being_C
being_I
being_BCI-4
)
BCI-algebra
) holds
(
X
: ( ( non
empty
being_B
being_C
being_I
being_BCI-4
) ( non
empty
being_B
being_C
being_I
being_BCI-4
)
BCI-algebra
) is
p-Semisimple
iff for
x
,
y
,
z
being ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) ) st
x
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) )
\
y
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) ) : ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) )
=
x
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) )
\
z
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) ) : ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) ) holds
y
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) )
=
z
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) ) ) ;
theorem
:: BCIALG_1:69
for
X
being ( ( non
empty
) ( non
empty
)
BCIStr_0
) holds
(
X
: ( ( non
empty
) ( non
empty
)
BCIStr_0
) is ( ( non
empty
being_B
being_C
being_I
being_BCI-4
p-Semisimple
) ( non
empty
being_B
being_C
being_I
being_BCI-4
p-Semisimple
)
BCI-algebra
) iff for
x
,
y
,
z
being ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) ) holds
(
(
x
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) )
\
y
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) )
)
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) )
\
(
x
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) )
\
z
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) )
)
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) ) : ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) )
=
z
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) )
\
y
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) ) : ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) ) &
x
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) )
\
(
0.
X
: ( ( non
empty
) ( non
empty
)
BCIStr_0
)
)
: ( ( ) (
V47
(
b
1
: ( ( non
empty
) ( non
empty
)
BCIStr_0
) ) )
Element
of the
carrier
of
b
1
: ( ( non
empty
) ( non
empty
)
BCIStr_0
) : ( ( ) ( non
empty
)
set
) ) : ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) )
=
x
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) ) ) ) ;
theorem
:: BCIALG_1:70
for
X
being ( ( non
empty
) ( non
empty
)
BCIStr_0
) holds
(
X
: ( ( non
empty
) ( non
empty
)
BCIStr_0
) is ( ( non
empty
being_B
being_C
being_I
being_BCI-4
p-Semisimple
) ( non
empty
being_B
being_C
being_I
being_BCI-4
p-Semisimple
)
BCI-algebra
) iff (
X
: ( ( non
empty
) ( non
empty
)
BCIStr_0
) is
being_I
& ( for
x
,
y
,
z
being ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) ) holds
(
x
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) )
\
(
y
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) )
\
z
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) )
)
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) ) : ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) )
=
z
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) )
\
(
y
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) )
\
x
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) )
)
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) ) : ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) ) &
x
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) )
\
(
0.
X
: ( ( non
empty
) ( non
empty
)
BCIStr_0
)
)
: ( ( ) (
V47
(
b
1
: ( ( non
empty
) ( non
empty
)
BCIStr_0
) ) )
Element
of the
carrier
of
b
1
: ( ( non
empty
) ( non
empty
)
BCIStr_0
) : ( ( ) ( non
empty
)
set
) ) : ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) )
=
x
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) ) ) ) ) ) ;
begin
theorem
:: BCIALG_1:71
for
X
being ( ( non
empty
being_B
being_C
being_I
being_BCI-4
) ( non
empty
being_B
being_C
being_I
being_BCI-4
)
BCI-algebra
) holds
(
X
: ( ( non
empty
being_B
being_C
being_I
being_BCI-4
) ( non
empty
being_B
being_C
being_I
being_BCI-4
)
BCI-algebra
) is
quasi-associative
iff for
x
being ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) ) holds
x
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) )
`
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) )
<=
x
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) ) ) ;
theorem
:: BCIALG_1:72
for
X
being ( ( non
empty
being_B
being_C
being_I
being_BCI-4
) ( non
empty
being_B
being_C
being_I
being_BCI-4
)
BCI-algebra
) holds
(
X
: ( ( non
empty
being_B
being_C
being_I
being_BCI-4
) ( non
empty
being_B
being_C
being_I
being_BCI-4
)
BCI-algebra
) is
quasi-associative
iff for
x
,
y
being ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) ) holds
(
x
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) )
\
y
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) )
)
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) )
`
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) )
=
(
y
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) )
\
x
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) )
)
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) )
`
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) ) ) ;
theorem
:: BCIALG_1:73
for
X
being ( ( non
empty
being_B
being_C
being_I
being_BCI-4
) ( non
empty
being_B
being_C
being_I
being_BCI-4
)
BCI-algebra
) holds
(
X
: ( ( non
empty
being_B
being_C
being_I
being_BCI-4
) ( non
empty
being_B
being_C
being_I
being_BCI-4
)
BCI-algebra
) is
quasi-associative
iff for
x
,
y
being ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) ) holds
(
x
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) )
`
)
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) )
\
y
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) ) : ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) )
=
(
x
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) )
\
y
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) )
)
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) )
`
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) ) ) ;
theorem
:: BCIALG_1:74
for
X
being ( ( non
empty
being_B
being_C
being_I
being_BCI-4
) ( non
empty
being_B
being_C
being_I
being_BCI-4
)
BCI-algebra
) holds
(
X
: ( ( non
empty
being_B
being_C
being_I
being_BCI-4
) ( non
empty
being_B
being_C
being_I
being_BCI-4
)
BCI-algebra
) is
quasi-associative
iff for
x
,
y
being ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) ) holds
(
x
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) )
\
y
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) )
)
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) )
\
(
y
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) )
\
x
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) )
)
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) ) : ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) )
in
BCK-part
X
: ( ( non
empty
being_B
being_C
being_I
being_BCI-4
) ( non
empty
being_B
being_C
being_I
being_BCI-4
)
BCI-algebra
) : ( ( non
empty
) ( non
empty
)
Subset
of ) ) ;
theorem
:: BCIALG_1:75
for
X
being ( ( non
empty
being_B
being_C
being_I
being_BCI-4
) ( non
empty
being_B
being_C
being_I
being_BCI-4
)
BCI-algebra
) holds
(
X
: ( ( non
empty
being_B
being_C
being_I
being_BCI-4
) ( non
empty
being_B
being_C
being_I
being_BCI-4
)
BCI-algebra
) is
quasi-associative
iff for
x
,
y
,
z
being ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) ) holds
(
x
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) )
\
y
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) )
)
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) )
\
z
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) ) : ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) )
<=
x
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) )
\
(
y
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) )
\
z
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) )
)
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) ) : ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) ) ) ;
begin
theorem
:: BCIALG_1:76
for
X
being ( ( non
empty
being_B
being_C
being_I
being_BCI-4
) ( non
empty
being_B
being_C
being_I
being_BCI-4
)
BCI-algebra
)
for
x
,
y
being ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) ) st
X
: ( ( non
empty
being_B
being_C
being_I
being_BCI-4
) ( non
empty
being_B
being_C
being_I
being_BCI-4
)
BCI-algebra
) is
alternative
holds
(
x
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) )
`
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) )
=
x
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) ) &
x
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) )
\
(
x
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) )
\
y
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) )
)
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) ) : ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) )
=
y
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) ) &
(
x
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) )
\
y
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) )
)
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) )
\
y
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) ) : ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) )
=
x
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) ) ) ;
theorem
:: BCIALG_1:77
for
X
being ( ( non
empty
being_B
being_C
being_I
being_BCI-4
) ( non
empty
being_B
being_C
being_I
being_BCI-4
)
BCI-algebra
)
for
x
,
a
,
b
being ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) ) st
X
: ( ( non
empty
being_B
being_C
being_I
being_BCI-4
) ( non
empty
being_B
being_C
being_I
being_BCI-4
)
BCI-algebra
) is
alternative
&
x
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) )
\
a
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) ) : ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) )
=
x
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) )
\
b
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) ) : ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) ) holds
a
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) )
=
b
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) ) ;
theorem
:: BCIALG_1:78
for
X
being ( ( non
empty
being_B
being_C
being_I
being_BCI-4
) ( non
empty
being_B
being_C
being_I
being_BCI-4
)
BCI-algebra
)
for
a
,
x
,
b
being ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) ) st
X
: ( ( non
empty
being_B
being_C
being_I
being_BCI-4
) ( non
empty
being_B
being_C
being_I
being_BCI-4
)
BCI-algebra
) is
alternative
&
a
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) )
\
x
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) ) : ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) )
=
b
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) )
\
x
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) ) : ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) ) holds
a
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) )
=
b
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) ) ;
theorem
:: BCIALG_1:79
for
X
being ( ( non
empty
being_B
being_C
being_I
being_BCI-4
) ( non
empty
being_B
being_C
being_I
being_BCI-4
)
BCI-algebra
)
for
x
,
y
being ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) ) st
X
: ( ( non
empty
being_B
being_C
being_I
being_BCI-4
) ( non
empty
being_B
being_C
being_I
being_BCI-4
)
BCI-algebra
) is
alternative
&
x
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) )
\
y
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) ) : ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) )
=
0.
X
: ( ( non
empty
being_B
being_C
being_I
being_BCI-4
) ( non
empty
being_B
being_C
being_I
being_BCI-4
)
BCI-algebra
) : ( ( ) (
V47
(
b
1
: ( ( non
empty
being_B
being_C
being_I
being_BCI-4
) ( non
empty
being_B
being_C
being_I
being_BCI-4
)
BCI-algebra
) ) )
Element
of the
carrier
of
b
1
: ( ( non
empty
being_B
being_C
being_I
being_BCI-4
) ( non
empty
being_B
being_C
being_I
being_BCI-4
)
BCI-algebra
) : ( ( ) ( non
empty
)
set
) ) holds
x
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) )
=
y
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) ) ;
theorem
:: BCIALG_1:80
for
X
being ( ( non
empty
being_B
being_C
being_I
being_BCI-4
) ( non
empty
being_B
being_C
being_I
being_BCI-4
)
BCI-algebra
)
for
x
,
a
,
b
being ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) ) st
X
: ( ( non
empty
being_B
being_C
being_I
being_BCI-4
) ( non
empty
being_B
being_C
being_I
being_BCI-4
)
BCI-algebra
) is
alternative
&
(
x
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) )
\
a
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) )
)
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) )
\
b
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) ) : ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) )
=
0.
X
: ( ( non
empty
being_B
being_C
being_I
being_BCI-4
) ( non
empty
being_B
being_C
being_I
being_BCI-4
)
BCI-algebra
) : ( ( ) (
V47
(
b
1
: ( ( non
empty
being_B
being_C
being_I
being_BCI-4
) ( non
empty
being_B
being_C
being_I
being_BCI-4
)
BCI-algebra
) ) )
Element
of the
carrier
of
b
1
: ( ( non
empty
being_B
being_C
being_I
being_BCI-4
) ( non
empty
being_B
being_C
being_I
being_BCI-4
)
BCI-algebra
) : ( ( ) ( non
empty
)
set
) ) holds
(
a
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) )
=
x
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) )
\
b
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) ) : ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) ) &
b
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) )
=
x
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) )
\
a
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) ) : ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) ) ) ;
registration
cluster
non
empty
being_B
being_C
being_I
being_BCI-4
alternative
->
non
empty
being_B
being_C
being_I
being_BCI-4
associative
for ( ( ) ( )
BCIStr_0
) ;
cluster
non
empty
being_B
being_C
being_I
being_BCI-4
associative
->
non
empty
being_B
being_C
being_I
being_BCI-4
alternative
for ( ( ) ( )
BCIStr_0
) ;
cluster
non
empty
being_B
being_C
being_I
being_BCI-4
alternative
->
non
empty
being_B
being_C
being_I
being_BCI-4
implicative
for ( ( ) ( )
BCIStr_0
) ;
end;
theorem
:: BCIALG_1:81
for
X
being ( ( non
empty
being_B
being_C
being_I
being_BCI-4
) ( non
empty
being_B
being_C
being_I
being_BCI-4
)
BCI-algebra
)
for
x
,
y
being ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) ) st
X
: ( ( non
empty
being_B
being_C
being_I
being_BCI-4
) ( non
empty
being_B
being_C
being_I
being_BCI-4
)
BCI-algebra
) is
alternative
holds
(
x
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) )
\
(
x
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) )
\
y
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) )
)
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) )
)
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) )
\
(
y
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) )
\
x
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) )
)
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) ) : ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) )
=
x
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) ) ;
theorem
:: BCIALG_1:82
for
X
being ( ( non
empty
being_B
being_C
being_I
being_BCI-4
) ( non
empty
being_B
being_C
being_I
being_BCI-4
)
BCI-algebra
)
for
y
,
x
being ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) ) st
X
: ( ( non
empty
being_B
being_C
being_I
being_BCI-4
) ( non
empty
being_B
being_C
being_I
being_BCI-4
)
BCI-algebra
) is
alternative
holds
y
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) )
\
(
y
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) )
\
(
x
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) )
\
(
x
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) )
\
y
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) )
)
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) )
)
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) )
)
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) ) : ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) )
=
y
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) ) ;
begin
registration
cluster
non
empty
being_B
being_C
being_I
being_BCI-4
associative
->
non
empty
being_B
being_C
being_I
being_BCI-4
weakly-positive-implicative
for ( ( ) ( )
BCIStr_0
) ;
cluster
non
empty
being_B
being_C
being_I
being_BCI-4
p-Semisimple
->
non
empty
being_B
being_C
being_I
being_BCI-4
weakly-positive-implicative
for ( ( ) ( )
BCIStr_0
) ;
end;
theorem
:: BCIALG_1:83
for
X
being ( ( non
empty
) ( non
empty
)
BCIStr_0
) holds
(
X
: ( ( non
empty
) ( non
empty
)
BCIStr_0
) is ( ( non
empty
being_B
being_C
being_I
being_BCI-4
implicative
) ( non
empty
being_B
being_C
being_I
being_BCI-4
implicative
)
BCI-algebra
) iff for
x
,
y
,
z
being ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) ) holds
(
(
(
x
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) )
\
y
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) )
)
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) )
\
(
x
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) )
\
z
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) )
)
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) )
)
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) )
\
(
z
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) )
\
y
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) )
)
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) ) : ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) )
=
0.
X
: ( ( non
empty
) ( non
empty
)
BCIStr_0
) : ( ( ) (
V47
(
b
1
: ( ( non
empty
) ( non
empty
)
BCIStr_0
) ) )
Element
of the
carrier
of
b
1
: ( ( non
empty
) ( non
empty
)
BCIStr_0
) : ( ( ) ( non
empty
)
set
) ) &
x
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) )
\
(
0.
X
: ( ( non
empty
) ( non
empty
)
BCIStr_0
)
)
: ( ( ) (
V47
(
b
1
: ( ( non
empty
) ( non
empty
)
BCIStr_0
) ) )
Element
of the
carrier
of
b
1
: ( ( non
empty
) ( non
empty
)
BCIStr_0
) : ( ( ) ( non
empty
)
set
) ) : ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) )
=
x
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) ) &
(
x
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) )
\
(
x
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) )
\
y
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) )
)
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) )
)
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) )
\
(
y
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) )
\
x
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) )
)
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) ) : ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) )
=
y
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) )
\
(
y
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) )
\
x
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) )
)
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) ) : ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) ) ) ) ;
theorem
:: BCIALG_1:84
for
X
being ( ( non
empty
being_B
being_C
being_I
being_BCI-4
) ( non
empty
being_B
being_C
being_I
being_BCI-4
)
BCI-algebra
) holds
(
X
: ( ( non
empty
being_B
being_C
being_I
being_BCI-4
) ( non
empty
being_B
being_C
being_I
being_BCI-4
)
BCI-algebra
) is
weakly-positive-implicative
iff for
x
,
y
being ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) ) holds
x
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) )
\
y
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) ) : ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) )
=
(
(
x
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) )
\
y
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) )
)
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) )
\
y
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) )
)
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) )
\
(
y
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) )
`
)
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) ) : ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) ) ) ;
registration
cluster
non
empty
being_B
being_C
being_I
being_BCI-4
positive-implicative
->
non
empty
being_B
being_C
being_I
being_BCI-4
weakly-positive-implicative
for ( ( ) ( )
BCIStr_0
) ;
cluster
non
empty
being_B
being_C
being_I
being_BCI-4
alternative
->
non
empty
being_B
being_C
being_I
being_BCI-4
weakly-positive-implicative
for ( ( ) ( )
BCIStr_0
) ;
end;
theorem
:: BCIALG_1:85
for
X
being ( ( non
empty
being_B
being_C
being_I
being_BCI-4
) ( non
empty
being_B
being_C
being_I
being_BCI-4
)
BCI-algebra
) st
X
: ( ( non
empty
being_B
being_C
being_I
being_BCI-4
) ( non
empty
being_B
being_C
being_I
being_BCI-4
)
BCI-algebra
) is ( ( non
empty
being_B
being_C
being_I
being_BCI-4
weakly-positive-implicative
) ( non
empty
being_B
being_C
being_I
being_BCI-4
weakly-positive-implicative
)
BCI-algebra
) holds
for
x
,
y
being ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) ) holds
(
x
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) )
\
(
x
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) )
\
y
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) )
)
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) )
)
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) )
\
(
y
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) )
\
x
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) )
)
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) ) : ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) )
=
(
(
y
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) )
\
(
y
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) )
\
x
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) )
)
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) )
)
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) )
\
(
y
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) )
\
x
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) )
)
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) )
)
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) )
\
(
x
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) )
\
y
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) )
)
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) ) : ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) ) ;
theorem
:: BCIALG_1:86
for
X
being ( ( non
empty
) ( non
empty
)
BCIStr_0
) holds
(
X
: ( ( non
empty
) ( non
empty
)
BCIStr_0
) is ( ( non
empty
being_B
being_C
being_I
being_BCI-4
positive-implicative
) ( non
empty
being_B
being_C
being_I
being_BCI-4
positive-implicative
weakly-positive-implicative
)
BCI-algebra
) iff for
x
,
y
,
z
being ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) ) holds
(
(
(
x
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) )
\
y
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) )
)
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) )
\
(
x
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) )
\
z
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) )
)
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) )
)
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) )
\
(
z
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) )
\
y
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) )
)
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) ) : ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) )
=
0.
X
: ( ( non
empty
) ( non
empty
)
BCIStr_0
) : ( ( ) (
V47
(
b
1
: ( ( non
empty
) ( non
empty
)
BCIStr_0
) ) )
Element
of the
carrier
of
b
1
: ( ( non
empty
) ( non
empty
)
BCIStr_0
) : ( ( ) ( non
empty
)
set
) ) &
x
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) )
\
(
0.
X
: ( ( non
empty
) ( non
empty
)
BCIStr_0
)
)
: ( ( ) (
V47
(
b
1
: ( ( non
empty
) ( non
empty
)
BCIStr_0
) ) )
Element
of the
carrier
of
b
1
: ( ( non
empty
) ( non
empty
)
BCIStr_0
) : ( ( ) ( non
empty
)
set
) ) : ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) )
=
x
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) ) &
x
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) )
\
y
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) ) : ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) )
=
(
(
x
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) )
\
y
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) )
)
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) )
\
y
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) )
)
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) )
\
(
y
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) )
`
)
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) ) : ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) ) &
(
x
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) )
\
(
x
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) )
\
y
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) )
)
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) )
)
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) )
\
(
y
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) )
\
x
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) )
)
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) ) : ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) )
=
(
(
y
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) )
\
(
y
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) )
\
x
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) )
)
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) )
)
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) )
\
(
y
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) )
\
x
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) )
)
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) )
)
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) )
\
(
x
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) )
\
y
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) )
)
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) ) : ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) ) ) ) ;