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:37
.= 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:37
.= nabla Y by Th4 ;
hence (ERl ('/\' P)) * (ERl ('/\' Q)) c= (ERl ('/\' Q)) * (ERl ('/\' P)) ; :: thesis:

end;

suppose A8: ( 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 2 :: thesis:
assume [x,y] in (ERl ('/\' P)) * (ERl ('/\' Q)) ; :: thesis:
then consider z being Element of Y such that
A9: [x,z] in ERl ('/\' P) and
A10: [z,y] in ERl ('/\' Q) by RELSET_1:51;
consider A being Subset of Y such that
A11: A in '/\' P and
A12: x in A and
A13: z in A by A9, PARTIT1:def 6;
consider B being Subset of Y such that
A14: B in '/\' Q and
A15: z in B and
A16: y in B by A10, PARTIT1:def 6;
consider hQ being Function, FQ being Subset-Family of Y such that
A17: ( dom hQ = Q & rng hQ = FQ ) and
A18: for d being set st d in Q holds
hQ . d in d and
A19: B = Intersect FQ and
B <> {} by A14, BVFUNC_2:def 1;
consider hP being Function, FP being Subset-Family of Y such that
A20: ( dom hP = P & rng hP = FP ) and
A21: for d being set st d in P holds
hP . d in d and
A22: A = Intersect FP and
A <> {} by A11, BVFUNC_2:def 1;
reconsider P = P, Q = Q as non empty Subset of (PARTITIONS Y) by A8;
deffunc H₁( Element of P) -> Element of $1 = EqClass (y,$1);
consider hP9 being Function of P,(bool Y) such that
A23: 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
A24: for p being Element of Q holds hQ9 . p = H₂(p) from FUNCT_2:sch 4();
deffunc H₃( set ) -> set = $1;
A25: 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
A26: for d being Element of G9 holds h9 . d in H₃(d) from FUNCT_2:sch 11(A25);
set h = (h9 +* hP9) +* hQ9;
A27: dom hQ9 = Q by FUNCT_2:def 1;
A28: dom hP9 = P by FUNCT_2:def 1;
A29: for d being set st d in P holds
((h9 +* hP9) +* hQ9) . d = hP9 . d

proof

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

per cases ;

suppose A31: d in Q ; :: thesis:

then A32: hQ . d in FQ by A17, FUNCT_1:def 5;
then A33: y in hQ . d by A16, A19, SETFAM_1:58;
A34: z in hQ . d by A15, A19, A32, SETFAM_1:58;
A35: hQ . d in d by A18, A31;
A36: hP . d in FP by A20, A30, FUNCT_1:def 5;
then A37: x in hP . d by A12, A22, SETFAM_1:58;
A38: z in hP . d by A13, A22, A36, SETFAM_1:58;
A39: hP . d in d by A21, A30;
thus ((h9 +* hP9) +* hQ9) . d = hQ9 . d by A27, A31, FUNCT_4:14
.= EqClass (x,d9) by A24, A31
.= hP . d by A39, A37, EQREL_1:def 8
.= EqClass (z,d9) by A39, A38, EQREL_1:def 8
.= hQ . d by A35, A34, EQREL_1:def 8
.= EqClass (y,d9) by A35, A33, EQREL_1:def 8
.= hP9 . d by A23 ; :: thesis:

end;

suppose not d in Q ; :: thesis:

hence ((h9 +* hP9) +* hQ9) . d = (h9 +* hP9) . d by A27, FUNCT_4:12
.= hP9 . d by A28, A30, FUNCT_4:14 ;
:: 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 set such that
A40: b in dom hP9 and
A41: hP9 . b = a by FUNCT_1:def 5;
reconsider b = b as Element of P by A40;
a = EqClass (y,b) by A23, A41;
hence y in a by EQREL_1:def 8; :: thesis:

end;

then A42: y in Intersect FP9 by SETFAM_1:58;
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 set such that
A43: b in dom hQ9 and
A44: hQ9 . b = a by FUNCT_1:def 5;
reconsider b = b as Element of Q by A43;
a = EqClass (x,b) by A24, A44;
hence x in a by EQREL_1:def 8; :: thesis:

end;

then A45: x in Intersect FQ9 by SETFAM_1:58;
A46: 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 A24;
hence hQ9 . d in d ; :: thesis:

end;

rng (h9 +* hP9) c= (rng h9) \/ (rng hP9) by FUNCT_4:18;
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:18, XBOOLE_1:8;
then reconsider F = rng ((h9 +* hP9) +* hQ9) as Subset-Family of Y by XBOOLE_1:1;
A47: dom ((h9 +* hP9) +* hQ9) = (dom (h9 +* hP9)) \/ Q by A27, FUNCT_4:def 1
.= ((dom h9) \/ P) \/ Q by A28, 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 ;
A48: 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 A23;
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 A49: 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 A50: ( d in G \ (P \/ Q) or d in P \/ Q ) by A49, XBOOLE_0:def 3;

per cases by A50, XBOOLE_0:def 3;

suppose A51: d in Q ; :: thesis:

then ((h9 +* hP9) +* hQ9) . d = hQ9 . d by A27, FUNCT_4:14;
hence ((h9 +* hP9) +* hQ9) . d in d by A46, A51; :: thesis:

end;

suppose A52: d in P ; :: thesis:

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

end;

suppose A53: 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 A28, A27, FUNCT_4:15, FUNCT_4:def 1;
then A54: ((h9 +* hP9) +* hQ9) . d = h9 . d by FUNCT_4:12;
d in G by A53, XBOOLE_0:def 5;
hence ((h9 +* hP9) +* hQ9) . d in d by A26, A54; :: thesis:

end;

then Intersect F <> {} by A1, A47, BVFUNC_2:def 5;
then consider t being Element of Y such that
A55: t in Intersect F by SUBSET_1:10;
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 set such that
A56: b in dom hP9 and
A57: hP9 . b = a by FUNCT_1:def 5;
hP9 . b = ((h9 +* hP9) +* hQ9) . b by A29, A56;
then a in F by A2, A28, A47, A56, A57, FUNCT_1:def 5;
hence t in a by A55, SETFAM_1:58; :: thesis:

end;

then A58: t in Intersect FP9 by SETFAM_1:58;
then Intersect FP9 in '/\' P by A48, A28, BVFUNC_2:def 1;
then A59: [t,y] in ERl ('/\' P) by A42, A58, 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 set such that
A60: b in dom hQ9 and
A61: hQ9 . b = a by FUNCT_1:def 5;
reconsider b = b as Element of Q by A60;
hQ9 . b = ((h9 +* hP9) +* hQ9) . b by A60, FUNCT_4:14;
then a in F by A3, A27, A47, A60, A61, FUNCT_1:def 5;
hence t in a by A55, SETFAM_1:58; :: thesis:

end;

then A62: t in Intersect FQ9 by SETFAM_1:58;
then Intersect FQ9 in '/\' Q by A46, A27, BVFUNC_2:def 1;
then [x,t] in ERl ('/\' Q) by A45, A62, PARTIT1:def 6;
hence [x,y] in (ERl ('/\' Q)) * (ERl ('/\' P)) by A59, RELSET_1:51; :: thesis:

end;