let Y be non empty set ; :: thesis: for u being Element of Funcs Y,BOOLEAN
for G being Subset of (PARTITIONS Y)
for PA, PB being a_partition of Y st u is_independent_of PA,G holds
Ex u,PA,G '<' Ex u,PB,G
let u be Element of Funcs Y,BOOLEAN ; :: thesis: for G being Subset of (PARTITIONS Y)
for PA, PB being a_partition of Y st u is_independent_of PA,G holds
Ex u,PA,G '<' Ex u,PB,G
let G be Subset of (PARTITIONS Y); :: thesis: for PA, PB being a_partition of Y st u is_independent_of PA,G holds
Ex u,PA,G '<' Ex u,PB,G
let PA, PB be a_partition of Y; :: thesis: ( u is_independent_of PA,G implies Ex u,PA,G '<' Ex u,PB,G )
assume
u is_independent_of PA,G
; :: thesis: Ex u,PA,G '<' Ex u,PB,G
then A1:
u is_dependent_of CompF PA,G
by BVFUNC_2:def 8;
for z being Element of Y holds ((Ex u,PA,G) 'imp' (Ex u,PB,G)) . z = TRUE
proof
let z be
Element of
Y;
:: thesis: ((Ex u,PA,G) 'imp' (Ex u,PB,G)) . z = TRUE
A2:
(
z in EqClass z,
(CompF PA,G) &
EqClass z,
(CompF PA,G) in CompF PA,
G )
by EQREL_1:def 8;
A3:
(
z in EqClass z,
(CompF PB,G) &
EqClass z,
(CompF PB,G) in CompF PB,
G )
by EQREL_1:def 8;
A4:
((Ex u,PA,G) 'imp' (Ex u,PB,G)) . z = ('not' ((Ex u,PA,G) . z)) 'or' ((Ex u,PB,G) . z)
by BVFUNC_1:def 11;
now per cases
( (Ex u,PB,G) . z = TRUE or (Ex u,PB,G) . z = FALSE )
by XBOOLEAN:def 3;
case
(Ex u,PB,G) . z = FALSE
;
:: thesis: ((Ex u,PA,G) 'imp' (Ex u,PB,G)) . z = TRUE then
u . z <> TRUE
by A3, BVFUNC_1:def 20;
then
for
x being
Element of
Y holds
( not
x in EqClass z,
(CompF PA,G) or not
u . x = TRUE )
by A1, A2, BVFUNC_1:def 18;
then
(B_SUP u,(CompF PA,G)) . z = FALSE
by BVFUNC_1:def 20;
hence
((Ex u,PA,G) 'imp' (Ex u,PB,G)) . z = TRUE
by A4;
:: thesis: verum end;
hence
((Ex u,PA,G) 'imp' (Ex u,PB,G)) . z = TRUE
;
:: thesis: verum
end;
then
(Ex u,PA,G) 'imp' (Ex u,PB,G) = I_el Y
by BVFUNC_1:def 14;
hence
Ex u,PA,G '<' Ex u,PB,G
by BVFUNC_1:19; :: thesis: verum