Copyright (c) 1999 Association of Mizar Users
environ
vocabulary FUNCT_2, MARGREL1, PARTIT1, EQREL_1, FUNCT_1, CAT_1, FUNCT_4,
RELAT_1, BOOLE, BVFUNC_2, T_1TOPSP, SETFAM_1, CANTOR_1, ZF_LANG,
BVFUNC_1;
notation TARSKI, XBOOLE_0, ENUMSET1, ZFMISC_1, SUBSET_1, SETFAM_1, RELAT_1,
FUNCT_1, FRAENKEL, CQC_LANG, FUNCT_4, MARGREL1, VALUAT_1, EQREL_1,
PARTIT1, CANTOR_1, BVFUNC_1, BVFUNC_2;
constructors BVFUNC_2, SETWISEO, CANTOR_1, FUNCT_7, BVFUNC_1;
clusters SUBSET_1, PARTIT1, CQC_LANG, MARGREL1, VALUAT_1, AMI_1, XBOOLE_0;
requirements SUBSET, BOOLE;
definitions TARSKI, BVFUNC_1;
theorems EQREL_1, T_1TOPSP, MARGREL1, PARTIT1, BVFUNC_1, BVFUNC_2, BVFUNC11,
BVFUNC14, FUNCT_4, CQC_LANG, TARSKI, ENUMSET1, FUNCT_1, CANTOR_1,
SETFAM_1, YELLOW14, VALUAT_1, XBOOLE_0;
begin :: Chap. 1 Preliminaries
reserve Y for non empty set,
a for Element of Funcs(Y,BOOLEAN),
G for Subset of PARTITIONS(Y),
A, B, C, D for a_partition of Y;
theorem Th1:
for h being Function, A',B',C',D' being set st
G={A,B,C,D} & A<>B & A<>C & A<>D & B<>C & B<>D & C<>D &
h = (B .--> B') +* (C .--> C') +* (D .--> D') +* (A .--> A')
holds h.B = B' & h.C = C' & h.D = D'
proof
let h be Function;
let A',B',C',D' be set;
assume A1: G={A,B,C,D} & A<>B & A<>C & A<>D & B<>C & B<>D & C<>D &
h = (B .--> B') +* (C .--> C') +*
(D .--> D') +* (A .--> A');
A2: dom (C .--> C') = {C} by CQC_LANG:5;
A3: dom (D .--> D') = {D} by CQC_LANG:5;
A4: dom (A .--> A') = {A} by CQC_LANG:5;
thus h.B = B'
proof
not B in dom (A .--> A') by TARSKI:def 1,A1,A4; then
A5:h.B=((B .--> B') +* (C .--> C') +*
(D .--> D')).B by FUNCT_4:42,A1;
not B in dom (D .--> D') by TARSKI:def 1,A1,A3; then
A6:h.B=((B .--> B') +* (C .--> C')).B by A5,FUNCT_4:42;
not B in dom (C .--> C') by TARSKI:def 1,A1,A2; then
h.B=(B .--> B').B by A6,FUNCT_4:42;
hence thesis by CQC_LANG:6;
end;
thus h.C = C'
proof
not C in dom (A .--> A') by TARSKI:def 1,A1,A4; then
A7:h.C=((B .--> B') +* (C .--> C') +* (D .--> D')).C by FUNCT_4:42,A1;
not C in dom (D .--> D') by TARSKI:def 1,A1,A3; then
A8:h.C=((B .--> B') +* (C .--> C')).C
by A7,FUNCT_4:42;
C in dom (C .--> C') by A2,TARSKI:def 1;then
h.C=(C .--> C').C by A8,FUNCT_4:44;
hence thesis by CQC_LANG:6;
end;
not D in dom (A .--> A') by TARSKI:def 1,A1,A4; then
A9:h.D=((B .--> B') +* (C .--> C') +* (D .--> D')).D
by FUNCT_4:42,A1;
D in dom (D .--> D') by A3,TARSKI:def 1;then
h.D=(D .--> D').D by A9,FUNCT_4:44;
hence thesis by CQC_LANG:6;
end;
theorem Th2:
for A,B,C,D being set,h being Function, A',B',C',D' being set st
h = (B .--> B') +* (C .--> C') +* (D .--> D') +* (A .--> A')
holds dom h = {A,B,C,D}
proof
let A,B,C,D be set;
let h be Function;
let A',B',C',D' be set;
assume
A1:h = (B .--> B') +* (C .--> C') +* (D .--> D') +* (A .--> A');
dom ((B .--> B') +* (C .--> C'))
= dom (B .--> B') \/ dom (C .--> C') by FUNCT_4:def 2;
then A2: dom ((B .--> B') +* (C .--> C') +* (D .--> D'))
= dom (B .--> B') \/ dom (C .--> C') \/ dom (D .--> D') by FUNCT_4:def 2;
dom (B .--> B') = {B} by CQC_LANG:5;
then dom ((B .--> B') +* (C .--> C') +* (D .--> D') +* (A .--> A'))
= {B} \/ dom (C .--> C') \/ dom (D .--> D') \/
dom (A .--> A') by A2,FUNCT_4:def 2
.= {B} \/ {C} \/ dom (D .--> D') \/ dom (A .--> A') by CQC_LANG:5
.= {B} \/ {C} \/ {D} \/ dom (A .--> A') by CQC_LANG:5
.= {A} \/ (({B} \/ {C}) \/ {D}) by CQC_LANG:5
.= {A} \/ ({B,C} \/ {D}) by ENUMSET1:41
.= {A} \/ {B,C,D} by ENUMSET1:43
.= {A,B,C,D} by ENUMSET1:44;
hence thesis by A1;
end;
theorem Th3:
for h being Function,A',B',C',D' being set st G={A,B,C,D} &
h = (B .--> B') +* (C .--> C') +* (D .--> D') +* (A .--> A')
holds rng h = {h.A,h.B,h.C,h.D}
proof
let h be Function;
let A',B',C',D' be set;
assume
A1: G={A,B,C,D} & h = (B .--> B')+*(C .--> C')+*(D .--> D')+*(A .--> A');
then A2: dom h = G by Th2;
then A3: A in dom h by ENUMSET1:19,A1;
A4: B in dom h by ENUMSET1:19,A1,A2;
A5: C in dom h by ENUMSET1:19,A1,A2;
A6: D in dom h by ENUMSET1:19,A1,A2;
A7:rng h c= {h.A,h.B,h.C,h.D}
proof
let t be set;
assume t in rng h;
then consider x1 being set such that
A8: x1 in dom h & t = h.x1 by FUNCT_1:def 5;
now per cases by A8,A1,A2,ENUMSET1:18;
case x1=A;
hence thesis by A8,ENUMSET1:19;
case x1=B;
hence thesis by A8,ENUMSET1:19;
case x1=C;
hence thesis by A8,ENUMSET1:19;
case x1=D;
hence thesis by A8,ENUMSET1:19;
end;
hence thesis;
end;
{h.A,h.B,h.C,h.D} c= rng h
proof
let t be set;
assume A9: t in {h.A,h.B,h.C,h.D};
per cases by A9,ENUMSET1:18;
suppose t=h.A;
hence thesis by A3,FUNCT_1:def 5;
suppose t=h.B;
hence thesis by A4,FUNCT_1:def 5;
suppose t=h.C;
hence thesis by A5,FUNCT_1:def 5;
suppose t=h.D;
hence thesis by A6,FUNCT_1:def 5;
end;
hence thesis by XBOOLE_0:def 10,A7;
end;
theorem
for z,u being Element of Y, h being Function
st G is independent & G={A,B,C,D} & A<>B & A<>C & A<>D & B<>C & B<>D & C<>D
holds EqClass(u,B '/\' C '/\' D) meets EqClass(z,A)
proof
let z,u be Element of Y;
let h be Function;
assume A1:G is independent & G={A,B,C,D} &
A<>B & A<>C & A<>D & B<>C & B<>D & C<>D;
then A2: G is independent;
set h = (B .--> EqClass(u,B)) +* (C .--> EqClass(u,C)) +*
(D .--> EqClass(u,D)) +* (A .--> EqClass(z,A));
A3: dom h = G by A1,Th2;
A4: h.A = EqClass(z,A) by YELLOW14:3;
A5: h.B = EqClass(u,B) by Th1,A1;
A6: h.C = EqClass(u,C) by Th1,A1;
A7: h.D = EqClass(u,D) by Th1,A1;
A8: for d being set st d in G holds h.d in d
proof
let d be set;
assume A9: d in G;
per cases by A9,A1,ENUMSET1:18;
suppose A10:d=A;h.A=EqClass(z,A) by YELLOW14:3;
hence thesis by A10;
suppose A11:d=B;h.B=EqClass(u,B) by Th1,A1;
hence thesis by A11;
suppose A12:d=C;h.C=EqClass(u,C) by Th1,A1;
hence thesis by A12;
suppose A13:d=D;h.D=EqClass(u,D) by Th1,A1;
hence thesis by A13;
end;
A in dom h by ENUMSET1:19,A1,A3;then
A14: h.A in rng h by FUNCT_1:def 5;
B in dom h by ENUMSET1:19,A1,A3;then
A15: h.B in rng h by FUNCT_1:def 5;
C in dom h by ENUMSET1:19,A1,A3;then
A16: h.C in rng h by FUNCT_1:def 5;
D in dom h by ENUMSET1:19,A1,A3;then
A17: h.D in rng h by FUNCT_1:def 5;
A18:rng h = {h.A,h.B,h.C,h.D} by Th3,A1;
rng h c= bool Y
proof
let t be set;
assume A19: t in rng h;
per cases by A19,A18,ENUMSET1:18;
suppose t=h.A;then t=EqClass(z,A) by YELLOW14:3; hence thesis;
suppose t=h.B; hence thesis by A5;
suppose t=h.C; hence thesis by A6;
suppose t=h.D; hence thesis by A7;
end;then
reconsider FF=rng h as Subset-Family of Y by SETFAM_1:def 7;
Intersect FF <>{} by A2,BVFUNC_2:def 5,A3,A8;then
consider m being set such that
A20: m in Intersect FF by XBOOLE_0:def 1;
m in meet FF by A14,CANTOR_1:def 3,A20;then
A21: m in h.A & m in h.B & m in h.C & m in h.D
by A14,A15,A16,A17,SETFAM_1:def 1;
A22: EqClass(u,B '/\' C '/\' D) = EqClass(u,B '/\' C) /\ EqClass(u,D)
by BVFUNC14:1;
m in EqClass(u,B) /\ EqClass(u,C) by A21,A5,A6,XBOOLE_0:def 3;then
m in EqClass(u,B) /\ EqClass(u,C) /\ EqClass(u,D) by A21,A7
,XBOOLE_0:def 3;then
m in EqClass(u,B) /\ EqClass(u,C) /\ EqClass(u,D) /\ EqClass(z,A)
by A21,A4,XBOOLE_0:def 3;then
EqClass(u,B) /\ EqClass(u,C) /\ EqClass(u,D) meets EqClass(z,A) by XBOOLE_0:4
;
hence thesis by A22,BVFUNC14:1;
end;
theorem Th5:
for z,u being Element of Y
st G is independent & G={A,B,C,D} & A<>B & A<>C & A<>D & B<>C & B<>D & C<>D &
EqClass(z,C '/\' D)=EqClass(u,C '/\' D)
holds EqClass(u,CompF(A,G)) meets EqClass(z,CompF(B,G))
proof
let z,u be Element of Y;
assume A1:G is independent & G={A,B,C,D} &
A<>B & A<>C & A<>D & B<>C & B<>D & C<>D &
EqClass(z,C '/\' D)=EqClass(u,C '/\' D);
then A2: G is independent;
A3:CompF(B,G) = A '/\' C '/\' D by BVFUNC14:8,A1;
set H=EqClass(z,CompF(B,G));
set I=EqClass(z,A), GG=EqClass(u,B '/\' C '/\' D);
set h = (B .--> EqClass(u,B)) +* (C .--> EqClass(u,C)) +*
(D .--> EqClass(u,D)) +* (A .--> EqClass(z,A));
A4: dom h = G by A1,Th2;
A5: h.A = EqClass(z,A) by YELLOW14:3;
A6: h.B = EqClass(u,B) by Th1,A1;
A7: h.C = EqClass(u,C) by Th1,A1;
A8: h.D = EqClass(u,D) by Th1,A1;
A9: for d being set st d in G holds h.d in d
proof
let d be set;
assume A10: d in G;
per cases by A10,A1,ENUMSET1:18;
suppose A11:d=A; h.A=EqClass(z,A) by YELLOW14:3;
hence thesis by A11;
suppose A12:d=B; h.B=EqClass(u,B) by Th1,A1;
hence thesis by A12;
suppose A13:d=C; h.C=EqClass(u,C) by Th1,A1;
hence thesis by A13;
suppose A14:d=D; h.D=EqClass(u,D) by Th1,A1;
hence thesis by A14;
end;
A in dom h by ENUMSET1:19,A1,A4;then
A15: h.A in rng h by FUNCT_1:def 5;
B in dom h by ENUMSET1:19,A1,A4;then
A16: h.B in rng h by FUNCT_1:def 5;
C in dom h by ENUMSET1:19,A1,A4;then
A17: h.C in rng h by FUNCT_1:def 5;
D in dom h by ENUMSET1:19,A1,A4;then
A18: h.D in rng h by FUNCT_1:def 5;
A19:rng h = {h.A,h.B,h.C,h.D} by Th3,A1;
rng h c= bool Y
proof
let t be set;
assume A20: t in rng h;
per cases by A20,A19,ENUMSET1:18;
suppose t=h.A;then
t=EqClass(z,A) by YELLOW14:3;hence thesis;
suppose t=h.B;then
t=EqClass(u,B) by Th1,A1;hence thesis;
suppose t=h.C;then
t=EqClass(u,C) by Th1,A1;hence thesis;
suppose t=h.D;then
t=EqClass(u,D) by Th1,A1;hence thesis;
end;then
reconsider FF=rng h as Subset-Family of Y by SETFAM_1:def 7;
dom h=G & rng h=FF &
(for d being set st d in G holds h.d in d) by A1,Th2,A9;then
(Intersect FF)<>{} by A2,BVFUNC_2:def 5;then
consider m being set such that
A21: m in Intersect FF by XBOOLE_0:def 1;
m in meet FF by A15,CANTOR_1:def 3,A21;then
A22: m in h.A & m in h.B & m in h.C & m in h.D
by A15,A16,A17,A18,SETFAM_1:def 1;
A23: GG = EqClass(u,B '/\' C) /\ EqClass(u,D) by BVFUNC14:1;
m in EqClass(u,B) /\ EqClass(u,C) by A22,A6,A7,XBOOLE_0:def 3;then
m in EqClass(u,B) /\ EqClass(u,C) /\ EqClass(u,D) by A22,A8
,XBOOLE_0:def 3;then
m in EqClass(u,B) /\ EqClass(u,C) /\ EqClass(u,D) /\ EqClass(z,A)
by A22,A5,XBOOLE_0:def 3;then
GG /\ I <> {} by A23,BVFUNC14:1;then
consider p being set such that
A24: p in GG /\ I by XBOOLE_0:def 1;
reconsider p as Element of Y by A24;
set K=EqClass(p,C '/\' D);
A25:p in K & K in C '/\' D by T_1TOPSP:def 1;
A26: p in GG & p in I by A24,XBOOLE_0:def 3;then
p in I /\ K by A25,XBOOLE_0:def 3;
then I /\ K in INTERSECTION(A,C '/\' D) & not (I /\ K in {{}})
by TARSKI:def 1,SETFAM_1:def 5;then
A27: I /\ K in INTERSECTION(A,C '/\' D) \ {{}} by XBOOLE_0:def 4;
set L=EqClass(z,C '/\' D);
GG = EqClass(u,B '/\' (C '/\' D)) by PARTIT1:16;then
A28: GG c= EqClass(u,C '/\' D) by BVFUNC11:3;
A29: p in GG by A24,XBOOLE_0:def 3;
p in EqClass(p,C '/\' D) by T_1TOPSP:def 1;then
K meets L by A29,A28,A1,XBOOLE_0:3;then
K=L by T_1TOPSP:9;
then A30:z in K by T_1TOPSP:def 1;
z in I by T_1TOPSP:def 1;then
A31:z in I /\ K by XBOOLE_0:def 3,A30;
A32:z in H by T_1TOPSP:def 1;
A '/\' (C '/\' D) = A '/\' C '/\' D by PARTIT1:16;then
I /\ K in CompF(B,G) by A27,PARTIT1:def 4,A3;
then I /\ K = H or I /\ K misses H by EQREL_1:def 6;then
p in H by A26,A25,XBOOLE_0:def 3,A32,A31,XBOOLE_0:3;then
p in GG /\ H by A29,XBOOLE_0:def 3;then
GG meets H by XBOOLE_0:4;
hence thesis by BVFUNC14:7,A1;
end;
begin
canceled 14;
theorem
G is independent & G={A,B,C,D} & A<>B & A<>C & A<>D & B<>C & B<>D & C<>D
implies Ex('not' All(a,A,G),B,G) '<' 'not' All(All(a,B,G),A,G)
proof
assume A1:G is independent & G={A,B,C,D} &
A<>B & A<>C & A<>D & B<>C & B<>D & C<>D;
A2:All(a,A,G) = B_INF(a,CompF(A,G)) by BVFUNC_2:def 9;
A3:Ex('not' All(a,A,G),B,G) = B_SUP('not'
All(a,A,G),CompF(B,G)) by BVFUNC_2:def 10;
let z be Element of Y;
assume A4:Pj(Ex('not' All(a,A,G),B,G),z)=TRUE;
now assume
not (ex x being Element of Y st
x in EqClass(z,CompF(B,G)) & Pj('not' All(a,A,G),x)=TRUE);then
Pj(B_SUP('not' All(a,A,G),CompF(B,G)),z) = FALSE by BVFUNC_1:def 20;
hence contradiction by A4,MARGREL1:43,A3;
end;then
consider x1 being Element of Y such that
A5: x1 in EqClass(z,CompF(B,G)) & Pj('not' All(a,A,G),x1)=TRUE;
'not' Pj(All(a,A,G),x1)=TRUE by A5,VALUAT_1:def 5;then
A6:Pj(All(a,A,G),x1)=FALSE by MARGREL1:41;
now assume
for x being Element of Y st x in EqClass(x1,CompF(A,G)) holds
Pj(a,x)=TRUE;then
Pj(B_INF(a,CompF(A,G)),x1) = TRUE by BVFUNC_1:def 19;
hence contradiction by A6,MARGREL1:43,A2;
end;then
consider x2 being Element of Y such that
A7: x2 in EqClass(x1,CompF(A,G)) & Pj(a,x2)<>TRUE;
A8:B '/\' C '/\' D = B '/\' (C '/\' D) by PARTIT1:16;
A9:A '/\' C '/\' D = A '/\' (C '/\' D) by PARTIT1:16;
A10:CompF(A,G) = B '/\' C '/\' D by BVFUNC14:7,A1;
A11: CompF(B,G) = A '/\' C '/\' D by BVFUNC14:8,A1;
A12:EqClass(z,A '/\' C '/\' D) c= EqClass(z,C '/\' D) by BVFUNC11:3,A9;
A13:EqClass(x1,B '/\' C '/\' D) c= EqClass(x1,C '/\' D) by BVFUNC11:3,A8;
A14:x1 in EqClass(x1,C '/\' D) & EqClass(x1,C '/\' D) in C '/\' D
by T_1TOPSP:def 1;
A15:x2 in EqClass(x2,C '/\' D) & EqClass(x2,C '/\' D) in C '/\' D
by T_1TOPSP:def 1;
EqClass(z,C '/\' D) meets EqClass(x1,C '/\' D)
by A5,A12,A11,A14,XBOOLE_0:3;then
A16:EqClass(z,C '/\' D) = EqClass(x1,C '/\' D) by T_1TOPSP:9;
EqClass(x1,C '/\' D) meets EqClass(x2,C '/\' D)
by A7,A13,A10,A15,XBOOLE_0:3;then
EqClass(z,C '/\' D)=EqClass(x2,C '/\' D) by A16,T_1TOPSP:9;then
EqClass(z,CompF(A,G)) meets EqClass(x2,CompF(B,G)) by Th5,A1;then
consider t being set such that
A17: t in EqClass(z,CompF(A,G)) /\ EqClass(x2,CompF(B,G)) by XBOOLE_0:4;
A18:t in EqClass(z,CompF(A,G)) & t in EqClass(x2,CompF(B,G))
by XBOOLE_0:def 3,A17;
reconsider t as Element of Y by A17;
A19:x2 in EqClass(x2,CompF(B,G)) & EqClass(x2,CompF(B,G)) in CompF(B,G) &
t in EqClass(t,CompF(B,G)) & EqClass(t,CompF(B,G)) in CompF(B,G)
by T_1TOPSP:def 1;
then EqClass(x2,CompF(B,G)) meets EqClass(t,CompF(B,G))
by XBOOLE_0:3,A18;then
x2 in EqClass(t,CompF(B,G)) by A19,EQREL_1:def 6;
then Pj(B_INF(a,CompF(B,G)),t) = FALSE by BVFUNC_1:def 19,A7;then
Pj(All(a,B,G),t)=FALSE by BVFUNC_2:def 9;then
Pj(All(a,B,G),t)<>TRUE by MARGREL1:43;then
Pj(B_INF(All(a,B,G),CompF(A,G)),z) = FALSE by A18,BVFUNC_1:def 19;then
Pj(All(All(a,B,G),A,G),z)=FALSE by BVFUNC_2:def 9;then
'not' Pj(All(All(a,B,G),A,G),z)=TRUE by MARGREL1:41;
hence thesis by VALUAT_1:def 5;
end;
canceled 2;
theorem
G is independent & G={A,B,C,D} & A<>B & A<>C & A<>D & B<>C & B<>D & C<>D
implies Ex(Ex('not' a,A,G),B,G) '<' 'not' All(All(a,B,G),A,G)
proof
assume A1:G is independent & G={A,B,C,D} &
A<>B & A<>C & A<>D & B<>C & B<>D & C<>D;
A2:Ex(Ex('not' a,A,G),B,G) = B_SUP(Ex('not'
a,A,G),CompF(B,G)) by BVFUNC_2:def 10;
let z be Element of Y;
assume A3:Pj(Ex(Ex('not' a,A,G),B,G),z)=TRUE;
now assume
not (ex x being Element of Y st
x in EqClass(z,CompF(B,G)) & Pj(Ex('not' a,A,G),x)=TRUE);then
Pj(B_SUP(Ex('not' a,A,G),CompF(B,G)),z) = FALSE by BVFUNC_1:def 20;
hence contradiction by A3,MARGREL1:43,A2;
end;then
consider x1 being Element of Y such that
A4: x1 in EqClass(z,CompF(B,G)) & Pj(Ex('not' a,A,G),x1)=TRUE;
now assume
not (ex x being Element of Y st
x in EqClass(x1,CompF(A,G)) & Pj('not' a,x)=TRUE);then
Pj(B_SUP('not' a,CompF(A,G)),x1) = FALSE by BVFUNC_1:def 20;then
Pj(Ex('not' a,A,G),x1)=FALSE by BVFUNC_2:def 10;
hence contradiction by A4,MARGREL1:43;
end;then
consider x2 being Element of Y such that
A5: x2 in EqClass(x1,CompF(A,G)) & Pj('not' a,x2)=TRUE;
'not' Pj(a,x2)=TRUE by A5,VALUAT_1:def 5;then
Pj(a,x2)=FALSE by MARGREL1:41;then
A6:Pj(a,x2)<>TRUE by MARGREL1:43;
A7:B '/\' C '/\' D = B '/\' (C '/\' D) by PARTIT1:16;
A8:A '/\' C '/\' D = A '/\' (C '/\' D) by PARTIT1:16;
A9:CompF(A,G) = B '/\' C '/\' D by BVFUNC14:7,A1;
A10: CompF(B,G) = A '/\' C '/\' D by BVFUNC14:8,A1;
A11:EqClass(z,A '/\' C '/\' D) c= EqClass(z,C '/\' D) by BVFUNC11:3,A8;
A12:EqClass(x1,B '/\' C '/\' D) c= EqClass(x1,C '/\' D) by BVFUNC11:3,A7;
A13:x1 in EqClass(x1,C '/\' D) & EqClass(x1,C '/\' D) in C '/\' D
by T_1TOPSP:def 1;
A14:x2 in EqClass(x2,C '/\' D) & EqClass(x2,C '/\' D) in C '/\' D
by T_1TOPSP:def 1;
EqClass(z,C '/\' D) meets EqClass(x1,C '/\' D)
by A4,A11,A10,A13,XBOOLE_0:3;then
A15:EqClass(z,C '/\' D) = EqClass(x1,C '/\' D) by T_1TOPSP:9;
EqClass(x1,C '/\' D) meets EqClass(x2,C '/\' D)
by A5,A12,A9,A14,XBOOLE_0:3;then
EqClass(z,C '/\' D)=EqClass(x2,C '/\' D) by A15,T_1TOPSP:9;then
EqClass(z,CompF(A,G)) meets EqClass(x2,CompF(B,G)) by Th5,A1;then
consider t being set such that
A16: t in EqClass(z,CompF(A,G)) /\ EqClass(x2,CompF(B,G)) by XBOOLE_0:4;
A17:t in EqClass(z,CompF(A,G)) & t in EqClass(x2,CompF(B,G))
by XBOOLE_0:def 3,A16;
reconsider t as Element of Y by A16;
A18:x2 in EqClass(x2,CompF(B,G)) & EqClass(x2,CompF(B,G)) in CompF(B,G) &
t in EqClass(t,CompF(B,G)) & EqClass(t,CompF(B,G)) in CompF(B,G)
by T_1TOPSP:def 1;
then EqClass(x2,CompF(B,G)) meets EqClass(t,CompF(B,G))
by XBOOLE_0:3,A17;then
x2 in EqClass(t,CompF(B,G)) by A18,EQREL_1:def 6;
then Pj(B_INF(a,CompF(B,G)),t) = FALSE by BVFUNC_1:def 19,A6;then
Pj(All(a,B,G),t)=FALSE by BVFUNC_2:def 9;then
Pj(All(a,B,G),t)<>TRUE by MARGREL1:43;then
Pj(B_INF(All(a,B,G),CompF(A,G)),z) = FALSE by A17,BVFUNC_1:def 19;then
Pj(All(All(a,B,G),A,G),z)=FALSE by BVFUNC_2:def 9;then
'not' Pj(All(All(a,B,G),A,G),z)=TRUE by MARGREL1:41;
hence thesis by VALUAT_1:def 5;
end;