The Mizar article:

Four Variable Predicate Calculus for Boolean Valued Functions. Part I

by
Shunichi Kobayashi

Received November 26, 1999

Copyright (c) 1999 Association of Mizar Users

MML identifier: BVFUNC20
[ MML identifier index ]


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;

Back to top