let Y be non empty set ; :: thesis: for G being Subset of () st G is independent holds
for P, Q being Subset of () st P c= G & Q c= G holds
(ERl ('/\' P)) * (ERl ('/\' Q)) c= (ERl ('/\' Q)) * (ERl ('/\' P))

let G be Subset of (); :: thesis: ( G is independent implies for P, Q being Subset of () 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 () st P c= G & Q c= G holds
(ERl ('/\' P)) * (ERl ('/\' Q)) c= (ERl ('/\' Q)) * (ERl ('/\' P))

let P, Q be Subset of (); :: 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 <> {} ) ) ;
suppose P = {} ; :: thesis: (ERl ('/\' P)) * (ERl ('/\' Q)) c= (ERl ('/\' Q)) * (ERl ('/\' P))
then P = {} () ;
then (ERl ('/\' Q)) * (ERl ('/\' P)) = (ERl ('/\' Q)) * (ERl (%O Y)) by Th1
.= (ERl ('/\' Q)) * () by PARTIT1:33
.= nabla Y by Th4 ;
hence (ERl ('/\' P)) * (ERl ('/\' Q)) c= (ERl ('/\' Q)) * (ERl ('/\' P)) ; :: thesis: verum
end;
suppose Q = {} ; :: thesis: (ERl ('/\' P)) * (ERl ('/\' Q)) c= (ERl ('/\' Q)) * (ERl ('/\' P))
then Q = {} () ;
then (ERl ('/\' Q)) * (ERl ('/\' P)) = (ERl (%O Y)) * (ERl ('/\' P)) by Th1
.= () * (ERl ('/\' P)) by PARTIT1:33
.= nabla Y by Th4 ;
hence (ERl ('/\' P)) * (ERl ('/\' Q)) c= (ERl ('/\' Q)) * (ERl ('/\' P)) ; :: thesis: verum
end;
suppose A4: ( P <> {} & Q <> {} ) ; :: thesis: (ERl ('/\' P)) * (ERl ('/\' Q)) c= (ERl ('/\' Q)) * (ERl ('/\' P))
then reconsider G9 = G as non empty Subset of () 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 ;
consider B being Subset of Y such that
A10: B in '/\' Q and
A11: z in B and
A12: y in B by ;
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 ;
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 ;
reconsider P = P, Q = Q as non empty Subset of () by A4;
deffunc H1( 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 = H1(p) from deffunc H2( 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 = H2(p) from deffunc H3( set ) -> set = \$1;
A21: for d being Element of G9 holds bool Y meets H3(d)
proof
let d be Element of G9; :: thesis: bool Y meets H3(d)
d meets d ;
hence bool Y meets d by XBOOLE_1:63; :: thesis: verum
end;
consider h9 being Function of G9,(bool Y) such that
A22: for d being Element of G9 holds h9 . d in H3(d) from 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: ( 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 ;
per cases ( d in Q or not d in Q ) ;
suppose A27: d in Q ; :: thesis: ((h9 +* hP9) +* hQ9) . d = hP9 . d
then A28: hQ . d in FQ by ;
then A29: y in hQ . d by ;
A30: z in hQ . d by ;
A31: hQ . d in d by ;
A32: hP . d in FP by ;
then A33: x in hP . d by ;
A34: z in hP . d by ;
A35: hP . d in d by ;
thus ((h9 +* hP9) +* hQ9) . d = hQ9 . d by
.= EqClass (x,d9) by
.= hP . d by
.= EqClass (z,d9) by
.= hQ . d by
.= EqClass (y,d9) by
.= hP9 . d by A19 ; :: thesis: verum
end;
suppose not d in Q ; :: thesis: ((h9 +* hP9) +* hQ9) . d = hP9 . d
hence ((h9 +* hP9) +* hQ9) . d = (h9 +* hP9) . d by
.= hP9 . d by ;
:: thesis: verum
end;
end;
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: ( 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 ;
hence y in a by EQREL_1:def 6; :: thesis: verum
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: ( 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 ;
hence x in a by EQREL_1:def 6; :: thesis: verum
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: ( 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;
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 ;
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
.= ((dom h9) \/ P) \/ Q by
.= (G \/ P) \/ Q by FUNCT_2:def 1
.= G \/ Q by
.= G by ;
A44: for d being set st d in P holds
hP9 . d in d
proof
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;
for d being set st d in G holds
((h9 +* hP9) +* hQ9) . d in d
proof
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
.= (G \ (P \/ Q)) \/ (P \/ Q) by XBOOLE_1:39 ;
then A46: ( d in G \ (P \/ Q) or d in P \/ Q ) by ;
per cases ( d in Q or d in P or d in G \ (P \/ Q) ) by ;
suppose A47: d in Q ; :: thesis: ((h9 +* hP9) +* hQ9) . d in d
then ((h9 +* hP9) +* hQ9) . d = hQ9 . d by ;
hence ((h9 +* hP9) +* hQ9) . d in d by ; :: thesis: verum
end;
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 ; :: thesis: verum
end;
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 ;
then A50: ((h9 +* hP9) +* hQ9) . d = h9 . d by FUNCT_4:11;
d in G by ;
hence ((h9 +* hP9) +* hQ9) . d in d by ; :: thesis: verum
end;
end;
end;
then Intersect F <> {} by ;
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: ( 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 ;
then a in F by ;
hence t in a by ; :: thesis: verum
end;
then A54: t in Intersect FP9 by SETFAM_1:43;
then Intersect FP9 in '/\' P by ;
then A55: [t,y] in ERl ('/\' P) by ;
for a being set st a in FQ9 holds
t in a
proof
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 ;
then a in F by ;
hence t in a by ; :: thesis: verum
end;
then A58: t in Intersect FQ9 by SETFAM_1:43;
then Intersect FQ9 in '/\' Q by ;
then [x,t] in ERl ('/\' Q) by ;
hence [x,y] in (ERl ('/\' Q)) * (ERl ('/\' P)) by ; :: thesis: verum
end;
end;