let Y be non empty set ; for a being Function of Y,BOOLEAN
for G being Subset of (PARTITIONS Y)
for P, Q being a_partition of Y st G is independent holds
All ((All (a,P,G)),Q,G) = All ((All (a,Q,G)),P,G)
let a be Function of Y,BOOLEAN; for G being Subset of (PARTITIONS Y)
for P, Q being a_partition of Y st G is independent holds
All ((All (a,P,G)),Q,G) = All ((All (a,Q,G)),P,G)
let G be Subset of (PARTITIONS Y); for P, Q being a_partition of Y st G is independent holds
All ((All (a,P,G)),Q,G) = All ((All (a,Q,G)),P,G)
let P, Q be a_partition of Y; ( G is independent implies All ((All (a,P,G)),Q,G) = All ((All (a,Q,G)),P,G) )
set A = G \ {P};
set B = G \ {Q};
A1:
CompF (P,G) = '/\' (G \ {P})
by BVFUNC_2:def 7;
A2:
( G \ {P} c= G & G \ {Q} c= G )
by XBOOLE_1:36;
A3:
CompF (Q,G) = '/\' (G \ {Q})
by BVFUNC_2:def 7;
assume
G is independent
; All ((All (a,P,G)),Q,G) = All ((All (a,Q,G)),P,G)
then A4:
(ERl ('/\' (G \ {P}))) * (ERl ('/\' (G \ {Q}))) = (ERl ('/\' (G \ {Q}))) * (ERl ('/\' (G \ {P})))
by A2, Th14;
A5:
for y being Element of Y holds
( ( ( for x being Element of Y st x in EqClass (y,(CompF (Q,G))) holds
(B_INF (a,(CompF (P,G)))) . x = TRUE ) implies (B_INF ((B_INF (a,(CompF (Q,G)))),(CompF (P,G)))) . y = TRUE ) & ( ex x being Element of Y st
( x in EqClass (y,(CompF (Q,G))) & not (B_INF (a,(CompF (P,G)))) . x = TRUE ) implies (B_INF ((B_INF (a,(CompF (Q,G)))),(CompF (P,G)))) . y = FALSE ) )
proof
let y be
Element of
Y;
( ( ( for x being Element of Y st x in EqClass (y,(CompF (Q,G))) holds
(B_INF (a,(CompF (P,G)))) . x = TRUE ) implies (B_INF ((B_INF (a,(CompF (Q,G)))),(CompF (P,G)))) . y = TRUE ) & ( ex x being Element of Y st
( x in EqClass (y,(CompF (Q,G))) & not (B_INF (a,(CompF (P,G)))) . x = TRUE ) implies (B_INF ((B_INF (a,(CompF (Q,G)))),(CompF (P,G)))) . y = FALSE ) )
hereby ( ex x being Element of Y st
( x in EqClass (y,(CompF (Q,G))) & not (B_INF (a,(CompF (P,G)))) . x = TRUE ) implies (B_INF ((B_INF (a,(CompF (Q,G)))),(CompF (P,G)))) . y = FALSE )
assume A6:
for
x being
Element of
Y st
x in EqClass (
y,
(CompF (Q,G))) holds
(B_INF (a,(CompF (P,G)))) . x = TRUE
;
(B_INF ((B_INF (a,(CompF (Q,G)))),(CompF (P,G)))) . y = TRUE
for
x being
Element of
Y st
x in EqClass (
y,
(CompF (P,G))) holds
(B_INF (a,(CompF (Q,G)))) . x = TRUE
proof
let x be
Element of
Y;
( x in EqClass (y,(CompF (P,G))) implies (B_INF (a,(CompF (Q,G)))) . x = TRUE )
assume
x in EqClass (
y,
(CompF (P,G)))
;
(B_INF (a,(CompF (Q,G)))) . x = TRUE
then A7:
[x,y] in ERl ('/\' (G \ {P}))
by A1, Th5;
for
z being
Element of
Y st
z in EqClass (
x,
(CompF (Q,G))) holds
a . z = TRUE
proof
let z be
Element of
Y;
( z in EqClass (x,(CompF (Q,G))) implies a . z = TRUE )
assume
z in EqClass (
x,
(CompF (Q,G)))
;
a . z = TRUE
then
[z,x] in ERl ('/\' (G \ {Q}))
by A3, Th5;
then
[z,y] in (ERl ('/\' (G \ {P}))) * (ERl ('/\' (G \ {Q})))
by A4, A7, RELAT_1:def 8;
then consider u being
object such that A8:
[z,u] in ERl ('/\' (G \ {P}))
and A9:
[u,y] in ERl ('/\' (G \ {Q}))
by RELAT_1:def 8;
u in field (ERl ('/\' (G \ {Q})))
by A9, RELAT_1:15;
then reconsider u =
u as
Element of
Y by ORDERS_1:12;
u in EqClass (
y,
(CompF (Q,G)))
by A3, A9, Th5;
then A10:
(B_INF (a,(CompF (P,G)))) . u <> FALSE
by A6;
z in EqClass (
u,
(CompF (P,G)))
by A1, A8, Th5;
hence
a . z = TRUE
by A10, BVFUNC_1:def 16;
verum
end;
hence
(B_INF (a,(CompF (Q,G)))) . x = TRUE
by BVFUNC_1:def 16;
verum
end; hence
(B_INF ((B_INF (a,(CompF (Q,G)))),(CompF (P,G)))) . y = TRUE
by BVFUNC_1:def 16;
verum
end;
given x being
Element of
Y such that A11:
x in EqClass (
y,
(CompF (Q,G)))
and A12:
(B_INF (a,(CompF (P,G)))) . x <> TRUE
;
(B_INF ((B_INF (a,(CompF (Q,G)))),(CompF (P,G)))) . y = FALSE
consider z being
Element of
Y such that A13:
z in EqClass (
x,
(CompF (P,G)))
and A14:
a . z <> TRUE
by A12, BVFUNC_1:def 16;
A15:
[x,y] in ERl ('/\' (G \ {Q}))
by A3, A11, Th5;
[z,x] in ERl ('/\' (G \ {P}))
by A1, A13, Th5;
then
[z,y] in (ERl ('/\' (G \ {Q}))) * (ERl ('/\' (G \ {P})))
by A4, A15, RELAT_1:def 8;
then consider u being
object such that A16:
[z,u] in ERl ('/\' (G \ {Q}))
and A17:
[u,y] in ERl ('/\' (G \ {P}))
by RELAT_1:def 8;
u in field (ERl ('/\' (G \ {Q})))
by A16, RELAT_1:15;
then reconsider u =
u as
Element of
Y by ORDERS_1:12;
z in EqClass (
u,
(CompF (Q,G)))
by A3, A16, Th5;
then A18:
(B_INF (a,(CompF (Q,G)))) . u = FALSE
by A14, BVFUNC_1:def 16;
u in EqClass (
y,
(CompF (P,G)))
by A1, A17, Th5;
hence
(B_INF ((B_INF (a,(CompF (Q,G)))),(CompF (P,G)))) . y = FALSE
by A18, BVFUNC_1:def 16;
verum
end;
thus All ((All (a,P,G)),Q,G) =
B_INF ((All (a,P,G)),(CompF (Q,G)))
by BVFUNC_2:def 9
.=
B_INF ((B_INF (a,(CompF (P,G)))),(CompF (Q,G)))
by BVFUNC_2:def 9
.=
B_INF ((B_INF (a,(CompF (Q,G)))),(CompF (P,G)))
by A5, BVFUNC_1:def 16
.=
B_INF ((All (a,Q,G)),(CompF (P,G)))
by BVFUNC_2:def 9
.=
All ((All (a,Q,G)),P,G)
by BVFUNC_2:def 9
; verum