let Y be non empty set ; for G being Subset of (PARTITIONS Y)
for a, b being Function of 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))
let G be Subset of (PARTITIONS Y); for a, b being Function of 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))
let a, b be Function of 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))
let PA be a_partition of Y; 'not' ((Ex (a,PA,G)) '&' (Ex (b,PA,G))) = (All (('not' a),PA,G)) 'or' (All (('not' b),PA,G))
A1:
All (('not' b),PA,G) = B_INF (('not' b),(CompF (PA,G)))
by BVFUNC_2:def 9;
A2:
Ex (b,PA,G) = B_SUP (b,(CompF (PA,G)))
by BVFUNC_2:def 10;
A3:
Ex (a,PA,G) = B_SUP (a,(CompF (PA,G)))
by BVFUNC_2:def 10;
A4:
(All (('not' a),PA,G)) 'or' (All (('not' b),PA,G)) '<' 'not' ((Ex (a,PA,G)) '&' (Ex (b,PA,G)))
proof
let z be
Element of
Y;
BVFUNC_1:def 12 ( not ((All (('not' a),PA,G)) 'or' (All (('not' b),PA,G))) . z = TRUE or ('not' ((Ex (a,PA,G)) '&' (Ex (b,PA,G)))) . z = TRUE )
A5:
(
(All (('not' b),PA,G)) . z = TRUE or
(All (('not' b),PA,G)) . z = FALSE )
by XBOOLEAN:def 3;
assume
((All (('not' a),PA,G)) 'or' (All (('not' b),PA,G))) . z = TRUE
;
('not' ((Ex (a,PA,G)) '&' (Ex (b,PA,G)))) . z = TRUE
then A6:
((All (('not' a),PA,G)) . z) 'or' ((All (('not' b),PA,G)) . z) = TRUE
by BVFUNC_1:def 4;
per cases
( (All (('not' a),PA,G)) . z = TRUE or (All (('not' b),PA,G)) . z = TRUE )
by A6, A5, BINARITH:3;
suppose A7:
(All (('not' a),PA,G)) . z = TRUE
;
('not' ((Ex (a,PA,G)) '&' (Ex (b,PA,G)))) . z = TRUE thus ('not' ((Ex (a,PA,G)) '&' (Ex (b,PA,G)))) . z =
'not' (((Ex (a,PA,G)) '&' (Ex (b,PA,G))) . z)
by MARGREL1:def 19
.=
'not' (((Ex (a,PA,G)) . z) '&' ((Ex (b,PA,G)) . z))
by MARGREL1:def 20
.=
'not' (FALSE '&' ((Ex (b,PA,G)) . z))
by A3, A9, BVFUNC_1:def 17
.=
'not' FALSE
by MARGREL1:12
.=
TRUE
by MARGREL1:11
;
verum end; suppose A10:
(All (('not' b),PA,G)) . z = TRUE
;
('not' ((Ex (a,PA,G)) '&' (Ex (b,PA,G)))) . z = TRUE thus ('not' ((Ex (a,PA,G)) '&' (Ex (b,PA,G)))) . z =
'not' (((Ex (a,PA,G)) '&' (Ex (b,PA,G))) . z)
by MARGREL1:def 19
.=
'not' (((Ex (a,PA,G)) . z) '&' ((Ex (b,PA,G)) . z))
by MARGREL1:def 20
.=
'not' (((Ex (a,PA,G)) . z) '&' FALSE)
by A2, A12, BVFUNC_1:def 17
.=
'not' FALSE
by MARGREL1:12
.=
TRUE
by MARGREL1:11
;
verum end; end;
end;
A13:
All (('not' a),PA,G) = B_INF (('not' a),(CompF (PA,G)))
by BVFUNC_2:def 9;
'not' ((Ex (a,PA,G)) '&' (Ex (b,PA,G))) '<' (All (('not' a),PA,G)) 'or' (All (('not' b),PA,G))
proof
let z be
Element of
Y;
BVFUNC_1:def 12 ( not ('not' ((Ex (a,PA,G)) '&' (Ex (b,PA,G)))) . z = TRUE or ((All (('not' a),PA,G)) 'or' (All (('not' b),PA,G))) . z = TRUE )
assume
('not' ((Ex (a,PA,G)) '&' (Ex (b,PA,G)))) . z = TRUE
;
((All (('not' a),PA,G)) 'or' (All (('not' b),PA,G))) . z = TRUE
then
'not' (((Ex (a,PA,G)) '&' (Ex (b,PA,G))) . z) = TRUE
by MARGREL1:def 19;
then
((Ex (a,PA,G)) '&' (Ex (b,PA,G))) . z = FALSE
by MARGREL1:11;
then A14:
((Ex (a,PA,G)) . z) '&' ((Ex (b,PA,G)) . z) = FALSE
by MARGREL1:def 20;
per cases
( (Ex (a,PA,G)) . z = FALSE or (Ex (b,PA,G)) . z = FALSE )
by A14, MARGREL1:12;
suppose A15:
(Ex (a,PA,G)) . z = FALSE
;
((All (('not' a),PA,G)) 'or' (All (('not' b),PA,G))) . z = TRUE thus ((All (('not' a),PA,G)) 'or' (All (('not' b),PA,G))) . z =
((All (('not' a),PA,G)) . z) 'or' ((All (('not' b),PA,G)) . z)
by BVFUNC_1:def 4
.=
TRUE 'or' ((All (('not' b),PA,G)) . z)
by A13, A16, BVFUNC_1:def 16
.=
TRUE
by BINARITH:10
;
verum end; suppose A17:
(Ex (b,PA,G)) . z = FALSE
;
((All (('not' a),PA,G)) 'or' (All (('not' b),PA,G))) . z = TRUE thus ((All (('not' a),PA,G)) 'or' (All (('not' b),PA,G))) . z =
((All (('not' a),PA,G)) . z) 'or' ((All (('not' b),PA,G)) . z)
by BVFUNC_1:def 4
.=
((All (('not' a),PA,G)) . z) 'or' TRUE
by A1, A18, BVFUNC_1:def 16
.=
TRUE
by BINARITH:10
;
verum end; end;
end;
hence
'not' ((Ex (a,PA,G)) '&' (Ex (b,PA,G))) = (All (('not' a),PA,G)) 'or' (All (('not' b),PA,G))
by A4, BVFUNC_1:15; verum