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;