begin
theorem
theorem
theorem
theorem
for
Y being non
empty set for
G being
Subset of
(PARTITIONS Y) for
a,
b being
Element of
Funcs Y,
BOOLEAN for
PA being
a_partition of
Y holds
'not' ((All a,PA,G) '&' (All b,PA,G)) = (Ex ('not' a),PA,G) 'or' (Ex ('not' b),PA,G)
theorem
for
Y being non
empty set for
G being
Subset of
(PARTITIONS Y) for
a,
b being
Element of
Funcs Y,
BOOLEAN for
PA being
a_partition of
Y holds
'not' ((Ex a,PA,G) '&' (Ex b,PA,G)) = (All ('not' a),PA,G) 'or' (All ('not' b),PA,G)
theorem
theorem
theorem
for
Y being non
empty set for
G being
Subset of
(PARTITIONS Y) for
a,
b being
Element of
Funcs Y,
BOOLEAN for
PA being
a_partition of
Y holds
a 'xor' b '<' ('not' ((Ex ('not' a),PA,G) 'xor' (Ex b,PA,G))) 'or' ('not' ((Ex a,PA,G) 'xor' (Ex ('not' b),PA,G)))
theorem
Lm1:
now
let Y be non
empty set ;
for a, b being Element of Funcs Y,BOOLEAN
for G being Subset of (PARTITIONS Y)
for PA being a_partition of Y
for z being Element of Y st (All (a 'or' b),PA,G) . z = TRUE holds
for x being Element of Y st x in EqClass z,(CompF PA,G) holds
(a 'or' b) . x = TRUE let a,
b be
Element of
Funcs Y,
BOOLEAN ;
for G being Subset of (PARTITIONS Y)
for PA being a_partition of Y
for z being Element of Y st (All (a 'or' b),PA,G) . z = TRUE holds
for x being Element of Y st x in EqClass z,(CompF PA,G) holds
(a 'or' b) . x = TRUE let G be
Subset of
(PARTITIONS Y);
for PA being a_partition of Y
for z being Element of Y st (All (a 'or' b),PA,G) . z = TRUE holds
for x being Element of Y st x in EqClass z,(CompF PA,G) holds
(a 'or' b) . x = TRUE let PA be
a_partition of
Y;
for z being Element of Y st (All (a 'or' b),PA,G) . z = TRUE holds
for x being Element of Y st x in EqClass z,(CompF PA,G) holds
(a 'or' b) . x = TRUE let z be
Element of
Y;
( (All (a 'or' b),PA,G) . z = TRUE implies for x being Element of Y st x in EqClass z,(CompF PA,G) holds
(a 'or' b) . x = TRUE )assume A1:
(All (a 'or' b),PA,G) . z = TRUE
;
for x being Element of Y st x in EqClass z,(CompF PA,G) holds
(a 'or' b) . x = TRUE assume
ex
x being
Element of
Y st
(
x in EqClass z,
(CompF PA,G) & not
(a 'or' b) . x = TRUE )
;
contradictionthen
(B_INF (a 'or' b),(CompF PA,G)) . z = FALSE
by BVFUNC_1:def 19;
hence
contradiction
by A1, BVFUNC_2:def 9;
verum
end;
theorem
theorem
theorem
theorem
Lm2:
now
let Y be non
empty set ;
for a, b being Element of Funcs Y,BOOLEAN
for G being Subset of (PARTITIONS Y)
for PA being a_partition of Y
for z being Element of Y st (All (a 'imp' b),PA,G) . z = TRUE holds
for x being Element of Y st x in EqClass z,(CompF PA,G) holds
(a 'imp' b) . x = TRUE let a,
b be
Element of
Funcs Y,
BOOLEAN ;
for G being Subset of (PARTITIONS Y)
for PA being a_partition of Y
for z being Element of Y st (All (a 'imp' b),PA,G) . z = TRUE holds
for x being Element of Y st x in EqClass z,(CompF PA,G) holds
(a 'imp' b) . x = TRUE let G be
Subset of
(PARTITIONS Y);
for PA being a_partition of Y
for z being Element of Y st (All (a 'imp' b),PA,G) . z = TRUE holds
for x being Element of Y st x in EqClass z,(CompF PA,G) holds
(a 'imp' b) . x = TRUE let PA be
a_partition of
Y;
for z being Element of Y st (All (a 'imp' b),PA,G) . z = TRUE holds
for x being Element of Y st x in EqClass z,(CompF PA,G) holds
(a 'imp' b) . x = TRUE let z be
Element of
Y;
( (All (a 'imp' b),PA,G) . z = TRUE implies for x being Element of Y st x in EqClass z,(CompF PA,G) holds
(a 'imp' b) . x = TRUE )assume A1:
(All (a 'imp' b),PA,G) . z = TRUE
;
for x being Element of Y st x in EqClass z,(CompF PA,G) holds
(a 'imp' b) . x = TRUE assume
ex
x being
Element of
Y st
(
x in EqClass z,
(CompF PA,G) & not
(a 'imp' b) . x = TRUE )
;
contradictionthen
(B_INF (a 'imp' b),(CompF PA,G)) . z = FALSE
by BVFUNC_1:def 19;
hence
contradiction
by A1, BVFUNC_2:def 9;
verum
end;
theorem
theorem
theorem
theorem
theorem
theorem
theorem
theorem
theorem
theorem
theorem
for
Y being non
empty set for
G being
Subset of
(PARTITIONS Y) for
a,
b being
Element of
Funcs Y,
BOOLEAN for
PA being
a_partition of
Y holds
(All a,PA,G) 'imp' (All b,PA,G) '<' (All a,PA,G) 'imp' (Ex b,PA,G)
theorem
for
Y being non
empty set for
G being
Subset of
(PARTITIONS Y) for
a,
b being
Element of
Funcs Y,
BOOLEAN for
PA being
a_partition of
Y holds
(Ex a,PA,G) 'imp' (Ex b,PA,G) '<' (All a,PA,G) 'imp' (Ex b,PA,G)
theorem Th26:
theorem
theorem
theorem
theorem
theorem
theorem
theorem
theorem
theorem
theorem
theorem
theorem
for
Y being non
empty set for
G being
Subset of
(PARTITIONS Y) for
c,
b,
a being
Element of
Funcs Y,
BOOLEAN for
PA being
a_partition of
Y holds
((Ex c,PA,G) '&' (All (c 'imp' b),PA,G)) '&' (All (c 'imp' a),PA,G) '<' Ex (a '&' b),
PA,
G
theorem
theorem
for
Y being non
empty set for
G being
Subset of
(PARTITIONS Y) for
b,
c,
a being
Element of
Funcs Y,
BOOLEAN for
PA being
a_partition of
Y holds
((Ex b,PA,G) '&' (All (b 'imp' c),PA,G)) '&' (All (c 'imp' a),PA,G) '<' Ex (a '&' b),
PA,
G
theorem
for
Y being non
empty set for
G being
Subset of
(PARTITIONS Y) for
c,
b,
a being
Element of
Funcs Y,
BOOLEAN for
PA being
a_partition of
Y holds
((Ex c,PA,G) '&' (All (b 'imp' ('not' c)),PA,G)) '&' (All (c 'imp' a),PA,G) '<' Ex (a '&' ('not' b)),
PA,
G