:: BINOP_1 semantic presentation
:: deftheorem defines . BINOP_1:def 1 :
theorem E1: :: BINOP_1:1
for b
1, b
2, b
3 being
set for b
4, b
5 being
Function of
[:b1,b2:],b
3 holds
( ( for b
6, b
7 being
set holds
( ( b
6 in b
1 & b
7 in b
2 ) implies ( b
4 . b
6,b
7 = b
5 . b
6,b
7 ) ) ) implies b
4 = b
5 )
proof
let c
1, c
2, c
3 be
set ;
let c
4, c
5 be
Function of
[:c1,c2:],c
3;
assume E2:
for b
1, b
2 being
set holds
( ( b
1 in c
1 & b
2 in c
2 ) implies ( c
4 . b
1,b
2 = c
5 . b
1,b
2 ) )
;
for b
1 being
set holds
( b
1 in [:c1,c2:] implies c
4 . b
1 = c
5 . b
1 )
proof
let c
6 be
set ;
assume
c
6 in [:c1,c2:]
;
then consider c
7, c
8 being
set such that E3:
( c
7 in c
1 & c
8 in c
2 )
and E4:
c
6 = [c7,c8]
by ZFMISC_1:def 2;
( c
4 . c
7,c
8 = c
4 . c
6 & c
5 . c
7,c
8 = c
5 . c
6 )
by E4;
hence
c
4 . c
6 = c
5 . c
6
by E2, E3;
end;
hence
c
4 = c
5
by FUNCT_2:18;
end;
theorem :: BINOP_1:2
for b
1, b
2, b
3 being
set for b
4, b
5 being
Function of
[:b1,b2:],b
3 holds
( ( for b
6 being
Element of b
1for b
7 being
Element of b
2 holds b
4 . b
6,b
7 = b
5 . b
6,b
7 ) implies b
4 = b
5 )
proof
let c
1, c
2, c
3 be
set ;
let c
4, c
5 be
Function of
[:c1,c2:],c
3;
assume
for b
1 being
Element of c
1for b
2 being
Element of c
2 holds c
4 . b
1,b
2 = c
5 . b
1,b
2
;
then
for b
1, b
2 being
set holds
( ( b
1 in c
1 & b
2 in c
2 ) implies ( c
4 . b
1,b
2 = c
5 . b
1,b
2 ) )
;
hence
c
4 = c
5
by E1;
end;
scheme :: BINOP_1:sch 1
s1{ F
1()
-> set , F
2()
-> set , F
3()
-> set , P
1[
set ,
set ,
set ] } :
ex b
1 being
Function of
[:F1(),F2():],F
3() st
for b
2, b
3 being
set holds
( ( b
2 in F
1() & b
3 in F
2() ) implies ( P
1[b
2,b
3,b
1 . b
2,b
3] ) )
E2:
for b
1, b
2 being
set holds
not ( b
1 in F
1() & b
2 in F
2() & ( for b
3 being
set holds
not ( b
3 in F
3() & P
1[b
1,b
2,b
3] ) ) )
proof
defpred S
1[
set ,
set ] means for b
1, b
2 being
set holds
( a
1 = [b1,b2] implies P
1[b
1,b
2,a
2] );
E3:
for b
1 being
set holds
not ( b
1 in [:F1(),F2():] & ( for b
2 being
set holds
not ( b
2 in F
3() & S
1[b
1,b
2] ) ) )
proof
let c
1 be
set ;
assume
c
1 in [:F1(),F2():]
;
then consider c
2, c
3 being
set such that E4:
( c
2 in F
1() & c
3 in F
2() )
and E5:
c
1 = [c2,c3]
by ZFMISC_1:def 2;
consider c
4 being
set such that E6:
c
4 in F
3()
and E7:
P
1[c
2,c
3,c
4]
by E2, E4;
take
c
4
;
thus
c
4 in F
3()
by E6;
let c
5, c
6 be
set ;
assume
c
1 = [c5,c6]
;
then
( c
2 = c
5 & c
3 = c
6 )
by E5, ZFMISC_1:33;
hence
P
1[c
5,c
6,c
4]
by E7;
end;
consider c
1 being
Function of
[:F1(),F2():],F
3()
such that E4:
for b
1 being
set holds
( b
1 in [:F1(),F2():] implies S
1[b
1,c
1 . b
1] )
from FUNCT_2:sch 1(E3);
take
c
1
;
let c
2, c
3 be
set ;
assume
( c
2 in F
1() & c
3 in F
2() )
;
then
[c2,c3] in [:F1(),F2():]
by ZFMISC_1:def 2;
hence
P
1[c
2,c
3,c
1 . c
2,c
3]
by E4;
end;
scheme :: BINOP_1:sch 2
s2{ F
1()
-> set , F
2()
-> set , F
3()
-> set , F
4(
set ,
set )
-> set } :
ex b
1 being
Function of
[:F1(),F2():],F
3() st
for b
2, b
3 being
set holds
( ( b
2 in F
1() & b
3 in F
2() ) implies ( b
1 . b
2,b
3 = F
4(b
2,b
3) ) )
E2:
for b
1, b
2 being
set holds
( ( b
1 in F
1() & b
2 in F
2() ) implies ( F
4(b
1,b
2)
in F
3() ) )
proof
defpred S
1[
set ,
set ,
set ] means a
3 = F
4(a
1,a
2);
E3:
for b
1, b
2 being
set holds
not ( b
1 in F
1() & b
2 in F
2() & ( for b
3 being
set holds
not ( b
3 in F
3() & S
1[b
1,b
2,b
3] ) ) )
proof
let c
1, c
2 be
set ;
assume E4:
( c
1 in F
1() & c
2 in F
2() )
;
take
F
4(c
1,c
2)
;
thus
( F
4(c
1,c
2)
in F
3() & S
1[c
1,c
2,F
4(c
1,c
2)] )
by E2, E4;
end;
thus
ex b
1 being
Function of
[:F1(),F2():],F
3() st
for b
2, b
3 being
set holds
( ( b
2 in F
1() & b
3 in F
2() ) implies ( S
1[b
2,b
3,b
1 . b
2,b
3] ) )
from BINOP_1:sch 1(E3);
end;
scheme :: BINOP_1:sch 3
s3{ F
1()
-> non
empty set , F
2()
-> non
empty set , F
3()
-> non
empty set , P
1[
set ,
set ,
set ] } :
provided
E2:
for b
1 being
Element of F
1()
for b
2 being
Element of F
2() holds
ex b
3 being
Element of F
3() st P
1[b
1,b
2,b
3]
proof
defpred S
1[
set ,
set ] means for b
1 being
Element of F
1()
for b
2 being
Element of F
2() holds
( a
1 = [b1,b2] implies P
1[b
1,b
2,a
2] );
E3:
for b
1 being
Element of
[:F1(),F2():] holds
ex b
2 being
Element of F
3() st
S
1[b
1,b
2]
proof
let c
1 be
Element of
[:F1(),F2():];
consider c
2, c
3 being
set such that E4:
c
2 in F
1()
and E5:
c
3 in F
2()
and E6:
c
1 = [c2,c3]
by ZFMISC_1:def 2;
reconsider c
4 = c
2 as
Element of F
1()
by E4;
reconsider c
5 = c
3 as
Element of F
2()
by E5;
consider c
6 being
Element of F
3()
such that E7:
P
1[c
4,c
5,c
6]
by E2;
take
c
6
;
let c
7 be
Element of F
1();
let c
8 be
Element of F
2();
assume
c
1 = [c7,c8]
;
then
( c
4 = c
7 & c
5 = c
8 )
by E6, ZFMISC_1:33;
hence
P
1[c
7,c
8,c
6]
by E7;
end;
consider c
1 being
Function of
[:F1(),F2():],F
3()
such that E4:
for b
1 being
Element of
[:F1(),F2():] holds
S
1[b
1,c
1 . b
1]
from FUNCT_2:sch 3(E3);
take
c
1
;
let c
2 be
Element of F
1();
let c
3 be
Element of F
2();
reconsider c
4 =
[c2,c3] as
Element of
[:F1(),F2():] by ZFMISC_1:def 2;
P
1[c
2,c
3,c
1 . c
4]
by E4;
hence
P
1[c
2,c
3,c
1 . c
2,c
3]
;
end;
scheme :: BINOP_1:sch 4
s4{ F
1()
-> non
empty set , F
2()
-> non
empty set , F
3()
-> non
empty set , F
4(
Element of F
1(),
Element of F
2())
-> Element of F
3() } :
provided
proof
defpred S
1[
Element of F
1(),
Element of F
2(),
set ] means a
3 = F
4(a
1,a
2);
E2:
for b
1 being
Element of F
1()
for b
2 being
Element of F
2() holds
ex b
3 being
Element of F
3() st
S
1[b
1,b
2,b
3]
;
thus
ex b
1 being
Function of
[:F1(),F2():],F
3() st
for b
2 being
Element of F
1()
for b
3 being
Element of F
2() holds
S
1[b
2,b
3,b
1 . b
2,b
3]
from BINOP_1:sch 3(E2);
end;
definition
let c
1 be
set ;
let c
2 be
BinOp of c
1;
attr a
2 is
commutative means :
E2:
:: BINOP_1:def 2
for b
1, b
2 being
Element of a
1 holds a
2 . b
1,b
2 = a
2 . b
2,b
1;
attr a
2 is
associative means :
E3:
:: BINOP_1:def 3
for b
1, b
2, b
3 being
Element of a
1 holds a
2 . b
1,
(a2 . b2,b3) = a
2 . (a2 . b1,b2),b
3;
attr a
2 is
idempotent means :
E4:
:: BINOP_1:def 4
for b
1 being
Element of a
1 holds a
2 . b
1,b
1 = b
1;
end;
:: deftheorem E2 defines commutative BINOP_1:def 2 :
:: deftheorem E3 defines associative BINOP_1:def 3 :
for b
1 being
set for b
2 being
BinOp of b
1 holds
( b
2 is
associative iff for b
3, b
4, b
5 being
Element of b
1 holds b
2 . b
3,
(b2 . b4,b5) = b
2 . (b2 . b3,b4),b
5 );
:: deftheorem E4 defines idempotent BINOP_1:def 4 :
registration
cluster -> empty commutative associative M4(
[:{} ,{} :],
{} );
coherence
for b1 being BinOp of {} holds
( b1 is empty & b1 is associative & b1 is commutative )
proof
let c
1 be
BinOp of
{} ;
E5:
[:{} ,{} :] = {}
by ZFMISC_1:113;
then E6:
( c
1 c= [:(dom c1),(rng c1):] &
dom c
1 = {} &
rng c
1 c= {} )
by FUNCT_2:def 1, RELAT_1:21, RELSET_1:12;
thus
c
1 is
empty
by E5, XBOOLE_1:3;
let c
2, c
3 be
Element of
{} ;
:: according to BINOP_1:def 2
thus c
1 . c
2,c
3 =
{}
by E6, FUNCT_1:def 4
.=
c
1 . c
3,c
2
by E6, FUNCT_1:def 4
;
end;
end;
:: deftheorem E5 defines is_a_left_unity_wrt BINOP_1:def 5 :
:: deftheorem E6 defines is_a_right_unity_wrt BINOP_1:def 6 :
:: deftheorem defines is_a_unity_wrt BINOP_1:def 7 :
theorem :: BINOP_1:3
canceled;
theorem :: BINOP_1:4
canceled;
theorem :: BINOP_1:5
canceled;
theorem :: BINOP_1:6
canceled;
theorem :: BINOP_1:7
canceled;
theorem :: BINOP_1:8
canceled;
theorem :: BINOP_1:9
canceled;
theorem :: BINOP_1:10
canceled;
theorem E7: :: BINOP_1:11
theorem E8: :: BINOP_1:12
proof
let c
1 be
set ;
let c
2 be
BinOp of c
1;
let c
3 be
Element of c
1;
assume E9:
c
2 is
commutative
;
now
thus
( ( for b
1 being
Element of c
1 holds
( c
2 . c
3,b
1 = b
1 & c
2 . b
1,c
3 = b
1 ) ) implies for b
1 being
Element of c
1 holds c
2 . c
3,b
1 = b
1 )
;
assume E10:
for b
1 being
Element of c
1 holds c
2 . c
3,b
1 = b
1
;
let c
4 be
Element of c
1;
thus
c
2 . c
3,c
4 = c
4
by E10;
thus c
2 . c
4,c
3 =
c
2 . c
3,c
4
by E9, E2
.=
c
4
by E10
;
end;
hence
( c
3 is_a_unity_wrt c
2 iff for b
1 being
Element of c
1 holds c
2 . c
3,b
1 = b
1 )
by E7;
end;
theorem E9: :: BINOP_1:13
proof
let c
1 be
set ;
let c
2 be
BinOp of c
1;
let c
3 be
Element of c
1;
assume E10:
c
2 is
commutative
;
now
thus
( ( for b
1 being
Element of c
1 holds
( c
2 . c
3,b
1 = b
1 & c
2 . b
1,c
3 = b
1 ) ) implies for b
1 being
Element of c
1 holds c
2 . b
1,c
3 = b
1 )
;
assume E11:
for b
1 being
Element of c
1 holds c
2 . b
1,c
3 = b
1
;
let c
4 be
Element of c
1;
thus c
2 . c
3,c
4 =
c
2 . c
4,c
3
by E10, E2
.=
c
4
by E11
;
thus
c
2 . c
4,c
3 = c
4
by E11;
end;
hence
( c
3 is_a_unity_wrt c
2 iff for b
1 being
Element of c
1 holds c
2 . b
1,c
3 = b
1 )
by E7;
end;
theorem E10: :: BINOP_1:14
theorem E11: :: BINOP_1:15
theorem :: BINOP_1:16
theorem E12: :: BINOP_1:17
theorem E13: :: BINOP_1:18
:: deftheorem defines the_unity_wrt BINOP_1:def 8 :
definition
let c
1 be
set ;
let c
2, c
3 be
BinOp of c
1;
pred c
2 is_left_distributive_wrt c
3 means :
E14:
:: BINOP_1:def 9
for b
1, b
2, b
3 being
Element of a
1 holds a
2 . b
1,
(a3 . b2,b3) = a
3 . (a2 . b1,b2),
(a2 . b1,b3);
pred c
2 is_right_distributive_wrt c
3 means :
E15:
:: BINOP_1:def 10
for b
1, b
2, b
3 being
Element of a
1 holds a
2 . (a3 . b1,b2),b
3 = a
3 . (a2 . b1,b3),
(a2 . b2,b3);
end;
:: deftheorem E14 defines is_left_distributive_wrt BINOP_1:def 9 :
:: deftheorem E15 defines is_right_distributive_wrt BINOP_1:def 10 :
:: deftheorem defines is_distributive_wrt BINOP_1:def 11 :
theorem :: BINOP_1:19
canceled;
theorem :: BINOP_1:20
canceled;
theorem :: BINOP_1:21
canceled;
theorem :: BINOP_1:22
canceled;
theorem E16: :: BINOP_1:23
for b
1 being
set for b
2, b
3 being
BinOp of b
1 holds
( b
2 is_distributive_wrt b
3 iff for b
4, b
5, b
6 being
Element of b
1 holds
( b
2 . b
4,
(b3 . b5,b6) = b
3 . (b2 . b4,b5),
(b2 . b4,b6) & b
2 . (b3 . b4,b5),b
6 = b
3 . (b2 . b4,b6),
(b2 . b5,b6) ) )
proof
let c
1 be
set ;
let c
2, c
3 be
BinOp of c
1;
thus
( c
2 is_distributive_wrt c
3 implies for b
1, b
2, b
3 being
Element of c
1 holds
( c
2 . b
1,
(c3 . b2,b3) = c
3 . (c2 . b1,b2),
(c2 . b1,b3) & c
2 . (c3 . b1,b2),b
3 = c
3 . (c2 . b1,b3),
(c2 . b2,b3) ) )
proof
assume
( c
2 is_left_distributive_wrt c
3 & c
2 is_right_distributive_wrt c
3 )
;
:: according to BINOP_1:def 11
hence
for b
1, b
2, b
3 being
Element of c
1 holds
( c
2 . b
1,
(c3 . b2,b3) = c
3 . (c2 . b1,b2),
(c2 . b1,b3) & c
2 . (c3 . b1,b2),b
3 = c
3 . (c2 . b1,b3),
(c2 . b2,b3) )
by E14, E15;
end;
assume
for b
1, b
2, b
3 being
Element of c
1 holds
( c
2 . b
1,
(c3 . b2,b3) = c
3 . (c2 . b1,b2),
(c2 . b1,b3) & c
2 . (c3 . b1,b2),b
3 = c
3 . (c2 . b1,b3),
(c2 . b2,b3) )
;
hence
( ( for b
1, b
2, b
3 being
Element of c
1 holds c
2 . b
1,
(c3 . b2,b3) = c
3 . (c2 . b1,b2),
(c2 . b1,b3) ) & ( for b
1, b
2, b
3 being
Element of c
1 holds c
2 . (c3 . b1,b2),b
3 = c
3 . (c2 . b1,b3),
(c2 . b2,b3) ) )
;
:: according to BINOP_1:def 9,
BINOP_1:def 10,
BINOP_1:def 11
end;
theorem E17: :: BINOP_1:24
proof
let c
1 be non
empty set ;
let c
2, c
3 be
BinOp of c
1;
assume E18:
c
3 is
commutative
;
( ( for b
1, b
2, b
3 being
Element of c
1 holds
( c
3 . b
1,
(c2 . b2,b3) = c
2 . (c3 . b1,b2),
(c3 . b1,b3) & c
3 . (c2 . b1,b2),b
3 = c
2 . (c3 . b1,b3),
(c3 . b2,b3) ) ) iff for b
1, b
2, b
3 being
Element of c
1 holds c
3 . b
1,
(c2 . b2,b3) = c
2 . (c3 . b1,b2),
(c3 . b1,b3) )
proof
thus
( ( for b
1, b
2, b
3 being
Element of c
1 holds
( c
3 . b
1,
(c2 . b2,b3) = c
2 . (c3 . b1,b2),
(c3 . b1,b3) & c
3 . (c2 . b1,b2),b
3 = c
2 . (c3 . b1,b3),
(c3 . b2,b3) ) ) implies for b
1, b
2, b
3 being
Element of c
1 holds c
3 . b
1,
(c2 . b2,b3) = c
2 . (c3 . b1,b2),
(c3 . b1,b3) )
;
assume E19:
for b
1, b
2, b
3 being
Element of c
1 holds c
3 . b
1,
(c2 . b2,b3) = c
2 . (c3 . b1,b2),
(c3 . b1,b3)
;
let c
4, c
5, c
6 be
Element of c
1;
thus
c
3 . c
4,
(c2 . c5,c6) = c
2 . (c3 . c4,c5),
(c3 . c4,c6)
by E19;
thus c
3 . (c2 . c4,c5),c
6 =
c
3 . c
6,
(c2 . c4,c5)
by E18, E2
.=
c
2 . (c3 . c6,c4),
(c3 . c6,c5)
by E19
.=
c
2 . (c3 . c4,c6),
(c3 . c6,c5)
by E18, E2
.=
c
2 . (c3 . c4,c6),
(c3 . c5,c6)
by E18, E2
;
end;
hence
( c
3 is_distributive_wrt c
2 iff for b
1, b
2, b
3 being
Element of c
1 holds c
3 . b
1,
(c2 . b2,b3) = c
2 . (c3 . b1,b2),
(c3 . b1,b3) )
by E16;
end;
theorem E18: :: BINOP_1:25
proof
let c
1 be non
empty set ;
let c
2, c
3 be
BinOp of c
1;
assume E19:
c
3 is
commutative
;
( ( for b
1, b
2, b
3 being
Element of c
1 holds
( c
3 . b
1,
(c2 . b2,b3) = c
2 . (c3 . b1,b2),
(c3 . b1,b3) & c
3 . (c2 . b1,b2),b
3 = c
2 . (c3 . b1,b3),
(c3 . b2,b3) ) ) iff for b
1, b
2, b
3 being
Element of c
1 holds c
3 . (c2 . b1,b2),b
3 = c
2 . (c3 . b1,b3),
(c3 . b2,b3) )
proof
thus
( ( for b
1, b
2, b
3 being
Element of c
1 holds
( c
3 . b
1,
(c2 . b2,b3) = c
2 . (c3 . b1,b2),
(c3 . b1,b3) & c
3 . (c2 . b1,b2),b
3 = c
2 . (c3 . b1,b3),
(c3 . b2,b3) ) ) implies for b
1, b
2, b
3 being
Element of c
1 holds c
3 . (c2 . b1,b2),b
3 = c
2 . (c3 . b1,b3),
(c3 . b2,b3) )
;
assume E20:
for b
1, b
2, b
3 being
Element of c
1 holds c
3 . (c2 . b1,b2),b
3 = c
2 . (c3 . b1,b3),
(c3 . b2,b3)
;
let c
4, c
5, c
6 be
Element of c
1;
thus c
3 . c
4,
(c2 . c5,c6) =
c
3 . (c2 . c5,c6),c
4
by E19, E2
.=
c
2 . (c3 . c5,c4),
(c3 . c6,c4)
by E20
.=
c
2 . (c3 . c4,c5),
(c3 . c6,c4)
by E19, E2
.=
c
2 . (c3 . c4,c5),
(c3 . c4,c6)
by E19, E2
;
thus
c
3 . (c2 . c4,c5),c
6 = c
2 . (c3 . c4,c6),
(c3 . c5,c6)
by E20;
end;
hence
( c
3 is_distributive_wrt c
2 iff for b
1, b
2, b
3 being
Element of c
1 holds c
3 . (c2 . b1,b2),b
3 = c
2 . (c3 . b1,b3),
(c3 . b2,b3) )
by E16;
end;
theorem E19: :: BINOP_1:26
theorem E20: :: BINOP_1:27
theorem :: BINOP_1:28
:: deftheorem E21 defines is_distributive_wrt BINOP_1:def 12 :
definition
let c
1 be non
empty set ;
let c
2 be
BinOp of c
1;
redefine attr a
2 is
commutative means :: BINOP_1:def 13
for b
1, b
2 being
Element of a
1 holds a
2 . b
1,b
2 = a
2 . b
2,b
1;
correctness
compatibility
( c2 is commutative iff for b1, b2 being Element of c1 holds c2 . b1,b2 = c2 . b2,b1 );
by E2;
redefine attr a
2 is
associative means :: BINOP_1:def 14
for b
1, b
2, b
3 being
Element of a
1 holds a
2 . b
1,
(a2 . b2,b3) = a
2 . (a2 . b1,b2),b
3;
correctness
compatibility
( c2 is associative iff for b1, b2, b3 being Element of c1 holds c2 . b1,(c2 . b2,b3) = c2 . (c2 . b1,b2),b3 );
by E3;
redefine attr a
2 is
idempotent means :: BINOP_1:def 15
for b
1 being
Element of a
1 holds a
2 . b
1,b
1 = b
1;
correctness
compatibility
( c2 is idempotent iff for b1 being Element of c1 holds c2 . b1,b1 = b1 );
by E4;
end;
:: deftheorem defines commutative BINOP_1:def 13 :
:: deftheorem defines associative BINOP_1:def 14 :
:: deftheorem defines idempotent BINOP_1:def 15 :
:: deftheorem defines is_a_left_unity_wrt BINOP_1:def 16 :
:: deftheorem defines is_a_right_unity_wrt BINOP_1:def 17 :
definition
let c
1 be non
empty set ;
let c
2, c
3 be
BinOp of c
1;
redefine pred c
2 is_left_distributive_wrt c
3 means :: BINOP_1:def 18
for b
1, b
2, b
3 being
Element of a
1 holds a
2 . b
1,
(a3 . b2,b3) = a
3 . (a2 . b1,b2),
(a2 . b1,b3);
correctness
compatibility
( c2 is_left_distributive_wrt c3 iff for b1, b2, b3 being Element of c1 holds c2 . b1,(c3 . b2,b3) = c3 . (c2 . b1,b2),(c2 . b1,b3) );
by E14;
redefine pred c
2 is_right_distributive_wrt c
3 means :: BINOP_1:def 19
for b
1, b
2, b
3 being
Element of a
1 holds a
2 . (a3 . b1,b2),b
3 = a
3 . (a2 . b1,b3),
(a2 . b2,b3);
correctness
compatibility
( c2 is_right_distributive_wrt c3 iff for b1, b2, b3 being Element of c1 holds c2 . (c3 . b1,b2),b3 = c3 . (c2 . b1,b3),(c2 . b2,b3) );
by E15;
end;
:: deftheorem defines is_left_distributive_wrt BINOP_1:def 18 :
:: deftheorem defines is_right_distributive_wrt BINOP_1:def 19 :
:: deftheorem defines is_distributive_wrt BINOP_1:def 20 :
theorem :: BINOP_1:29
for b
1, b
2, b
3, b
4, b
5 being
set for b
6 being
Function of
[:b1,b2:],b
3 holds
( ( b
4 in b
1 & b
5 in b
2 ) implies ( not b
3 <> {} or b
6 . b
4,b
5 in b
3 ) )