let Y be non empty set ; for G being Subset of (PARTITIONS Y)
for a, u being Function of Y,BOOLEAN
for PA being a_partition of Y st u is_independent_of PA,G holds
All ((a 'imp' u),PA,G) = (Ex (a,PA,G)) 'imp' u
let G be Subset of (PARTITIONS Y); for a, u being Function of Y,BOOLEAN
for PA being a_partition of Y st u is_independent_of PA,G holds
All ((a 'imp' u),PA,G) = (Ex (a,PA,G)) 'imp' u
let a, u be Function of Y,BOOLEAN; for PA being a_partition of Y st u is_independent_of PA,G holds
All ((a 'imp' u),PA,G) = (Ex (a,PA,G)) 'imp' u
let PA be a_partition of Y; ( u is_independent_of PA,G implies All ((a 'imp' u),PA,G) = (Ex (a,PA,G)) 'imp' u )
assume A1:
u is_independent_of PA,G
; All ((a 'imp' u),PA,G) = (Ex (a,PA,G)) 'imp' u
A2:
(Ex (a,PA,G)) 'imp' u '<' All ((a 'imp' u),PA,G)
proof
let z be
Element of
Y;
BVFUNC_1:def 12 ( not ((Ex (a,PA,G)) 'imp' u) . z = TRUE or (All ((a 'imp' u),PA,G)) . z = TRUE )
A3:
z in EqClass (
z,
(CompF (PA,G)))
by EQREL_1:def 6;
assume
((Ex (a,PA,G)) 'imp' u) . z = TRUE
;
(All ((a 'imp' u),PA,G)) . z = TRUE
then A4:
('not' ((Ex (a,PA,G)) . z)) 'or' (u . z) = TRUE
by BVFUNC_1:def 8;
A5:
(
'not' ((Ex (a,PA,G)) . z) = TRUE or
'not' ((Ex (a,PA,G)) . z) = FALSE )
by XBOOLEAN:def 3;
hence
(All ((a 'imp' u),PA,G)) . z = TRUE
;
verum
end;
All ((a 'imp' u),PA,G) '<' (Ex (a,PA,G)) 'imp' u
proof
let z be
Element of
Y;
BVFUNC_1:def 12 ( not (All ((a 'imp' u),PA,G)) . z = TRUE or ((Ex (a,PA,G)) 'imp' u) . z = TRUE )
assume A8:
(All ((a 'imp' u),PA,G)) . z = TRUE
;
((Ex (a,PA,G)) 'imp' u) . z = TRUE
A9:
((Ex (a,PA,G)) 'imp' u) . z = ('not' ((Ex (a,PA,G)) . z)) 'or' (u . z)
by BVFUNC_1:def 8;
per cases
( for x being Element of Y st x in EqClass (z,(CompF (PA,G))) holds
u . x = TRUE or ( ex x being Element of Y st
( x in EqClass (z,(CompF (PA,G))) & not u . x = TRUE ) & ex x being Element of Y st
( x in EqClass (z,(CompF (PA,G))) & a . x = TRUE ) ) or ( ex x being Element of Y st
( x in EqClass (z,(CompF (PA,G))) & not u . x = TRUE ) & ( for x being Element of Y holds
( not x in EqClass (z,(CompF (PA,G))) or not a . x = TRUE ) ) ) )
;
suppose A10:
( ex
x being
Element of
Y st
(
x in EqClass (
z,
(CompF (PA,G))) & not
u . x = TRUE ) & ex
x being
Element of
Y st
(
x in EqClass (
z,
(CompF (PA,G))) &
a . x = TRUE ) )
;
((Ex (a,PA,G)) 'imp' u) . z = TRUE then consider x1 being
Element of
Y such that A11:
x1 in EqClass (
z,
(CompF (PA,G)))
and A12:
u . x1 <> TRUE
;
consider x2 being
Element of
Y such that A13:
x2 in EqClass (
z,
(CompF (PA,G)))
and A14:
a . x2 = TRUE
by A10;
A15:
u . x1 = u . x2
by A1, A11, A13, BVFUNC_1:def 15;
(a 'imp' u) . x2 =
('not' (a . x2)) 'or' (u . x2)
by BVFUNC_1:def 8
.=
('not' TRUE) 'or' FALSE
by A12, A14, A15, XBOOLEAN:def 3
.=
FALSE 'or' FALSE
by MARGREL1:11
.=
FALSE
;
hence
((Ex (a,PA,G)) 'imp' u) . z = TRUE
by A8, A13, BVFUNC_1:def 16;
verum end; end;
end;
hence
All ((a 'imp' u),PA,G) = (Ex (a,PA,G)) 'imp' u
by A2, BVFUNC_1:15; verum