let Y be non empty set ; :: thesis: for G being Subset of (PARTITIONS Y) st G is independent holds

for P, Q being Subset of (PARTITIONS Y) st P c= G & Q c= G holds

(ERl ('/\' P)) * (ERl ('/\' Q)) c= (ERl ('/\' Q)) * (ERl ('/\' P))

let G be Subset of (PARTITIONS Y); :: thesis: ( G is independent implies for P, Q being Subset of (PARTITIONS Y) st P c= G & Q c= G holds

(ERl ('/\' P)) * (ERl ('/\' Q)) c= (ERl ('/\' Q)) * (ERl ('/\' P)) )

assume A1: G is independent ; :: thesis: for P, Q being Subset of (PARTITIONS Y) st P c= G & Q c= G holds

(ERl ('/\' P)) * (ERl ('/\' Q)) c= (ERl ('/\' Q)) * (ERl ('/\' P))

let P, Q be Subset of (PARTITIONS Y); :: thesis: ( P c= G & Q c= G implies (ERl ('/\' P)) * (ERl ('/\' Q)) c= (ERl ('/\' Q)) * (ERl ('/\' P)) )

assume that

A2: P c= G and

A3: Q c= G ; :: thesis: (ERl ('/\' P)) * (ERl ('/\' Q)) c= (ERl ('/\' Q)) * (ERl ('/\' P))

for P, Q being Subset of (PARTITIONS Y) st P c= G & Q c= G holds

(ERl ('/\' P)) * (ERl ('/\' Q)) c= (ERl ('/\' Q)) * (ERl ('/\' P))

let G be Subset of (PARTITIONS Y); :: thesis: ( G is independent implies for P, Q being Subset of (PARTITIONS Y) st P c= G & Q c= G holds

(ERl ('/\' P)) * (ERl ('/\' Q)) c= (ERl ('/\' Q)) * (ERl ('/\' P)) )

assume A1: G is independent ; :: thesis: for P, Q being Subset of (PARTITIONS Y) st P c= G & Q c= G holds

(ERl ('/\' P)) * (ERl ('/\' Q)) c= (ERl ('/\' Q)) * (ERl ('/\' P))

let P, Q be Subset of (PARTITIONS Y); :: thesis: ( P c= G & Q c= G implies (ERl ('/\' P)) * (ERl ('/\' Q)) c= (ERl ('/\' Q)) * (ERl ('/\' P)) )

assume that

A2: P c= G and

A3: Q c= G ; :: thesis: (ERl ('/\' P)) * (ERl ('/\' Q)) c= (ERl ('/\' Q)) * (ERl ('/\' P))

per cases
( P = {} or Q = {} or ( P <> {} & Q <> {} ) )
;

end;

suppose
P = {}
; :: thesis: (ERl ('/\' P)) * (ERl ('/\' Q)) c= (ERl ('/\' Q)) * (ERl ('/\' P))

then
P = {} (PARTITIONS Y)
;

then (ERl ('/\' Q)) * (ERl ('/\' P)) = (ERl ('/\' Q)) * (ERl (%O Y)) by Th1

.= (ERl ('/\' Q)) * (nabla Y) by PARTIT1:33

.= nabla Y by Th4 ;

hence (ERl ('/\' P)) * (ERl ('/\' Q)) c= (ERl ('/\' Q)) * (ERl ('/\' P)) ; :: thesis: verum

end;then (ERl ('/\' Q)) * (ERl ('/\' P)) = (ERl ('/\' Q)) * (ERl (%O Y)) by Th1

.= (ERl ('/\' Q)) * (nabla Y) by PARTIT1:33

.= nabla Y by Th4 ;

hence (ERl ('/\' P)) * (ERl ('/\' Q)) c= (ERl ('/\' Q)) * (ERl ('/\' P)) ; :: thesis: verum

suppose
Q = {}
; :: thesis: (ERl ('/\' P)) * (ERl ('/\' Q)) c= (ERl ('/\' Q)) * (ERl ('/\' P))

then
Q = {} (PARTITIONS Y)
;

then (ERl ('/\' Q)) * (ERl ('/\' P)) = (ERl (%O Y)) * (ERl ('/\' P)) by Th1

.= (nabla Y) * (ERl ('/\' P)) by PARTIT1:33

.= nabla Y by Th4 ;

hence (ERl ('/\' P)) * (ERl ('/\' Q)) c= (ERl ('/\' Q)) * (ERl ('/\' P)) ; :: thesis: verum

end;then (ERl ('/\' Q)) * (ERl ('/\' P)) = (ERl (%O Y)) * (ERl ('/\' P)) by Th1

.= (nabla Y) * (ERl ('/\' P)) by PARTIT1:33

.= nabla Y by Th4 ;

hence (ERl ('/\' P)) * (ERl ('/\' Q)) c= (ERl ('/\' Q)) * (ERl ('/\' P)) ; :: thesis: verum

suppose A4:
( P <> {} & Q <> {} )
; :: thesis: (ERl ('/\' P)) * (ERl ('/\' Q)) c= (ERl ('/\' Q)) * (ERl ('/\' P))

then reconsider G9 = G as non empty Subset of (PARTITIONS Y) by A2;

let x, y be Element of Y; :: according to RELSET_1:def 1 :: thesis: ( not [x,y] in (ERl ('/\' P)) * (ERl ('/\' Q)) or [x,y] in (ERl ('/\' Q)) * (ERl ('/\' P)) )

assume [x,y] in (ERl ('/\' P)) * (ERl ('/\' Q)) ; :: thesis: [x,y] in (ERl ('/\' Q)) * (ERl ('/\' P))

then consider z being Element of Y such that

A5: [x,z] in ERl ('/\' P) and

A6: [z,y] in ERl ('/\' Q) by RELSET_1:28;

consider A being Subset of Y such that

A7: A in '/\' P and

A8: x in A and

A9: z in A by A5, PARTIT1:def 6;

consider B being Subset of Y such that

A10: B in '/\' Q and

A11: z in B and

A12: y in B by A6, PARTIT1:def 6;

consider hQ being Function, FQ being Subset-Family of Y such that

A13: ( dom hQ = Q & rng hQ = FQ ) and

A14: for d being set st d in Q holds

hQ . d in d and

A15: B = Intersect FQ and

B <> {} by A10, BVFUNC_2:def 1;

consider hP being Function, FP being Subset-Family of Y such that

A16: ( dom hP = P & rng hP = FP ) and

A17: for d being set st d in P holds

hP . d in d and

A18: A = Intersect FP and

A <> {} by A7, BVFUNC_2:def 1;

reconsider P = P, Q = Q as non empty Subset of (PARTITIONS Y) by A4;

deffunc H_{1}( Element of P) -> Element of $1 = EqClass (y,$1);

consider hP9 being Function of P,(bool Y) such that

A19: for p being Element of P holds hP9 . p = H_{1}(p)
from FUNCT_2:sch 4();

deffunc H_{2}( Element of Q) -> Element of $1 = EqClass (x,$1);

consider hQ9 being Function of Q,(bool Y) such that

A20: for p being Element of Q holds hQ9 . p = H_{2}(p)
from FUNCT_2:sch 4();

deffunc H_{3}( set ) -> set = $1;

A21: for d being Element of G9 holds bool Y meets H_{3}(d)

A22: for d being Element of G9 holds h9 . d in H_{3}(d)
from FUNCT_2:sch 10(A21);

set h = (h9 +* hP9) +* hQ9;

A23: dom hQ9 = Q by FUNCT_2:def 1;

A24: dom hP9 = P by FUNCT_2:def 1;

A25: for d being set st d in P holds

((h9 +* hP9) +* hQ9) . d = hP9 . d

set A9 = Intersect FP9;

set B9 = Intersect FQ9;

for a being set st a in FP9 holds

y in a

for a being set st a in FQ9 holds

x in a

A42: for d being set st d in Q holds

hQ9 . d in d

then rng (h9 +* hP9) c= bool Y by XBOOLE_1:1;

then ( rng ((h9 +* hP9) +* hQ9) c= (rng (h9 +* hP9)) \/ (rng hQ9) & (rng (h9 +* hP9)) \/ (rng hQ9) c= bool Y ) by FUNCT_4:17, XBOOLE_1:8;

then reconsider F = rng ((h9 +* hP9) +* hQ9) as Subset-Family of Y by XBOOLE_1:1;

A43: dom ((h9 +* hP9) +* hQ9) = (dom (h9 +* hP9)) \/ Q by A23, FUNCT_4:def 1

.= ((dom h9) \/ P) \/ Q by A24, FUNCT_4:def 1

.= (G \/ P) \/ Q by FUNCT_2:def 1

.= G \/ Q by A2, XBOOLE_1:12

.= G by A3, XBOOLE_1:12 ;

A44: for d being set st d in P holds

hP9 . d in d

((h9 +* hP9) +* hQ9) . d in d

then consider t being Element of Y such that

A51: t in Intersect F by SUBSET_1:4;

for a being set st a in FP9 holds

t in a

then Intersect FP9 in '/\' P by A44, A24, BVFUNC_2:def 1;

then A55: [t,y] in ERl ('/\' P) by A38, A54, PARTIT1:def 6;

for a being set st a in FQ9 holds

t in a

then Intersect FQ9 in '/\' Q by A42, A23, BVFUNC_2:def 1;

then [x,t] in ERl ('/\' Q) by A41, A58, PARTIT1:def 6;

hence [x,y] in (ERl ('/\' Q)) * (ERl ('/\' P)) by A55, RELSET_1:28; :: thesis: verum

end;let x, y be Element of Y; :: according to RELSET_1:def 1 :: thesis: ( not [x,y] in (ERl ('/\' P)) * (ERl ('/\' Q)) or [x,y] in (ERl ('/\' Q)) * (ERl ('/\' P)) )

assume [x,y] in (ERl ('/\' P)) * (ERl ('/\' Q)) ; :: thesis: [x,y] in (ERl ('/\' Q)) * (ERl ('/\' P))

then consider z being Element of Y such that

A5: [x,z] in ERl ('/\' P) and

A6: [z,y] in ERl ('/\' Q) by RELSET_1:28;

consider A being Subset of Y such that

A7: A in '/\' P and

A8: x in A and

A9: z in A by A5, PARTIT1:def 6;

consider B being Subset of Y such that

A10: B in '/\' Q and

A11: z in B and

A12: y in B by A6, PARTIT1:def 6;

consider hQ being Function, FQ being Subset-Family of Y such that

A13: ( dom hQ = Q & rng hQ = FQ ) and

A14: for d being set st d in Q holds

hQ . d in d and

A15: B = Intersect FQ and

B <> {} by A10, BVFUNC_2:def 1;

consider hP being Function, FP being Subset-Family of Y such that

A16: ( dom hP = P & rng hP = FP ) and

A17: for d being set st d in P holds

hP . d in d and

A18: A = Intersect FP and

A <> {} by A7, BVFUNC_2:def 1;

reconsider P = P, Q = Q as non empty Subset of (PARTITIONS Y) by A4;

deffunc H

consider hP9 being Function of P,(bool Y) such that

A19: for p being Element of P holds hP9 . p = H

deffunc H

consider hQ9 being Function of Q,(bool Y) such that

A20: for p being Element of Q holds hQ9 . p = H

deffunc H

A21: for d being Element of G9 holds bool Y meets H

proof

consider h9 being Function of G9,(bool Y) such that
let d be Element of G9; :: thesis: bool Y meets H_{3}(d)

d meets d ;

hence bool Y meets d by XBOOLE_1:63; :: thesis: verum

end;d meets d ;

hence bool Y meets d by XBOOLE_1:63; :: thesis: verum

A22: for d being Element of G9 holds h9 . d in H

set h = (h9 +* hP9) +* hQ9;

A23: dom hQ9 = Q by FUNCT_2:def 1;

A24: dom hP9 = P by FUNCT_2:def 1;

A25: for d being set st d in P holds

((h9 +* hP9) +* hQ9) . d = hP9 . d

proof

reconsider FP9 = rng hP9, FQ9 = rng hQ9 as Subset-Family of Y ;
let d be set ; :: thesis: ( d in P implies ((h9 +* hP9) +* hQ9) . d = hP9 . d )

assume A26: d in P ; :: thesis: ((h9 +* hP9) +* hQ9) . d = hP9 . d

then reconsider d9 = d as Element of P ;

end;assume A26: d in P ; :: thesis: ((h9 +* hP9) +* hQ9) . d = hP9 . d

then reconsider d9 = d as Element of P ;

per cases
( d in Q or not d in Q )
;

end;

suppose A27:
d in Q
; :: thesis: ((h9 +* hP9) +* hQ9) . d = hP9 . d

then A28:
hQ . d in FQ
by A13, FUNCT_1:def 3;

then A29: y in hQ . d by A12, A15, SETFAM_1:43;

A30: z in hQ . d by A11, A15, A28, SETFAM_1:43;

A31: hQ . d in d by A14, A27;

A32: hP . d in FP by A16, A26, FUNCT_1:def 3;

then A33: x in hP . d by A8, A18, SETFAM_1:43;

A34: z in hP . d by A9, A18, A32, SETFAM_1:43;

A35: hP . d in d by A17, A26;

thus ((h9 +* hP9) +* hQ9) . d = hQ9 . d by A23, A27, FUNCT_4:13

.= EqClass (x,d9) by A20, A27

.= hP . d by A35, A33, EQREL_1:def 6

.= EqClass (z,d9) by A35, A34, EQREL_1:def 6

.= hQ . d by A31, A30, EQREL_1:def 6

.= EqClass (y,d9) by A31, A29, EQREL_1:def 6

.= hP9 . d by A19 ; :: thesis: verum

end;then A29: y in hQ . d by A12, A15, SETFAM_1:43;

A30: z in hQ . d by A11, A15, A28, SETFAM_1:43;

A31: hQ . d in d by A14, A27;

A32: hP . d in FP by A16, A26, FUNCT_1:def 3;

then A33: x in hP . d by A8, A18, SETFAM_1:43;

A34: z in hP . d by A9, A18, A32, SETFAM_1:43;

A35: hP . d in d by A17, A26;

thus ((h9 +* hP9) +* hQ9) . d = hQ9 . d by A23, A27, FUNCT_4:13

.= EqClass (x,d9) by A20, A27

.= hP . d by A35, A33, EQREL_1:def 6

.= EqClass (z,d9) by A35, A34, EQREL_1:def 6

.= hQ . d by A31, A30, EQREL_1:def 6

.= EqClass (y,d9) by A31, A29, EQREL_1:def 6

.= hP9 . d by A19 ; :: thesis: verum

set A9 = Intersect FP9;

set B9 = Intersect FQ9;

for a being set st a in FP9 holds

y in a

proof

then A38:
y in Intersect FP9
by SETFAM_1:43;
let a be set ; :: thesis: ( a in FP9 implies y in a )

assume a in FP9 ; :: thesis: y in a

then consider b being object such that

A36: b in dom hP9 and

A37: hP9 . b = a by FUNCT_1:def 3;

reconsider b = b as Element of P by A36;

a = EqClass (y,b) by A19, A37;

hence y in a by EQREL_1:def 6; :: thesis: verum

end;assume a in FP9 ; :: thesis: y in a

then consider b being object such that

A36: b in dom hP9 and

A37: hP9 . b = a by FUNCT_1:def 3;

reconsider b = b as Element of P by A36;

a = EqClass (y,b) by A19, A37;

hence y in a by EQREL_1:def 6; :: thesis: verum

for a being set st a in FQ9 holds

x in a

proof

then A41:
x in Intersect FQ9
by SETFAM_1:43;
let a be set ; :: thesis: ( a in FQ9 implies x in a )

assume a in FQ9 ; :: thesis: x in a

then consider b being object such that

A39: b in dom hQ9 and

A40: hQ9 . b = a by FUNCT_1:def 3;

reconsider b = b as Element of Q by A39;

a = EqClass (x,b) by A20, A40;

hence x in a by EQREL_1:def 6; :: thesis: verum

end;assume a in FQ9 ; :: thesis: x in a

then consider b being object such that

A39: b in dom hQ9 and

A40: hQ9 . b = a by FUNCT_1:def 3;

reconsider b = b as Element of Q by A39;

a = EqClass (x,b) by A20, A40;

hence x in a by EQREL_1:def 6; :: thesis: verum

A42: for d being set st d in Q holds

hQ9 . d in d

proof

rng (h9 +* hP9) c= (rng h9) \/ (rng hP9)
by FUNCT_4:17;
let d be set ; :: thesis: ( d in Q implies hQ9 . d in d )

assume d in Q ; :: thesis: hQ9 . d in d

then reconsider d = d as Element of Q ;

hQ9 . d = EqClass (x,d) by A20;

hence hQ9 . d in d ; :: thesis: verum

end;assume d in Q ; :: thesis: hQ9 . d in d

then reconsider d = d as Element of Q ;

hQ9 . d = EqClass (x,d) by A20;

hence hQ9 . d in d ; :: thesis: verum

then rng (h9 +* hP9) c= bool Y by XBOOLE_1:1;

then ( rng ((h9 +* hP9) +* hQ9) c= (rng (h9 +* hP9)) \/ (rng hQ9) & (rng (h9 +* hP9)) \/ (rng hQ9) c= bool Y ) by FUNCT_4:17, XBOOLE_1:8;

then reconsider F = rng ((h9 +* hP9) +* hQ9) as Subset-Family of Y by XBOOLE_1:1;

A43: dom ((h9 +* hP9) +* hQ9) = (dom (h9 +* hP9)) \/ Q by A23, FUNCT_4:def 1

.= ((dom h9) \/ P) \/ Q by A24, FUNCT_4:def 1

.= (G \/ P) \/ Q by FUNCT_2:def 1

.= G \/ Q by A2, XBOOLE_1:12

.= G by A3, XBOOLE_1:12 ;

A44: for d being set st d in P holds

hP9 . d in d

proof

for d being set st d in G holds
let d be set ; :: thesis: ( d in P implies hP9 . d in d )

assume d in P ; :: thesis: hP9 . d in d

then reconsider d = d as Element of P ;

hP9 . d = EqClass (y,d) by A19;

hence hP9 . d in d ; :: thesis: verum

end;assume d in P ; :: thesis: hP9 . d in d

then reconsider d = d as Element of P ;

hP9 . d = EqClass (y,d) by A19;

hence hP9 . d in d ; :: thesis: verum

((h9 +* hP9) +* hQ9) . d in d

proof

then
Intersect F <> {}
by A1, A43, BVFUNC_2:def 5;
let d be set ; :: thesis: ( d in G implies ((h9 +* hP9) +* hQ9) . d in d )

assume A45: d in G ; :: thesis: ((h9 +* hP9) +* hQ9) . d in d

G = (P \/ Q) \/ G by A2, A3, XBOOLE_1:8, XBOOLE_1:12

.= (G \ (P \/ Q)) \/ (P \/ Q) by XBOOLE_1:39 ;

then A46: ( d in G \ (P \/ Q) or d in P \/ Q ) by A45, XBOOLE_0:def 3;

end;assume A45: d in G ; :: thesis: ((h9 +* hP9) +* hQ9) . d in d

G = (P \/ Q) \/ G by A2, A3, XBOOLE_1:8, XBOOLE_1:12

.= (G \ (P \/ Q)) \/ (P \/ Q) by XBOOLE_1:39 ;

then A46: ( d in G \ (P \/ Q) or d in P \/ Q ) by A45, XBOOLE_0:def 3;

per cases
( d in Q or d in P or d in G \ (P \/ Q) )
by A46, XBOOLE_0:def 3;

end;

suppose A47:
d in Q
; :: thesis: ((h9 +* hP9) +* hQ9) . d in d

then
((h9 +* hP9) +* hQ9) . d = hQ9 . d
by A23, FUNCT_4:13;

hence ((h9 +* hP9) +* hQ9) . d in d by A42, A47; :: thesis: verum

end;hence ((h9 +* hP9) +* hQ9) . d in d by A42, A47; :: thesis: verum

suppose A48:
d in P
; :: thesis: ((h9 +* hP9) +* hQ9) . d in d

then
((h9 +* hP9) +* hQ9) . d = hP9 . d
by A25;

hence ((h9 +* hP9) +* hQ9) . d in d by A44, A48; :: thesis: verum

end;hence ((h9 +* hP9) +* hQ9) . d in d by A44, A48; :: thesis: verum

suppose A49:
d in G \ (P \/ Q)
; :: thesis: ((h9 +* hP9) +* hQ9) . d in d

then
not d in P \/ Q
by XBOOLE_0:def 5;

then ( (h9 +* hP9) +* hQ9 = h9 +* (hP9 +* hQ9) & not d in dom (hP9 +* hQ9) ) by A24, A23, FUNCT_4:14, FUNCT_4:def 1;

then A50: ((h9 +* hP9) +* hQ9) . d = h9 . d by FUNCT_4:11;

d in G by A49, XBOOLE_0:def 5;

hence ((h9 +* hP9) +* hQ9) . d in d by A22, A50; :: thesis: verum

end;then ( (h9 +* hP9) +* hQ9 = h9 +* (hP9 +* hQ9) & not d in dom (hP9 +* hQ9) ) by A24, A23, FUNCT_4:14, FUNCT_4:def 1;

then A50: ((h9 +* hP9) +* hQ9) . d = h9 . d by FUNCT_4:11;

d in G by A49, XBOOLE_0:def 5;

hence ((h9 +* hP9) +* hQ9) . d in d by A22, A50; :: thesis: verum

then consider t being Element of Y such that

A51: t in Intersect F by SUBSET_1:4;

for a being set st a in FP9 holds

t in a

proof

then A54:
t in Intersect FP9
by SETFAM_1:43;
let a be set ; :: thesis: ( a in FP9 implies t in a )

assume a in FP9 ; :: thesis: t in a

then consider b being object such that

A52: b in dom hP9 and

A53: hP9 . b = a by FUNCT_1:def 3;

hP9 . b = ((h9 +* hP9) +* hQ9) . b by A25, A52;

then a in F by A2, A24, A43, A52, A53, FUNCT_1:def 3;

hence t in a by A51, SETFAM_1:43; :: thesis: verum

end;assume a in FP9 ; :: thesis: t in a

then consider b being object such that

A52: b in dom hP9 and

A53: hP9 . b = a by FUNCT_1:def 3;

hP9 . b = ((h9 +* hP9) +* hQ9) . b by A25, A52;

then a in F by A2, A24, A43, A52, A53, FUNCT_1:def 3;

hence t in a by A51, SETFAM_1:43; :: thesis: verum

then Intersect FP9 in '/\' P by A44, A24, BVFUNC_2:def 1;

then A55: [t,y] in ERl ('/\' P) by A38, A54, PARTIT1:def 6;

for a being set st a in FQ9 holds

t in a

proof

then A58:
t in Intersect FQ9
by SETFAM_1:43;
let a be set ; :: thesis: ( a in FQ9 implies t in a )

assume a in FQ9 ; :: thesis: t in a

then consider b being object such that

A56: b in dom hQ9 and

A57: hQ9 . b = a by FUNCT_1:def 3;

reconsider b = b as Element of Q by A56;

hQ9 . b = ((h9 +* hP9) +* hQ9) . b by A56, FUNCT_4:13;

then a in F by A3, A23, A43, A56, A57, FUNCT_1:def 3;

hence t in a by A51, SETFAM_1:43; :: thesis: verum

end;assume a in FQ9 ; :: thesis: t in a

then consider b being object such that

A56: b in dom hQ9 and

A57: hQ9 . b = a by FUNCT_1:def 3;

reconsider b = b as Element of Q by A56;

hQ9 . b = ((h9 +* hP9) +* hQ9) . b by A56, FUNCT_4:13;

then a in F by A3, A23, A43, A56, A57, FUNCT_1:def 3;

hence t in a by A51, SETFAM_1:43; :: thesis: verum

then Intersect FQ9 in '/\' Q by A42, A23, BVFUNC_2:def 1;

then [x,t] in ERl ('/\' Q) by A41, A58, PARTIT1:def 6;

hence [x,y] in (ERl ('/\' Q)) * (ERl ('/\' P)) by A55, RELSET_1:28; :: thesis: verum