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 'or' u),PA,G) '<' (Ex (a,PA,G)) 'or' 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 'or' u),PA,G) '<' (Ex (a,PA,G)) 'or' 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 'or' u),PA,G) '<' (Ex (a,PA,G)) 'or' u
let PA be a_partition of Y; ( u is_independent_of PA,G implies All ((a 'or' u),PA,G) '<' (Ex (a,PA,G)) 'or' u )
assume A1:
u is_independent_of PA,G
; All ((a 'or' u),PA,G) '<' (Ex (a,PA,G)) 'or' u
let z be Element of Y; BVFUNC_1:def 12 ( not (All ((a 'or' u),PA,G)) . z = TRUE or ((Ex (a,PA,G)) 'or' u) . z = TRUE )
assume A2:
(All ((a 'or' u),PA,G)) . z = TRUE
; ((Ex (a,PA,G)) 'or' u) . z = TRUE
A3:
for x being Element of Y holds
( not x in EqClass (z,(CompF (PA,G))) or a . x = TRUE or u . x = TRUE )
A5:
((Ex (a,PA,G)) 'or' u) . z = ((Ex (a,PA,G)) . z) 'or' (u . z)
by BVFUNC_1:def 4;
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 A6:
( 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 ) ) )
;
((Ex (a,PA,G)) 'or' u) . z = TRUE A7:
z in EqClass (
z,
(CompF (PA,G)))
by EQREL_1:def 6;
A8:
a . z <> TRUE
by A6, EQREL_1:def 6;
consider x1 being
Element of
Y such that A9:
x1 in EqClass (
z,
(CompF (PA,G)))
and A10:
u . x1 <> TRUE
by A6;
u . x1 = u . z
by A1, A7, A9, BVFUNC_1:def 15;
hence
((Ex (a,PA,G)) 'or' u) . z = TRUE
by A3, A8, A10, EQREL_1:def 6;
verum end; end;