let Y be non empty set ; :: thesis: for G being Subset of (PARTITIONS Y)
for A, B, C, D, E, F, J, M being a_partition of Y st G = {A,B,C,D,E,F,J,M} & A <> B & A <> C & A <> D & A <> E & A <> F & A <> J & A <> M & B <> C & B <> D & B <> E & B <> F & B <> J & B <> M & C <> D & C <> E & C <> F & C <> J & C <> M & D <> E & D <> F & D <> J & D <> M & E <> F & E <> J & E <> M & F <> J & F <> M & J <> M holds
CompF (A,G) = (((((B '/\' C) '/\' D) '/\' E) '/\' F) '/\' J) '/\' M
let G be Subset of (PARTITIONS Y); :: thesis: for A, B, C, D, E, F, J, M being a_partition of Y st G = {A,B,C,D,E,F,J,M} & A <> B & A <> C & A <> D & A <> E & A <> F & A <> J & A <> M & B <> C & B <> D & B <> E & B <> F & B <> J & B <> M & C <> D & C <> E & C <> F & C <> J & C <> M & D <> E & D <> F & D <> J & D <> M & E <> F & E <> J & E <> M & F <> J & F <> M & J <> M holds
CompF (A,G) = (((((B '/\' C) '/\' D) '/\' E) '/\' F) '/\' J) '/\' M
let A, B, C, D, E, F, J, M be a_partition of Y; :: thesis: ( G = {A,B,C,D,E,F,J,M} & A <> B & A <> C & A <> D & A <> E & A <> F & A <> J & A <> M & B <> C & B <> D & B <> E & B <> F & B <> J & B <> M & C <> D & C <> E & C <> F & C <> J & C <> M & D <> E & D <> F & D <> J & D <> M & E <> F & E <> J & E <> M & F <> J & F <> M & J <> M implies CompF (A,G) = (((((B '/\' C) '/\' D) '/\' E) '/\' F) '/\' J) '/\' M )
assume that
A1: G = {A,B,C,D,E,F,J,M} and
A2: A <> B and
A3: A <> C and
A4: ( A <> D & A <> E ) and
A5: ( A <> F & A <> J ) and
A6: A <> M and
A7: ( B <> C & B <> D & B <> E & B <> F & B <> J & B <> M & C <> D & C <> E & C <> F & C <> J & C <> M & D <> E & D <> F & D <> J & D <> M & E <> F & E <> J & E <> M & F <> J & F <> M & J <> M ) ; :: thesis: CompF (A,G) = (((((B '/\' C) '/\' D) '/\' E) '/\' F) '/\' J) '/\' M
A8: not B in {A} by A2, TARSKI:def 1;
G \ {A} = ({A} \/ {B,C,D,E,F,J,M}) \ {A} by A1, ENUMSET1:22;
then A9: G \ {A} = ({A} \ {A}) \/ ({B,C,D,E,F,J,M} \ {A}) by XBOOLE_1:42;
A10: ( not D in {A} & not E in {A} ) by A4, TARSKI:def 1;
A11: not C in {A} by A3, TARSKI:def 1;
A12: not M in {A} by A6, TARSKI:def 1;
A13: ( not F in {A} & not J in {A} ) by A5, TARSKI:def 1;
{B,C,D,E,F,J,M} \ {A} = ({B} \/ {C,D,E,F,J,M}) \ {A} by ENUMSET1:16
.= ({B} \ {A}) \/ ({C,D,E,F,J,M} \ {A}) by XBOOLE_1:42
.= {B} \/ ({C,D,E,F,J,M} \ {A}) by A8, ZFMISC_1:59
.= {B} \/ (({C} \/ {D,E,F,J,M}) \ {A}) by ENUMSET1:11
.= {B} \/ (({C} \ {A}) \/ ({D,E,F,J,M} \ {A})) by XBOOLE_1:42
.= {B} \/ (({C} \ {A}) \/ (({D,E} \/ {F,J,M}) \ {A})) by ENUMSET1:8
.= {B} \/ (({C} \ {A}) \/ (({D,E} \ {A}) \/ ({F,J,M} \ {A}))) by XBOOLE_1:42
.= {B} \/ (({C} \ {A}) \/ ({D,E} \/ ({F,J,M} \ {A}))) by A10, ZFMISC_1:63
.= {B} \/ (({C} \ {A}) \/ ({D,E} \/ (({F,J} \/ {M}) \ {A}))) by ENUMSET1:3
.= {B} \/ (({C} \ {A}) \/ ({D,E} \/ (({F,J} \ {A}) \/ ({M} \ {A})))) by XBOOLE_1:42
.= {B} \/ (({C} \ {A}) \/ ({D,E} \/ ({F,J} \/ ({M} \ {A})))) by A13, ZFMISC_1:63
.= {B} \/ ({C} \/ ({D,E} \/ ({F,J} \/ ({M} \ {A})))) by A11, ZFMISC_1:59
.= {B} \/ ({C} \/ ({D,E} \/ ({F,J} \/ {M}))) by A12, ZFMISC_1:59
.= {B} \/ ({C} \/ ({D,E} \/ {F,J,M})) by ENUMSET1:3
.= {B} \/ ({C} \/ {D,E,F,J,M}) by ENUMSET1:8
.= {B} \/ {C,D,E,F,J,M} by ENUMSET1:11
.= {B,C,D,E,F,J,M} by ENUMSET1:16 ;
then A14: G \ {A} = {} \/ {B,C,D,E,F,J,M} by A9, XBOOLE_1:37;
A15: '/\' (G \ {A}) c= (((((B '/\' C) '/\' D) '/\' E) '/\' F) '/\' J) '/\' M

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in '/\' (G \ {A}) or x in (((((B '/\' C) '/\' D) '/\' E) '/\' F) '/\' J) '/\' M )
reconsider xx = x as set by TARSKI:1;
assume x in '/\' (G \ {A}) ; :: thesis: x in (((((B '/\' C) '/\' D) '/\' E) '/\' F) '/\' J) '/\' M
then consider h being Function, FF being Subset-Family of Y such that
A16: dom h = G \ {A} and
A17: rng h = FF and
A18: for d being set st d in G \ {A} holds
h . d in d and
A19: x = Intersect FF and
A20: x <> {} by BVFUNC_2:def 1;
A21: C in G \ {A} by A14, ENUMSET1:def 5;
then A22: h . C in C by A18;
set mbcdef = ((((h . B) /\ (h . C)) /\ (h . D)) /\ (h . E)) /\ (h . F);
set mbcde = (((h . B) /\ (h . C)) /\ (h . D)) /\ (h . E);
set mbcdefj = (((((h . B) /\ (h . C)) /\ (h . D)) /\ (h . E)) /\ (h . F)) /\ (h . J);
A23: not x in {{}} by A20, TARSKI:def 1;
A24: J in G \ {A} by A14, ENUMSET1:def 5;
then A25: h . J in rng h by A16, FUNCT_1:def 3;
set mbc = (h . B) /\ (h . C);
A26: B in G \ {A} by A14, ENUMSET1:def 5;
then h . B in B by A18;
then A27: (h . B) /\ (h . C) in INTERSECTION (B,C) by A22, SETFAM_1:def 5;
A28: h . B in rng h by A16, A26, FUNCT_1:def 3;
then A29: Intersect FF = meet (rng h) by A17, SETFAM_1:def 9;
A30: h . C in rng h by A16, A21, FUNCT_1:def 3;
A31: F in G \ {A} by A14, ENUMSET1:def 5;
then A32: h . F in rng h by A16, FUNCT_1:def 3;
set mbcd = ((h . B) /\ (h . C)) /\ (h . D);
A33: E in G \ {A} by A14, ENUMSET1:def 5;
then A34: h . E in rng h by A16, FUNCT_1:def 3;
A35: M in G \ {A} by A14, ENUMSET1:def 5;
then A36: h . M in rng h by A16, FUNCT_1:def 3;
A37: D in G \ {A} by A14, ENUMSET1:def 5;
then A38: h . D in rng h by A16, FUNCT_1:def 3;
A39: xx c= ((((((h . B) /\ (h . C)) /\ (h . D)) /\ (h . E)) /\ (h . F)) /\ (h . J)) /\ (h . M)

proof

let p be object ; :: according to TARSKI:def 3 :: thesis: ( not p in xx or p in ((((((h . B) /\ (h . C)) /\ (h . D)) /\ (h . E)) /\ (h . F)) /\ (h . J)) /\ (h . M) )
assume A40: p in xx ; :: thesis: p in ((((((h . B) /\ (h . C)) /\ (h . D)) /\ (h . E)) /\ (h . F)) /\ (h . J)) /\ (h . M)
then ( p in h . B & p in h . C ) by A19, A28, A30, A29, SETFAM_1:def 1;
then A41: p in (h . B) /\ (h . C) by XBOOLE_0:def 4;
p in h . D by A19, A38, A29, A40, SETFAM_1:def 1;
then A42: p in ((h . B) /\ (h . C)) /\ (h . D) by A41, XBOOLE_0:def 4;
p in h . E by A19, A34, A29, A40, SETFAM_1:def 1;
then A43: p in (((h . B) /\ (h . C)) /\ (h . D)) /\ (h . E) by A42, XBOOLE_0:def 4;
p in h . F by A19, A32, A29, A40, SETFAM_1:def 1;
then A44: p in ((((h . B) /\ (h . C)) /\ (h . D)) /\ (h . E)) /\ (h . F) by A43, XBOOLE_0:def 4;
p in h . J by A19, A25, A29, A40, SETFAM_1:def 1;
then A45: p in (((((h . B) /\ (h . C)) /\ (h . D)) /\ (h . E)) /\ (h . F)) /\ (h . J) by A44, XBOOLE_0:def 4;
p in h . M by A19, A36, A29, A40, SETFAM_1:def 1;
hence p in ((((((h . B) /\ (h . C)) /\ (h . D)) /\ (h . E)) /\ (h . F)) /\ (h . J)) /\ (h . M) by A45, XBOOLE_0:def 4; :: thesis: verum

end;

then ((h . B) /\ (h . C)) /\ (h . D) <> {} by A20;
then A46: not ((h . B) /\ (h . C)) /\ (h . D) in {{}} by TARSKI:def 1;
((((((h . B) /\ (h . C)) /\ (h . D)) /\ (h . E)) /\ (h . F)) /\ (h . J)) /\ (h . M) c= xx

proof

A47: rng h c= {(h . B),(h . C),(h . D),(h . E),(h . F),(h . J),(h . M)}

proof

let u be object ; :: according to TARSKI:def 3 :: thesis: ( not u in rng h or u in {(h . B),(h . C),(h . D),(h . E),(h . F),(h . J),(h . M)} )
assume u in rng h ; :: thesis: u in {(h . B),(h . C),(h . D),(h . E),(h . F),(h . J),(h . M)}
then consider x1 being object such that
A48: x1 in dom h and
A49: u = h . x1 by FUNCT_1:def 3;
( x1 = B or x1 = C or x1 = D or x1 = E or x1 = F or x1 = J or x1 = M ) by A14, A16, A48, ENUMSET1:def 5;
hence u in {(h . B),(h . C),(h . D),(h . E),(h . F),(h . J),(h . M)} by A49, ENUMSET1:def 5; :: thesis: verum

end;

let p be object ; :: according to TARSKI:def 3 :: thesis: ( not p in ((((((h . B) /\ (h . C)) /\ (h . D)) /\ (h . E)) /\ (h . F)) /\ (h . J)) /\ (h . M) or p in xx )
assume A50: p in ((((((h . B) /\ (h . C)) /\ (h . D)) /\ (h . E)) /\ (h . F)) /\ (h . J)) /\ (h . M) ; :: thesis: p in xx
then A51: p in h . M by XBOOLE_0:def 4;
A52: p in (((((h . B) /\ (h . C)) /\ (h . D)) /\ (h . E)) /\ (h . F)) /\ (h . J) by A50, XBOOLE_0:def 4;
then A53: p in h . J by XBOOLE_0:def 4;
A54: p in ((((h . B) /\ (h . C)) /\ (h . D)) /\ (h . E)) /\ (h . F) by A52, XBOOLE_0:def 4;
then A55: p in (((h . B) /\ (h . C)) /\ (h . D)) /\ (h . E) by XBOOLE_0:def 4;
then A56: p in h . E by XBOOLE_0:def 4;
A57: p in ((h . B) /\ (h . C)) /\ (h . D) by A55, XBOOLE_0:def 4;
then A58: p in h . D by XBOOLE_0:def 4;
p in (h . B) /\ (h . C) by A57, XBOOLE_0:def 4;
then A59: ( p in h . B & p in h . C ) by XBOOLE_0:def 4;
p in h . F by A54, XBOOLE_0:def 4;
then for y being set st y in rng h holds
p in y by A59, A58, A56, A53, A51, A47, ENUMSET1:def 5;
hence p in xx by A19, A28, A29, SETFAM_1:def 1; :: thesis: verum

end;

then A60: ((((((h . B) /\ (h . C)) /\ (h . D)) /\ (h . E)) /\ (h . F)) /\ (h . J)) /\ (h . M) = x by A39, XBOOLE_0:def 10;
(h . B) /\ (h . C) <> {} by A20, A39;
then not (h . B) /\ (h . C) in {{}} by TARSKI:def 1;
then (h . B) /\ (h . C) in (INTERSECTION (B,C)) \ {{}} by A27, XBOOLE_0:def 5;
then A61: (h . B) /\ (h . C) in B '/\' C by PARTIT1:def 4;
h . D in D by A18, A37;
then ((h . B) /\ (h . C)) /\ (h . D) in INTERSECTION ((B '/\' C),D) by A61, SETFAM_1:def 5;
then ((h . B) /\ (h . C)) /\ (h . D) in (INTERSECTION ((B '/\' C),D)) \ {{}} by A46, XBOOLE_0:def 5;
then A62: ((h . B) /\ (h . C)) /\ (h . D) in (B '/\' C) '/\' D by PARTIT1:def 4;
(((h . B) /\ (h . C)) /\ (h . D)) /\ (h . E) <> {} by A20, A39;
then A63: not (((h . B) /\ (h . C)) /\ (h . D)) /\ (h . E) in {{}} by TARSKI:def 1;
h . E in E by A18, A33;
then (((h . B) /\ (h . C)) /\ (h . D)) /\ (h . E) in INTERSECTION (((B '/\' C) '/\' D),E) by A62, SETFAM_1:def 5;
then (((h . B) /\ (h . C)) /\ (h . D)) /\ (h . E) in (INTERSECTION (((B '/\' C) '/\' D),E)) \ {{}} by A63, XBOOLE_0:def 5;
then A64: (((h . B) /\ (h . C)) /\ (h . D)) /\ (h . E) in ((B '/\' C) '/\' D) '/\' E by PARTIT1:def 4;
((((h . B) /\ (h . C)) /\ (h . D)) /\ (h . E)) /\ (h . F) <> {} by A20, A39;
then A65: not ((((h . B) /\ (h . C)) /\ (h . D)) /\ (h . E)) /\ (h . F) in {{}} by TARSKI:def 1;
h . F in F by A18, A31;
then ((((h . B) /\ (h . C)) /\ (h . D)) /\ (h . E)) /\ (h . F) in INTERSECTION ((((B '/\' C) '/\' D) '/\' E),F) by A64, SETFAM_1:def 5;
then ((((h . B) /\ (h . C)) /\ (h . D)) /\ (h . E)) /\ (h . F) in (INTERSECTION ((((B '/\' C) '/\' D) '/\' E),F)) \ {{}} by A65, XBOOLE_0:def 5;
then A66: ((((h . B) /\ (h . C)) /\ (h . D)) /\ (h . E)) /\ (h . F) in (((B '/\' C) '/\' D) '/\' E) '/\' F by PARTIT1:def 4;
(((((h . B) /\ (h . C)) /\ (h . D)) /\ (h . E)) /\ (h . F)) /\ (h . J) <> {} by A20, A39;
then A67: not (((((h . B) /\ (h . C)) /\ (h . D)) /\ (h . E)) /\ (h . F)) /\ (h . J) in {{}} by TARSKI:def 1;
h . J in J by A18, A24;
then (((((h . B) /\ (h . C)) /\ (h . D)) /\ (h . E)) /\ (h . F)) /\ (h . J) in INTERSECTION (((((B '/\' C) '/\' D) '/\' E) '/\' F),J) by A66, SETFAM_1:def 5;
then (((((h . B) /\ (h . C)) /\ (h . D)) /\ (h . E)) /\ (h . F)) /\ (h . J) in (INTERSECTION (((((B '/\' C) '/\' D) '/\' E) '/\' F),J)) \ {{}} by A67, XBOOLE_0:def 5;
then A68: (((((h . B) /\ (h . C)) /\ (h . D)) /\ (h . E)) /\ (h . F)) /\ (h . J) in ((((B '/\' C) '/\' D) '/\' E) '/\' F) '/\' J by PARTIT1:def 4;
h . M in M by A18, A35;
then x in INTERSECTION ((((((B '/\' C) '/\' D) '/\' E) '/\' F) '/\' J),M) by A60, A68, SETFAM_1:def 5;
then x in (INTERSECTION ((((((B '/\' C) '/\' D) '/\' E) '/\' F) '/\' J),M)) \ {{}} by A23, XBOOLE_0:def 5;
hence x in (((((B '/\' C) '/\' D) '/\' E) '/\' F) '/\' J) '/\' M by PARTIT1:def 4; :: thesis: verum

end;

A69: (((((B '/\' C) '/\' D) '/\' E) '/\' F) '/\' J) '/\' M c= '/\' (G \ {A})

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in (((((B '/\' C) '/\' D) '/\' E) '/\' F) '/\' J) '/\' M or x in '/\' (G \ {A}) )
reconsider xx = x as set by TARSKI:1;
assume A70: x in (((((B '/\' C) '/\' D) '/\' E) '/\' F) '/\' J) '/\' M ; :: thesis: x in '/\' (G \ {A})
then A71: x <> {} by EQREL_1:def 4;
x in (INTERSECTION ((((((B '/\' C) '/\' D) '/\' E) '/\' F) '/\' J),M)) \ {{}} by A70, PARTIT1:def 4;
then consider bcdefj, m being set such that
A72: bcdefj in ((((B '/\' C) '/\' D) '/\' E) '/\' F) '/\' J and
A73: m in M and
A74: x = bcdefj /\ m by SETFAM_1:def 5;
bcdefj in (INTERSECTION (((((B '/\' C) '/\' D) '/\' E) '/\' F),J)) \ {{}} by A72, PARTIT1:def 4;
then consider bcdef, j being set such that
A75: bcdef in (((B '/\' C) '/\' D) '/\' E) '/\' F and
A76: j in J and
A77: bcdefj = bcdef /\ j by SETFAM_1:def 5;
bcdef in (INTERSECTION ((((B '/\' C) '/\' D) '/\' E),F)) \ {{}} by A75, PARTIT1:def 4;
then consider bcde, f being set such that
A78: bcde in ((B '/\' C) '/\' D) '/\' E and
A79: f in F and
A80: bcdef = bcde /\ f by SETFAM_1:def 5;
bcde in (INTERSECTION (((B '/\' C) '/\' D),E)) \ {{}} by A78, PARTIT1:def 4;
then consider bcd, e being set such that
A81: bcd in (B '/\' C) '/\' D and
A82: e in E and
A83: bcde = bcd /\ e by SETFAM_1:def 5;
bcd in (INTERSECTION ((B '/\' C),D)) \ {{}} by A81, PARTIT1:def 4;
then consider bc, d being set such that
A84: bc in B '/\' C and
A85: d in D and
A86: bcd = bc /\ d by SETFAM_1:def 5;
bc in (INTERSECTION (B,C)) \ {{}} by A84, PARTIT1:def 4;
then consider b, c being set such that
A87: ( b in B & c in C ) and
A88: bc = b /\ c by SETFAM_1:def 5;
set h = ((((((B .--> b) +* (C .--> c)) +* (D .--> d)) +* (E .--> e)) +* (F .--> f)) +* (J .--> j)) +* (M .--> m);
A89: (((((((B .--> b) +* (C .--> c)) +* (D .--> d)) +* (E .--> e)) +* (F .--> f)) +* (J .--> j)) +* (M .--> m)) . B = b by A7, Th49;
A90: dom (((((((B .--> b) +* (C .--> c)) +* (D .--> d)) +* (E .--> e)) +* (F .--> f)) +* (J .--> j)) +* (M .--> m)) = {M,B,C,D,E,F,J} by Th50
.= {M} \/ {B,C,D,E,F,J} by ENUMSET1:16
.= {B,C,D,E,F,J,M} by ENUMSET1:21 ;
then A91: ( E in dom (((((((B .--> b) +* (C .--> c)) +* (D .--> d)) +* (E .--> e)) +* (F .--> f)) +* (J .--> j)) +* (M .--> m)) & F in dom (((((((B .--> b) +* (C .--> c)) +* (D .--> d)) +* (E .--> e)) +* (F .--> f)) +* (J .--> j)) +* (M .--> m)) ) by ENUMSET1:def 5;
A92: D in dom (((((((B .--> b) +* (C .--> c)) +* (D .--> d)) +* (E .--> e)) +* (F .--> f)) +* (J .--> j)) +* (M .--> m)) by A90, ENUMSET1:def 5;
then A93: (((((((B .--> b) +* (C .--> c)) +* (D .--> d)) +* (E .--> e)) +* (F .--> f)) +* (J .--> j)) +* (M .--> m)) . D in rng (((((((B .--> b) +* (C .--> c)) +* (D .--> d)) +* (E .--> e)) +* (F .--> f)) +* (J .--> j)) +* (M .--> m)) by FUNCT_1:def 3;
A94: ( J in dom (((((((B .--> b) +* (C .--> c)) +* (D .--> d)) +* (E .--> e)) +* (F .--> f)) +* (J .--> j)) +* (M .--> m)) & M in dom (((((((B .--> b) +* (C .--> c)) +* (D .--> d)) +* (E .--> e)) +* (F .--> f)) +* (J .--> j)) +* (M .--> m)) ) by A90, ENUMSET1:def 5;
A95: ( B in dom (((((((B .--> b) +* (C .--> c)) +* (D .--> d)) +* (E .--> e)) +* (F .--> f)) +* (J .--> j)) +* (M .--> m)) & C in dom (((((((B .--> b) +* (C .--> c)) +* (D .--> d)) +* (E .--> e)) +* (F .--> f)) +* (J .--> j)) +* (M .--> m)) ) by A90, ENUMSET1:def 5;
A96: {((((((((B .--> b) +* (C .--> c)) +* (D .--> d)) +* (E .--> e)) +* (F .--> f)) +* (J .--> j)) +* (M .--> m)) . B),((((((((B .--> b) +* (C .--> c)) +* (D .--> d)) +* (E .--> e)) +* (F .--> f)) +* (J .--> j)) +* (M .--> m)) . C),((((((((B .--> b) +* (C .--> c)) +* (D .--> d)) +* (E .--> e)) +* (F .--> f)) +* (J .--> j)) +* (M .--> m)) . D),((((((((B .--> b) +* (C .--> c)) +* (D .--> d)) +* (E .--> e)) +* (F .--> f)) +* (J .--> j)) +* (M .--> m)) . E),((((((((B .--> b) +* (C .--> c)) +* (D .--> d)) +* (E .--> e)) +* (F .--> f)) +* (J .--> j)) +* (M .--> m)) . F),((((((((B .--> b) +* (C .--> c)) +* (D .--> d)) +* (E .--> e)) +* (F .--> f)) +* (J .--> j)) +* (M .--> m)) . J),((((((((B .--> b) +* (C .--> c)) +* (D .--> d)) +* (E .--> e)) +* (F .--> f)) +* (J .--> j)) +* (M .--> m)) . M)} c= rng (((((((B .--> b) +* (C .--> c)) +* (D .--> d)) +* (E .--> e)) +* (F .--> f)) +* (J .--> j)) +* (M .--> m))

proof

let t be object ; :: according to TARSKI:def 3 :: thesis: ( not t in {((((((((B .--> b) +* (C .--> c)) +* (D .--> d)) +* (E .--> e)) +* (F .--> f)) +* (J .--> j)) +* (M .--> m)) . B),((((((((B .--> b) +* (C .--> c)) +* (D .--> d)) +* (E .--> e)) +* (F .--> f)) +* (J .--> j)) +* (M .--> m)) . C),((((((((B .--> b) +* (C .--> c)) +* (D .--> d)) +* (E .--> e)) +* (F .--> f)) +* (J .--> j)) +* (M .--> m)) . D),((((((((B .--> b) +* (C .--> c)) +* (D .--> d)) +* (E .--> e)) +* (F .--> f)) +* (J .--> j)) +* (M .--> m)) . E),((((((((B .--> b) +* (C .--> c)) +* (D .--> d)) +* (E .--> e)) +* (F .--> f)) +* (J .--> j)) +* (M .--> m)) . F),((((((((B .--> b) +* (C .--> c)) +* (D .--> d)) +* (E .--> e)) +* (F .--> f)) +* (J .--> j)) +* (M .--> m)) . J),((((((((B .--> b) +* (C .--> c)) +* (D .--> d)) +* (E .--> e)) +* (F .--> f)) +* (J .--> j)) +* (M .--> m)) . M)} or t in rng (((((((B .--> b) +* (C .--> c)) +* (D .--> d)) +* (E .--> e)) +* (F .--> f)) +* (J .--> j)) +* (M .--> m)) )
assume t in {((((((((B .--> b) +* (C .--> c)) +* (D .--> d)) +* (E .--> e)) +* (F .--> f)) +* (J .--> j)) +* (M .--> m)) . B),((((((((B .--> b) +* (C .--> c)) +* (D .--> d)) +* (E .--> e)) +* (F .--> f)) +* (J .--> j)) +* (M .--> m)) . C),((((((((B .--> b) +* (C .--> c)) +* (D .--> d)) +* (E .--> e)) +* (F .--> f)) +* (J .--> j)) +* (M .--> m)) . D),((((((((B .--> b) +* (C .--> c)) +* (D .--> d)) +* (E .--> e)) +* (F .--> f)) +* (J .--> j)) +* (M .--> m)) . E),((((((((B .--> b) +* (C .--> c)) +* (D .--> d)) +* (E .--> e)) +* (F .--> f)) +* (J .--> j)) +* (M .--> m)) . F),((((((((B .--> b) +* (C .--> c)) +* (D .--> d)) +* (E .--> e)) +* (F .--> f)) +* (J .--> j)) +* (M .--> m)) . J),((((((((B .--> b) +* (C .--> c)) +* (D .--> d)) +* (E .--> e)) +* (F .--> f)) +* (J .--> j)) +* (M .--> m)) . M)} ; :: thesis: t in rng (((((((B .--> b) +* (C .--> c)) +* (D .--> d)) +* (E .--> e)) +* (F .--> f)) +* (J .--> j)) +* (M .--> m))
then ( t = (((((((B .--> b) +* (C .--> c)) +* (D .--> d)) +* (E .--> e)) +* (F .--> f)) +* (J .--> j)) +* (M .--> m)) . D or t = (((((((B .--> b) +* (C .--> c)) +* (D .--> d)) +* (E .--> e)) +* (F .--> f)) +* (J .--> j)) +* (M .--> m)) . B or t = (((((((B .--> b) +* (C .--> c)) +* (D .--> d)) +* (E .--> e)) +* (F .--> f)) +* (J .--> j)) +* (M .--> m)) . C or t = (((((((B .--> b) +* (C .--> c)) +* (D .--> d)) +* (E .--> e)) +* (F .--> f)) +* (J .--> j)) +* (M .--> m)) . E or t = (((((((B .--> b) +* (C .--> c)) +* (D .--> d)) +* (E .--> e)) +* (F .--> f)) +* (J .--> j)) +* (M .--> m)) . F or t = (((((((B .--> b) +* (C .--> c)) +* (D .--> d)) +* (E .--> e)) +* (F .--> f)) +* (J .--> j)) +* (M .--> m)) . J or t = (((((((B .--> b) +* (C .--> c)) +* (D .--> d)) +* (E .--> e)) +* (F .--> f)) +* (J .--> j)) +* (M .--> m)) . M ) by ENUMSET1:def 5;
hence t in rng (((((((B .--> b) +* (C .--> c)) +* (D .--> d)) +* (E .--> e)) +* (F .--> f)) +* (J .--> j)) +* (M .--> m)) by A92, A95, A91, A94, FUNCT_1:def 3; :: thesis: verum

end;

A97: for p being set st p in G \ {A} holds
(((((((B .--> b) +* (C .--> c)) +* (D .--> d)) +* (E .--> e)) +* (F .--> f)) +* (J .--> j)) +* (M .--> m)) . p in p

proof

let p be set ; :: thesis: ( p in G \ {A} implies (((((((B .--> b) +* (C .--> c)) +* (D .--> d)) +* (E .--> e)) +* (F .--> f)) +* (J .--> j)) +* (M .--> m)) . p in p )
assume p in G \ {A} ; :: thesis: (((((((B .--> b) +* (C .--> c)) +* (D .--> d)) +* (E .--> e)) +* (F .--> f)) +* (J .--> j)) +* (M .--> m)) . p in p
then ( p = D or p = B or p = C or p = E or p = F or p = J or p = M ) by A14, ENUMSET1:def 5;
hence (((((((B .--> b) +* (C .--> c)) +* (D .--> d)) +* (E .--> e)) +* (F .--> f)) +* (J .--> j)) +* (M .--> m)) . p in p by A7, A73, A76, A79, A82, A85, A87, Th49; :: thesis: verum

end;

A98: (((((((B .--> b) +* (C .--> c)) +* (D .--> d)) +* (E .--> e)) +* (F .--> f)) +* (J .--> j)) +* (M .--> m)) . C = c by A7, Th49;
A99: (((((((B .--> b) +* (C .--> c)) +* (D .--> d)) +* (E .--> e)) +* (F .--> f)) +* (J .--> j)) +* (M .--> m)) . M = m by A7, Th49;
A100: (((((((B .--> b) +* (C .--> c)) +* (D .--> d)) +* (E .--> e)) +* (F .--> f)) +* (J .--> j)) +* (M .--> m)) . J = j by A7, Th49;
A101: (((((((B .--> b) +* (C .--> c)) +* (D .--> d)) +* (E .--> e)) +* (F .--> f)) +* (J .--> j)) +* (M .--> m)) . F = f by A7, Th49;
A102: rng (((((((B .--> b) +* (C .--> c)) +* (D .--> d)) +* (E .--> e)) +* (F .--> f)) +* (J .--> j)) +* (M .--> m)) c= {((((((((B .--> b) +* (C .--> c)) +* (D .--> d)) +* (E .--> e)) +* (F .--> f)) +* (J .--> j)) +* (M .--> m)) . B),((((((((B .--> b) +* (C .--> c)) +* (D .--> d)) +* (E .--> e)) +* (F .--> f)) +* (J .--> j)) +* (M .--> m)) . C),((((((((B .--> b) +* (C .--> c)) +* (D .--> d)) +* (E .--> e)) +* (F .--> f)) +* (J .--> j)) +* (M .--> m)) . D),((((((((B .--> b) +* (C .--> c)) +* (D .--> d)) +* (E .--> e)) +* (F .--> f)) +* (J .--> j)) +* (M .--> m)) . E),((((((((B .--> b) +* (C .--> c)) +* (D .--> d)) +* (E .--> e)) +* (F .--> f)) +* (J .--> j)) +* (M .--> m)) . F),((((((((B .--> b) +* (C .--> c)) +* (D .--> d)) +* (E .--> e)) +* (F .--> f)) +* (J .--> j)) +* (M .--> m)) . J),((((((((B .--> b) +* (C .--> c)) +* (D .--> d)) +* (E .--> e)) +* (F .--> f)) +* (J .--> j)) +* (M .--> m)) . M)}

proof

let t be object ; :: according to TARSKI:def 3 :: thesis: ( not t in rng (((((((B .--> b) +* (C .--> c)) +* (D .--> d)) +* (E .--> e)) +* (F .--> f)) +* (J .--> j)) +* (M .--> m)) or t in {((((((((B .--> b) +* (C .--> c)) +* (D .--> d)) +* (E .--> e)) +* (F .--> f)) +* (J .--> j)) +* (M .--> m)) . B),((((((((B .--> b) +* (C .--> c)) +* (D .--> d)) +* (E .--> e)) +* (F .--> f)) +* (J .--> j)) +* (M .--> m)) . C),((((((((B .--> b) +* (C .--> c)) +* (D .--> d)) +* (E .--> e)) +* (F .--> f)) +* (J .--> j)) +* (M .--> m)) . D),((((((((B .--> b) +* (C .--> c)) +* (D .--> d)) +* (E .--> e)) +* (F .--> f)) +* (J .--> j)) +* (M .--> m)) . E),((((((((B .--> b) +* (C .--> c)) +* (D .--> d)) +* (E .--> e)) +* (F .--> f)) +* (J .--> j)) +* (M .--> m)) . F),((((((((B .--> b) +* (C .--> c)) +* (D .--> d)) +* (E .--> e)) +* (F .--> f)) +* (J .--> j)) +* (M .--> m)) . J),((((((((B .--> b) +* (C .--> c)) +* (D .--> d)) +* (E .--> e)) +* (F .--> f)) +* (J .--> j)) +* (M .--> m)) . M)} )
assume t in rng (((((((B .--> b) +* (C .--> c)) +* (D .--> d)) +* (E .--> e)) +* (F .--> f)) +* (J .--> j)) +* (M .--> m)) ; :: thesis: t in {((((((((B .--> b) +* (C .--> c)) +* (D .--> d)) +* (E .--> e)) +* (F .--> f)) +* (J .--> j)) +* (M .--> m)) . B),((((((((B .--> b) +* (C .--> c)) +* (D .--> d)) +* (E .--> e)) +* (F .--> f)) +* (J .--> j)) +* (M .--> m)) . C),((((((((B .--> b) +* (C .--> c)) +* (D .--> d)) +* (E .--> e)) +* (F .--> f)) +* (J .--> j)) +* (M .--> m)) . D),((((((((B .--> b) +* (C .--> c)) +* (D .--> d)) +* (E .--> e)) +* (F .--> f)) +* (J .--> j)) +* (M .--> m)) . E),((((((((B .--> b) +* (C .--> c)) +* (D .--> d)) +* (E .--> e)) +* (F .--> f)) +* (J .--> j)) +* (M .--> m)) . F),((((((((B .--> b) +* (C .--> c)) +* (D .--> d)) +* (E .--> e)) +* (F .--> f)) +* (J .--> j)) +* (M .--> m)) . J),((((((((B .--> b) +* (C .--> c)) +* (D .--> d)) +* (E .--> e)) +* (F .--> f)) +* (J .--> j)) +* (M .--> m)) . M)}
then consider x1 being object such that
A103: x1 in dom (((((((B .--> b) +* (C .--> c)) +* (D .--> d)) +* (E .--> e)) +* (F .--> f)) +* (J .--> j)) +* (M .--> m)) and
A104: t = (((((((B .--> b) +* (C .--> c)) +* (D .--> d)) +* (E .--> e)) +* (F .--> f)) +* (J .--> j)) +* (M .--> m)) . x1 by FUNCT_1:def 3;
( x1 = D or x1 = B or x1 = C or x1 = E or x1 = F or x1 = J or x1 = M ) by A90, A103, ENUMSET1:def 5;
hence t in {((((((((B .--> b) +* (C .--> c)) +* (D .--> d)) +* (E .--> e)) +* (F .--> f)) +* (J .--> j)) +* (M .--> m)) . B),((((((((B .--> b) +* (C .--> c)) +* (D .--> d)) +* (E .--> e)) +* (F .--> f)) +* (J .--> j)) +* (M .--> m)) . C),((((((((B .--> b) +* (C .--> c)) +* (D .--> d)) +* (E .--> e)) +* (F .--> f)) +* (J .--> j)) +* (M .--> m)) . D),((((((((B .--> b) +* (C .--> c)) +* (D .--> d)) +* (E .--> e)) +* (F .--> f)) +* (J .--> j)) +* (M .--> m)) . E),((((((((B .--> b) +* (C .--> c)) +* (D .--> d)) +* (E .--> e)) +* (F .--> f)) +* (J .--> j)) +* (M .--> m)) . F),((((((((B .--> b) +* (C .--> c)) +* (D .--> d)) +* (E .--> e)) +* (F .--> f)) +* (J .--> j)) +* (M .--> m)) . J),((((((((B .--> b) +* (C .--> c)) +* (D .--> d)) +* (E .--> e)) +* (F .--> f)) +* (J .--> j)) +* (M .--> m)) . M)} by A104, ENUMSET1:def 5; :: thesis: verum

end;

then A105: rng (((((((B .--> b) +* (C .--> c)) +* (D .--> d)) +* (E .--> e)) +* (F .--> f)) +* (J .--> j)) +* (M .--> m)) = {((((((((B .--> b) +* (C .--> c)) +* (D .--> d)) +* (E .--> e)) +* (F .--> f)) +* (J .--> j)) +* (M .--> m)) . B),((((((((B .--> b) +* (C .--> c)) +* (D .--> d)) +* (E .--> e)) +* (F .--> f)) +* (J .--> j)) +* (M .--> m)) . C),((((((((B .--> b) +* (C .--> c)) +* (D .--> d)) +* (E .--> e)) +* (F .--> f)) +* (J .--> j)) +* (M .--> m)) . D),((((((((B .--> b) +* (C .--> c)) +* (D .--> d)) +* (E .--> e)) +* (F .--> f)) +* (J .--> j)) +* (M .--> m)) . E),((((((((B .--> b) +* (C .--> c)) +* (D .--> d)) +* (E .--> e)) +* (F .--> f)) +* (J .--> j)) +* (M .--> m)) . F),((((((((B .--> b) +* (C .--> c)) +* (D .--> d)) +* (E .--> e)) +* (F .--> f)) +* (J .--> j)) +* (M .--> m)) . J),((((((((B .--> b) +* (C .--> c)) +* (D .--> d)) +* (E .--> e)) +* (F .--> f)) +* (J .--> j)) +* (M .--> m)) . M)} by A96, XBOOLE_0:def 10;
A106: (((((((B .--> b) +* (C .--> c)) +* (D .--> d)) +* (E .--> e)) +* (F .--> f)) +* (J .--> j)) +* (M .--> m)) . E = e by A7, Th49;
A107: (((((((B .--> b) +* (C .--> c)) +* (D .--> d)) +* (E .--> e)) +* (F .--> f)) +* (J .--> j)) +* (M .--> m)) . D = d by A7, Th49;
rng (((((((B .--> b) +* (C .--> c)) +* (D .--> d)) +* (E .--> e)) +* (F .--> f)) +* (J .--> j)) +* (M .--> m)) c= bool Y

proof

let t be object ; :: according to TARSKI:def 3 :: thesis: ( not t in rng (((((((B .--> b) +* (C .--> c)) +* (D .--> d)) +* (E .--> e)) +* (F .--> f)) +* (J .--> j)) +* (M .--> m)) or t in bool Y )
assume t in rng (((((((B .--> b) +* (C .--> c)) +* (D .--> d)) +* (E .--> e)) +* (F .--> f)) +* (J .--> j)) +* (M .--> m)) ; :: thesis: t in bool Y
then ( t = (((((((B .--> b) +* (C .--> c)) +* (D .--> d)) +* (E .--> e)) +* (F .--> f)) +* (J .--> j)) +* (M .--> m)) . D or t = (((((((B .--> b) +* (C .--> c)) +* (D .--> d)) +* (E .--> e)) +* (F .--> f)) +* (J .--> j)) +* (M .--> m)) . B or t = (((((((B .--> b) +* (C .--> c)) +* (D .--> d)) +* (E .--> e)) +* (F .--> f)) +* (J .--> j)) +* (M .--> m)) . C or t = (((((((B .--> b) +* (C .--> c)) +* (D .--> d)) +* (E .--> e)) +* (F .--> f)) +* (J .--> j)) +* (M .--> m)) . E or t = (((((((B .--> b) +* (C .--> c)) +* (D .--> d)) +* (E .--> e)) +* (F .--> f)) +* (J .--> j)) +* (M .--> m)) . F or t = (((((((B .--> b) +* (C .--> c)) +* (D .--> d)) +* (E .--> e)) +* (F .--> f)) +* (J .--> j)) +* (M .--> m)) . J or t = (((((((B .--> b) +* (C .--> c)) +* (D .--> d)) +* (E .--> e)) +* (F .--> f)) +* (J .--> j)) +* (M .--> m)) . M ) by A102, ENUMSET1:def 5;
hence t in bool Y by A73, A76, A79, A82, A85, A87, A107, A89, A98, A106, A101, A100, A99; :: thesis: verum

end;

then reconsider FF = rng (((((((B .--> b) +* (C .--> c)) +* (D .--> d)) +* (E .--> e)) +* (F .--> f)) +* (J .--> j)) +* (M .--> m)) as Subset-Family of Y ;
reconsider h = ((((((B .--> b) +* (C .--> c)) +* (D .--> d)) +* (E .--> e)) +* (F .--> f)) +* (J .--> j)) +* (M .--> m) as Function ;
A108: xx c= Intersect FF

proof

let u be object ; :: according to TARSKI:def 3 :: thesis: ( not u in xx or u in Intersect FF )
assume A109: u in xx ; :: thesis: u in Intersect FF
for y being set st y in FF holds
u in y

proof

let y be set ; :: thesis: ( y in FF implies u in y )
assume A110: y in FF ; :: thesis: u in y

now :: thesis: ( ( y = h . D & u in y ) or ( y = h . B & u in y ) or ( y = h . C & u in y ) or ( y = h . E & u in y ) or ( y = h . F & u in y ) or ( y = h . J & u in y ) or ( y = h . M & u in y ) )

per cases ( y = h . D or y = h . B or y = h . C or y = h . E or y = h . F or y = h . J or y = h . M ) by A102, A110, ENUMSET1:def 5;

case A111: y = h . D ; :: thesis: u in y

u in (((d /\ ((b /\ c) /\ e)) /\ f) /\ j) /\ m by A74, A77, A80, A83, A86, A88, A109, XBOOLE_1:16;
then u in ((d /\ (((b /\ c) /\ e) /\ f)) /\ j) /\ m by XBOOLE_1:16;
then u in (d /\ ((((b /\ c) /\ e) /\ f) /\ j)) /\ m by XBOOLE_1:16;
then u in d /\ (((((b /\ c) /\ e) /\ f) /\ j) /\ m) by XBOOLE_1:16;
hence u in y by A107, A111, XBOOLE_0:def 4; :: thesis: verum

end;

case A112: y = h . B ; :: thesis: u in y

u in ((((c /\ (d /\ b)) /\ e) /\ f) /\ j) /\ m by A74, A77, A80, A83, A86, A88, A109, XBOOLE_1:16;
then u in (((c /\ ((d /\ b) /\ e)) /\ f) /\ j) /\ m by XBOOLE_1:16;
then u in (((c /\ ((d /\ e) /\ b)) /\ f) /\ j) /\ m by XBOOLE_1:16;
then u in ((c /\ (((d /\ e) /\ b) /\ f)) /\ j) /\ m by XBOOLE_1:16;
then u in (c /\ ((((d /\ e) /\ b) /\ f) /\ j)) /\ m by XBOOLE_1:16;
then u in (c /\ (((d /\ e) /\ (f /\ b)) /\ j)) /\ m by XBOOLE_1:16;
then u in (c /\ ((d /\ e) /\ ((f /\ b) /\ j))) /\ m by XBOOLE_1:16;
then u in (c /\ ((d /\ e) /\ (f /\ (j /\ b)))) /\ m by XBOOLE_1:16;
then u in ((c /\ (d /\ e)) /\ (f /\ (j /\ b))) /\ m by XBOOLE_1:16;
then u in (((c /\ (d /\ e)) /\ f) /\ (j /\ b)) /\ m by XBOOLE_1:16;
then u in ((((c /\ (d /\ e)) /\ f) /\ j) /\ b) /\ m by XBOOLE_1:16;
then u in ((((c /\ (d /\ e)) /\ f) /\ j) /\ m) /\ b by XBOOLE_1:16;
hence u in y by A89, A112, XBOOLE_0:def 4; :: thesis: verum

end;

case A113: y = h . C ; :: thesis: u in y

u in ((((c /\ (d /\ b)) /\ e) /\ f) /\ j) /\ m by A74, A77, A80, A83, A86, A88, A109, XBOOLE_1:16;
then u in (((c /\ ((d /\ b) /\ e)) /\ f) /\ j) /\ m by XBOOLE_1:16;
then u in (((c /\ ((d /\ e) /\ b)) /\ f) /\ j) /\ m by XBOOLE_1:16;
then u in ((c /\ (((d /\ e) /\ b) /\ f)) /\ j) /\ m by XBOOLE_1:16;
then u in (c /\ ((((d /\ e) /\ b) /\ f) /\ j)) /\ m by XBOOLE_1:16;
then u in c /\ (((((d /\ e) /\ b) /\ f) /\ j) /\ m) by XBOOLE_1:16;
hence u in y by A98, A113, XBOOLE_0:def 4; :: thesis: verum

end;

case A114: y = h . E ; :: thesis: u in y

u in ((((b /\ c) /\ d) /\ (f /\ e)) /\ j) /\ m by A74, A77, A80, A83, A86, A88, A109, XBOOLE_1:16;
then u in (((b /\ c) /\ d) /\ ((f /\ e) /\ j)) /\ m by XBOOLE_1:16;
then u in (((b /\ c) /\ d) /\ ((f /\ j) /\ e)) /\ m by XBOOLE_1:16;
then u in ((((b /\ c) /\ d) /\ (f /\ j)) /\ e) /\ m by XBOOLE_1:16;
then u in ((((b /\ c) /\ d) /\ (f /\ j)) /\ m) /\ e by XBOOLE_1:16;
hence u in y by A106, A114, XBOOLE_0:def 4; :: thesis: verum

end;

case A115: y = h . F ; :: thesis: u in y

u in (((((b /\ c) /\ d) /\ e) /\ j) /\ f) /\ m by A74, A77, A80, A83, A86, A88, A109, XBOOLE_1:16;
then u in (((((b /\ c) /\ d) /\ e) /\ j) /\ m) /\ f by XBOOLE_1:16;
hence u in y by A101, A115, XBOOLE_0:def 4; :: thesis: verum

end;

case A116: y = h . J ; :: thesis: u in y

u in (((((b /\ c) /\ d) /\ e) /\ f) /\ m) /\ j by A74, A77, A80, A83, A86, A88, A109, XBOOLE_1:16;
hence u in y by A100, A116, XBOOLE_0:def 4; :: thesis: verum

end;

case y = h . M ; :: thesis: u in y

hence u in y by A74, A99, A109, XBOOLE_0:def 4; :: thesis: verum

end;

end;

end;

hence u in y ; :: thesis: verum

end;

then u in meet FF by A105, SETFAM_1:def 1;
hence u in Intersect FF by A105, SETFAM_1:def 9; :: thesis: verum

end;

A117: Intersect FF = meet (rng h) by A93, SETFAM_1:def 9;
Intersect FF c= xx

proof

let t be object ; :: according to TARSKI:def 3 :: thesis: ( not t in Intersect FF or t in xx )
assume A118: t in Intersect FF ; :: thesis: t in xx
h . C in {(h . B),(h . C),(h . D),(h . E),(h . F),(h . J),(h . M)} by ENUMSET1:def 5;
then A119: t in c by A98, A96, A117, A118, SETFAM_1:def 1;
h . B in {(h . B),(h . C),(h . D),(h . E),(h . F),(h . J),(h . M)} by ENUMSET1:def 5;
then t in b by A89, A96, A117, A118, SETFAM_1:def 1;
then A120: t in b /\ c by A119, XBOOLE_0:def 4;
h . D in {(h . B),(h . C),(h . D),(h . E),(h . F),(h . J),(h . M)} by ENUMSET1:def 5;
then t in d by A107, A96, A117, A118, SETFAM_1:def 1;
then A121: t in (b /\ c) /\ d by A120, XBOOLE_0:def 4;
h . E in {(h . B),(h . C),(h . D),(h . E),(h . F),(h . J),(h . M)} by ENUMSET1:def 5;
then t in e by A106, A96, A117, A118, SETFAM_1:def 1;
then A122: t in ((b /\ c) /\ d) /\ e by A121, XBOOLE_0:def 4;
h . F in {(h . B),(h . C),(h . D),(h . E),(h . F),(h . J),(h . M)} by ENUMSET1:def 5;
then t in f by A101, A96, A117, A118, SETFAM_1:def 1;
then A123: t in (((b /\ c) /\ d) /\ e) /\ f by A122, XBOOLE_0:def 4;
h . J in {(h . B),(h . C),(h . D),(h . E),(h . F),(h . J),(h . M)} by ENUMSET1:def 5;
then t in j by A100, A96, A117, A118, SETFAM_1:def 1;
then A124: t in ((((b /\ c) /\ d) /\ e) /\ f) /\ j by A123, XBOOLE_0:def 4;
h . M in {(h . B),(h . C),(h . D),(h . E),(h . F),(h . J),(h . M)} by ENUMSET1:def 5;
then t in m by A99, A96, A117, A118, SETFAM_1:def 1;
hence t in xx by A74, A77, A80, A83, A86, A88, A124, XBOOLE_0:def 4; :: thesis: verum

end;

then x = Intersect FF by A108, XBOOLE_0:def 10;
hence x in '/\' (G \ {A}) by A14, A90, A97, A71, BVFUNC_2:def 1; :: thesis: verum

end;

CompF (A,G) = '/\' (G \ {A}) by BVFUNC_2:def 7;
hence CompF (A,G) = (((((B '/\' C) '/\' D) '/\' E) '/\' F) '/\' J) '/\' M by A69, A15, XBOOLE_0:def 10; :: thesis: verum