let Y be non empty set ; :: thesis:
let G be Subset of (PARTITIONS Y); :: thesis:
assume A1: G is independent ; :: thesis:
let P, Q be Subset of (PARTITIONS Y); :: thesis:
assume that
A2: P c= G and
A3: Q c= G ; :: thesis:

per cases ;

suppose P = {} ; :: thesis:

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:

end;

suppose Q = {} ; :: thesis:

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:

end;

suppose A4: ( P <> {} & Q <> {} ) ; :: thesis:

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:
assume [x,y] in (ERl ('/\' P)) * (ERl ('/\' Q)) ; :: thesis:
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₁( 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₁(p) from FUNCT_2:sch 4();
deffunc H₂( 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₂(p) from FUNCT_2:sch 4();
deffunc H₃( set ) -> set = $1;
A21: for d being Element of G9 holds bool Y meets H₃(d)

proof

let d be Element of G9; :: thesis:
d meets d ;
hence bool Y meets d by XBOOLE_1:63; :: thesis:

end;

consider h9 being Function of G9,(bool Y) such that
A22: for d being Element of G9 holds h9 . d in H₃(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

proof

let d be set ; :: thesis:
assume A26: d in P ; :: thesis:
then reconsider d9 = d as Element of P ;

per cases ;

suppose A27: d in Q ; :: thesis:

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:

end;

suppose not d in Q ; :: thesis:

hence ((h9 +* hP9) +* hQ9) . d = (h9 +* hP9) . d by A23, FUNCT_4:11
.= hP9 . d by A24, A26, FUNCT_4:13 ;
:: thesis:

end;

reconsider FP9 = rng hP9, FQ9 = rng hQ9 as Subset-Family of Y ;
set A9 = Intersect FP9;
set B9 = Intersect FQ9;
for a being set st a in FP9 holds
y in a

proof

let a be set ; :: thesis:
assume a in FP9 ; :: thesis:
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:

end;

then A38: y in Intersect FP9 by SETFAM_1:43;
for a being set st a in FQ9 holds
x in a

proof

let a be set ; :: thesis:
assume a in FQ9 ; :: thesis:
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:

end;

then A41: x in Intersect FQ9 by SETFAM_1:43;
A42: for d being set st d in Q holds
hQ9 . d in d

proof

let d be set ; :: thesis:
assume d in Q ; :: thesis:
then reconsider d = d as Element of Q ;
hQ9 . d = EqClass (x,d) by A20;
hence hQ9 . d in d ; :: thesis:

end;

rng (h9 +* hP9) c= (rng h9) \/ (rng hP9) by FUNCT_4:17;
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

let d be set ; :: thesis:
assume d in P ; :: thesis:
then reconsider d = d as Element of P ;
hP9 . d = EqClass (y,d) by A19;
hence hP9 . d in d ; :: thesis:

end;

for d being set st d in G holds
((h9 +* hP9) +* hQ9) . d in d

proof

let d be set ; :: thesis:
assume A45: d in G ; :: thesis:
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 by A46, XBOOLE_0:def 3;

suppose A47: d in Q ; :: thesis:

then ((h9 +* hP9) +* hQ9) . d = hQ9 . d by A23, FUNCT_4:13;
hence ((h9 +* hP9) +* hQ9) . d in d by A42, A47; :: thesis:

end;

suppose A48: d in P ; :: thesis:

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

end;

suppose A49: d in G \ (P \/ Q) ; :: thesis:

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:

end;

then Intersect F <> {} by A1, A43, BVFUNC_2:def 5;
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

let a be set ; :: thesis:
assume a in FP9 ; :: thesis:
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:

end;

then A54: t in Intersect FP9 by SETFAM_1:43;
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

let a be set ; :: thesis:
assume a in FQ9 ; :: thesis:
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:

end;

then A58: t in Intersect FQ9 by SETFAM_1:43;
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:

end;