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