:: Classes of Independent Partitions
::  by Andrzej Trybulec
::
:: Received February 14, 2001
:: Copyright (c) 2001-2012 Association of Mizar Users
::           (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland).
:: This code can be distributed under the GNU General Public Licence
:: version 3.0 or later, or the Creative Commons Attribution-ShareAlike
:: License version 3.0 or later, subject to the binding interpretation
:: detailed in file COPYING.interpretation.
:: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these
:: licenses, or see http://www.gnu.org/licenses/gpl.html and
:: http://creativecommons.org/licenses/by-sa/3.0/.

environ

 vocabularies XBOOLE_0, SUBSET_1, FUNCT_2, MARGREL1, PARTIT1, EQREL_1, FUNCT_1,
      SETFAM_1, RELAT_1, ZFMISC_1, TARSKI, RELAT_2, XBOOLEAN, BVFUNC_2,
      BVFUNC_1, FUNCT_4, FUNCT_5, OPOSET_1, BINOP_1;
 notations TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, SETFAM_1, MARGREL1, RELAT_1,
      RELAT_2, FUNCT_1, RELSET_1, FUNCT_2, BINOP_1, FUNCT_4, FUNCT_5, EQREL_1,
      PARTIT1, BVFUNC_1, BVFUNC_2;
 constructors SETFAM_1, FUNCT_4, XCMPLX_0, BVFUNC_1, BVFUNC_2, RELSET_1,
      FUNCT_5, RELAT_2, DOMAIN_1, BINOP_1;
 registrations SUBSET_1, RELAT_1, FUNCT_1, PARTFUN1, EQREL_1, MARGREL1,
      PARTIT1, RELSET_1, XBOOLE_0, FUNCT_2;
 requirements SUBSET, BOOLE, ARITHM;
 definitions BVFUNC_1, TARSKI, RELAT_2, XBOOLE_0, XBOOLEAN, RELSET_1, EQREL_1;
 theorems TARSKI, FUNCT_1, FUNCT_2, BVFUNC_1, BVFUNC_2, RELSET_1, PARTIT1,
      SETFAM_1, SUBSET_1, FUNCT_4, RELAT_1, EQREL_1, RELAT_2, XBOOLE_0,
      XBOOLE_1, PARTFUN1, ORDERS_1, XBOOLEAN, MARGREL1, CARD_1, ZFMISC_1,
      XTUPLE_0;
 schemes FUNCT_2;

begin :: Preliminaries

reserve Y for non empty set,
  a for Function of Y,BOOLEAN,
  G for Subset of PARTITIONS(Y),
  P,Q for a_partition of Y;

definition
  let Y be non empty set, G be non empty Subset of PARTITIONS Y;
  redefine mode Element of G -> a_partition of Y;
  coherence
  proof
    let p be Element of G;
    thus thesis by PARTIT1:def 3;
  end;
end;

theorem Th1:
  '/\' {} PARTITIONS Y = %O Y
proof
  for x being set holds x in %O Y iff ex h being Function, F being
Subset-Family of Y st dom h={} PARTITIONS Y & rng h = F & (for d being set st d
  in {} PARTITIONS Y holds h.d in d) & x=Intersect F & x<>{}
  proof
    let x be set;
    hereby
      reconsider h = {} as Function;
      assume x in %O Y;
      then
A1:   x in {Y} by PARTIT1:def 8;
      take h,F = {}bool Y;
      thus dom h={} PARTITIONS Y;
      thus rng h = F;
      thus for d being set st d in {} PARTITIONS Y holds h.d in d;
      x = Y by A1,TARSKI:def 1;
      hence x=Intersect F by SETFAM_1:def 9;
      thus x<>{} by A1,TARSKI:def 1;
    end;
    given h being Function, F being Subset-Family of Y such that
A2: dom h={} PARTITIONS Y & rng h = F and
    for d being set st d in {} PARTITIONS Y holds h.d in d and
A3: x=Intersect F and
    x<>{};
    F = {} by A2,RELAT_1:42;
    then x = Y by A3,SETFAM_1:def 9;
    then x in {Y} by TARSKI:def 1;
    hence thesis by PARTIT1:def 8;
  end;
  hence thesis by BVFUNC_2:def 1;
end;

theorem Th2:
  for R,S being Equivalence_Relation of Y holds R \/ S c= R*S
proof
  let R,S be Equivalence_Relation of Y;
  let x,y be Element of Y;
  assume
A1: [x,y] in R \/ S;
  per cases by A1,XBOOLE_0:def 3;
  suppose
A2: [x,y] in R;
    [y,y] in S by EQREL_1:5;
    hence thesis by A2,RELAT_1:def 8;
  end;
  suppose
A3: [x,y] in S;
    [x,x] in R by EQREL_1:5;
    hence thesis by A3,RELAT_1:def 8;
  end;
end;

theorem
  for R being Relation of Y holds R c= nabla Y;

theorem Th4:
  for R being Equivalence_Relation of Y holds (nabla Y)*R = nabla Y
  & R*nabla Y = nabla Y
proof
  let R being Equivalence_Relation of Y;
  (nabla Y) \/ R c= (nabla Y)*R by Th2;
  then nabla Y c= (nabla Y)*R by EQREL_1:1;
  hence (nabla Y)*R = nabla Y by XBOOLE_0:def 10;
  (nabla Y) \/ R c= R*nabla Y by Th2;
  then nabla Y c= R*nabla Y by EQREL_1:1;
  hence thesis by XBOOLE_0:def 10;
end;

theorem Th5:
  for P being a_partition of Y, x,y being Element of Y holds [x,y]
  in ERl P iff x in EqClass(y,P)
proof
  let P be a_partition of Y, x,y be Element of Y;
  hereby
    assume [x,y] in ERl P;
    then ex A being Subset of Y st A in P & x in A & y in A by PARTIT1:def 6;
    hence x in EqClass(y,P) by EQREL_1:def 6;
  end;
  y in EqClass(y,P) by EQREL_1:def 6;
  hence thesis by PARTIT1:def 6;
end;

theorem
  for P,Q,R being a_partition of Y st ERl(R) = ERl(P)*ERl(Q) for x,y
being Element of Y holds x in EqClass(y,R) iff ex z being Element of Y st x in
  EqClass(z,P) & z in EqClass(y,Q)
proof
  let P,Q,R be a_partition of Y such that
A1: ERl(R) = ERl(P)*ERl(Q);
  let x,y be Element of Y;
  hereby
    assume x in EqClass(y,R);
    then [x,y] in ERl R by Th5;
    then consider z being Element of Y such that
A2: [x,z] in ERl P and
A3: [z,y] in ERl Q by A1,RELSET_1:28;
    take z;
    thus x in EqClass(z,P) by A2,Th5;
    thus z in EqClass(y,Q) by A3,Th5;
  end;
  given z being Element of Y such that
A4: x in EqClass(z,P) & z in EqClass(y,Q);
  [x,z] in ERl P & [z,y] in ERl Q by A4,Th5;
  then [x,y] in ERl R by A1,RELAT_1:def 8;
  hence thesis by Th5;
end;

theorem Th7:
  for R,S being Relation, Y being set st R is_reflexive_in Y &
  S is_reflexive_in Y holds R*S is_reflexive_in Y
proof
  let R,S be Relation, Y be set such that
A1: R is_reflexive_in Y & S is_reflexive_in Y;
  let x be set;
  assume x in Y;
  then [x,x] in R & [x,x] in S by A1,RELAT_2:def 1;
  hence thesis by RELAT_1:def 8;
end;

theorem Th8:
  for R being Relation, Y being set st R is_reflexive_in Y holds Y c= field R
proof
  let R be Relation, Y be set such that
A1: R is_reflexive_in Y;
  let x be set;
  assume x in Y;
  then [x,x] in R by A1,RELAT_2:def 1;
  hence thesis by RELAT_1:15;
end;

theorem Th9:
  for Y being set, R being Relation of Y st R is_reflexive_in Y holds
    Y = field R
proof
  let Y be set, R be Relation of Y;
  assume R is_reflexive_in Y;
  hence Y c= field R by Th8;
  field R c= Y \/ Y by RELSET_1:8;
  hence thesis;
end;

theorem
  for R,S being Equivalence_Relation of Y st R*S = S*R holds
  R*S is Equivalence_Relation of Y
proof
  let R,S be Equivalence_Relation of Y such that
A1: R*S = S*R;
A2: field S = Y by ORDERS_1:12;
  then
A3: S is_reflexive_in Y by RELAT_2:def 9;
A4: field R = Y by ORDERS_1:12;
  then R is_reflexive_in Y by RELAT_2:def 9;
  then R*S is_reflexive_in Y by A3,Th7;
  then
A5: field (R*S) = Y & dom(R*S) = Y by ORDERS_1:13;
A6: R*S is_symmetric_in Y
  proof
A7: S is_symmetric_in Y by A2,RELAT_2:def 11;
    let x,y be set such that
A8: x in Y and
A9: y in Y;
    assume [x,y] in R*S;
    then consider z being set such that
A10: [x,z] in R and
A11: [z,y] in S by RELAT_1:def 8;
    z in field S by A11,RELAT_1:15;
    then
A12: [y,z] in S by A2,A7,A9,A11,RELAT_2:def 3;
A13: R is_symmetric_in Y by A4,RELAT_2:def 11;
    z in field R by A10,RELAT_1:15;
    then [z,x] in R by A4,A13,A8,A10,RELAT_2:def 3;
    hence thesis by A1,A12,RELAT_1:def 8;
  end;
A14: R*R c= R & S*S c= S by RELAT_2:27;
  R*S*(R*S) = R*S*R*S by RELAT_1:36
    .= R*(R*S)*S by A1,RELAT_1:36
    .= R*R*S*S by RELAT_1:36
    .= R*R*(S*S) by RELAT_1:36;
  then R*S*(R*S) c= R*S by A14,RELAT_1:31;
  hence thesis by A5,A6,PARTFUN1:def 2,RELAT_2:27,def 11;
end;

begin :: Boolean-valued Functions

theorem Th11:
  for a,b being Function of Y,BOOLEAN st a '<' b holds
  'not' b '<' 'not' a
proof
  let a,b being Function of Y,BOOLEAN such that
A1: a '<' b;
  let x be Element of Y;
  assume
A2: ('not' b).x= TRUE;
  b.x = ('not' 'not' b).x .= 'not' TRUE by A2,MARGREL1:def 19
    .= FALSE;
  then a.x <> TRUE by A1,BVFUNC_1:def 12;
  then a.x = FALSE by XBOOLEAN:def 3;
  hence ('not' a).x = 'not' FALSE by MARGREL1:def 19
    .=TRUE;
end;

theorem Th12:
  for a,b being Function of Y,BOOLEAN, G being Subset of PARTITIONS(Y),
      P being a_partition of Y st a '<' b holds All(a,P,G) '<' All(b,P,G)
proof
  let a,b be Function of Y,BOOLEAN, G be Subset of PARTITIONS(Y), P be
  a_partition of Y such that
A1: a '<' b;
  let x be Element of Y;
  assume
A2: All(a,P,G).x= TRUE;
A3: All(a,P,G) = B_INF(a,CompF(P,G)) by BVFUNC_2:def 9;
A4: for y being Element of Y st y in EqClass(x,CompF(P,G)) holds b.y=TRUE
  proof
    let y be Element of Y;
    assume y in EqClass(x,CompF(P,G));
    then a.y=TRUE by A3,A2,BVFUNC_1:def 16;
    hence thesis by A1,BVFUNC_1:def 12;
  end;
  All(b,P,G) = B_INF(b,CompF(P,G)) by BVFUNC_2:def 9;
  hence thesis by A4,BVFUNC_1:def 16;
end;

theorem
  for a,b being Function of Y,BOOLEAN,
      G being Subset of PARTITIONS(Y), P being a_partition of Y st
    a '<' b holds Ex(a,P,G) '<' Ex(b,P,G)
proof
  let a,b be Function of Y,BOOLEAN, G be Subset of PARTITIONS(Y), P be
  a_partition of Y;
A1: Ex(b,P,G) = Ex('not' 'not' b,P,G) .= 'not' All('not' b,P,G) by BVFUNC_2:18;
  assume a '<' b;
  then 'not' b '<' 'not' a by Th11;
  then
A2: All('not' b,P,G) '<' All('not' a,P,G) by Th12;
  Ex(a,P,G) = Ex('not' 'not' a,P,G) .= 'not' All('not' a,P,G) by BVFUNC_2:18;
  hence thesis by A1,A2,Th11;
end;

begin :: Independent Families of Partitions

Lm1: G is independent implies for P,Q being Subset of PARTITIONS Y st P c= G &
Q c= G holds ERl('/\'P)*ERl('/\'Q) c= ERl('/\'Q)*ERl('/\'P)
proof
  assume
A1: G is independent;
  let P,Q be Subset of PARTITIONS Y such that
A2: P c= G and
A3: Q c= G;
  per cases;
  suppose
    P = {};
    then P = {} PARTITIONS Y;
    then ERl('/\'Q)*ERl('/\'P) = ERl('/\'Q)*ERl(%O Y) by Th1
      .= ERl('/\'Q)*nabla Y by PARTIT1:33
      .= nabla Y by Th4;
    hence thesis;
  end;
  suppose Q = {}; then
 Q = {} PARTITIONS Y;
    then ERl('/\'Q)*ERl('/\'P)= ERl(%O Y)*ERl('/\'P) by Th1
      .= (nabla Y)*ERl('/\'P) by PARTIT1:33
      .= nabla Y by Th4;
    hence thesis;
  end;
  suppose
A4: P <> {} & Q <> {};
    then reconsider G9 = G as non empty Subset of PARTITIONS(Y) by A2;
    let x,y be Element of Y;
    assume [x,y] in ERl('/\'P)*ERl('/\'Q);
    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 A5,PARTIT1:def 6;
    consider B being Subset of Y such that
A10: B in '/\'Q and
A11: z in B and
A12: y in B by A6,PARTIT1:def 6;
    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 A10,BVFUNC_2:def 1;
    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 A7,BVFUNC_2:def 1;
    reconsider P, Q as non empty Subset of PARTITIONS Y by A4;
    deffunc P(Element of P) = EqClass(y,$1);
    consider hP9 being Function of P, bool Y such that
A19: for p being Element of P holds hP9.p = P(p) from FUNCT_2:sch 4;
    deffunc Q(Element of Q) = EqClass(x,$1);
    consider hQ9 being Function of Q, bool Y such that
A20: for p being Element of Q holds hQ9.p = Q(p) from FUNCT_2:sch 4;
    deffunc P(set) = $1;
A21: for d being Element of G9 holds bool Y meets P(d)
    proof
      let d be Element of G9;
      d meets d;
      hence bool Y meets d by XBOOLE_1:63;
    end;
    consider h9 being Function of G9, bool Y such that
A22: for d being Element of G9 holds h9.d in P(d) from FUNCT_2:sch
10(A21);
    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 h.d = hP9.d
    proof
      let d be set;
      assume
A26:  d in P;
      then reconsider d9 = d as Element of P;
      per cases;
      suppose
A27:    d in Q;
        then
A28:    hQ.d in FQ by A13,FUNCT_1:def 3; then
A29:    y in hQ.d by A12,A15,SETFAM_1:43;
A30:    z in hQ.d by A11,A15,A28,SETFAM_1:43;
A31:    hQ.d in d by A14,A27;
A32:    hP.d in FP by A16,A26,FUNCT_1:def 3; then
A33:    x in hP.d by A8,A18,SETFAM_1:43;
A34:    z in hP.d by A9,A18,A32,SETFAM_1:43;
A35:    hP.d in d by A17,A26;
        thus h.d = hQ9.d by A23,A27,FUNCT_4:13
          .= EqClass(x,d9) by A20,A27
          .= hP.d by A35,A33,EQREL_1:def 6
          .= EqClass(z,d9) by A35,A34,EQREL_1:def 6
          .= hQ.d by A31,A30,EQREL_1:def 6
          .= EqClass(y,d9) by A31,A29,EQREL_1:def 6
          .= hP9.d by A19;
      end;
      suppose
        not d in Q;
        hence h.d = (h9 +* hP9).d by A23,FUNCT_4:11
          .= hP9.d by A24,A26,FUNCT_4:13;
      end;
    end;
    reconsider FP9 = rng hP9, FQ9 = rng hQ9 as Subset-Family of Y;
    set A9 = Intersect FP9, B9 = Intersect FQ9;
    for a being set st a in FP9 holds y in a
    proof
      let a be set;
      assume a in FP9;
      then consider b being set such that
A36:  b in dom hP9 and
A37:  hP9.b = a by FUNCT_1:def 3;
      reconsider b as Element of P by A36;
      a = EqClass(y,b) by A19,A37;
      hence thesis by EQREL_1:def 6;
    end;
    then
A38: y in A9 by SETFAM_1:43;
    for a being set st a in FQ9 holds x in a
    proof
      let a be set;
      assume a in FQ9;
      then consider b being set such that
A39:  b in dom hQ9 and
A40:  hQ9.b = a by FUNCT_1:def 3;
      reconsider b as Element of Q by A39;
      a = EqClass(x,b) by A20,A40;
      hence thesis by EQREL_1:def 6;
    end;
    then
A41: x in B9 by SETFAM_1:43;
A42: for d being set st d in Q holds hQ9.d in d
    proof
      let d be set;
      assume d in Q;
      then reconsider d as Element of Q;
      hQ9.d = EqClass(x,d) by A20;
      hence thesis;
    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 h c= rng(h9 +* hP9) \/ rng hQ9 & rng(h9 +* hP9) \/ rng hQ9 c=
    bool Y by FUNCT_4:17,XBOOLE_1:8;
    then reconsider F = rng h as Subset-Family of Y by XBOOLE_1:1;
A43: dom h = dom(h9 +* hP9) \/ Q by A23,FUNCT_4:def 1
      .= dom h9 \/ P \/ Q by A24,FUNCT_4:def 1
      .= G \/ P \/ Q by FUNCT_2:def 1
      .= G \/ Q by A2,XBOOLE_1:12
      .= G by A3,XBOOLE_1:12;
A44: for d being set st d in P holds hP9.d in d
    proof
      let d be set;
      assume d in P;
      then reconsider d as Element of P;
      hP9.d = EqClass(y,d) by A19;
      hence thesis;
    end;
    for d being set st d in G holds h.d in d
    proof
      let d be set;
      assume
A45:  d in G;
      G = P \/ Q \/ G by A2,A3,XBOOLE_1:8,12
        .= G \ (P \/ Q) \/ (P \/ Q) by XBOOLE_1:39;
      then
A46:  d in G \ (P \/ Q) or d in P \/ Q by A45,XBOOLE_0:def 3;
      per cases by A46,XBOOLE_0:def 3;
      suppose
A47:    d in Q;
        then h.d = hQ9.d by A23,FUNCT_4:13;
        hence thesis by A42,A47;
      end;
      suppose
A48:    d in P;
        then h.d = hP9.d by A25;
        hence thesis by A44,A48;
      end;
      suppose
A49:    d in G \ (P \/ Q);
        then not d in (P \/ Q) by XBOOLE_0:def 5;
        then h = h9 +* (hP9 +* hQ9) & not d in dom(hP9 +* hQ9) by A24,A23,
FUNCT_4:14,def 1; then
A50:    h.d = h9.d by FUNCT_4:11;
        d in G by A49,XBOOLE_0:def 5;
        hence thesis by A22,A50;
      end;
    end;
    then Intersect F <> {} by A1,A43,BVFUNC_2:def 5;
    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;
      assume a in FP9;
      then consider b being set such that
A52:  b in dom hP9 and
A53:  hP9.b = a by FUNCT_1:def 3;
      hP9.b = h.b by A25,A52;
      then a in F by A2,A24,A43,A52,A53,FUNCT_1:def 3;
      hence thesis by A51,SETFAM_1:43;
    end;
    then
A54: t in A9 by SETFAM_1:43;
    then A9 in '/\'P by A44,A24,BVFUNC_2:def 1;
    then
A55: [t,y] in ERl('/\'P) by A38,A54,PARTIT1:def 6;
    for a being set st a in FQ9 holds t in a
    proof
      let a be set;
      assume a in FQ9;
      then consider b being set such that
A56:  b in dom hQ9 and
A57:  hQ9.b = a by FUNCT_1:def 3;
      reconsider b as Element of Q by A56;
      hQ9.b = h.b by A56,FUNCT_4:13;
      then a in F by A3,A23,A43,A56,A57,FUNCT_1:def 3;
      hence thesis by A51,SETFAM_1:43;
    end;
    then
A58: t in B9 by SETFAM_1:43;
    then B9 in '/\'Q by A42,A23,BVFUNC_2:def 1;
    then [x,t] in ERl('/\'Q) by A41,A58,PARTIT1:def 6;
    hence thesis by A55,RELSET_1:28;
  end;
end;

theorem Th14:
  G is independent implies for P,Q being Subset of PARTITIONS Y st
  P c= G & Q c= G holds ERl('/\'P)*ERl('/\'Q) = ERl('/\'Q)*ERl('/\'P)
proof
  assume
A1: G is independent;
  let P,Q be Subset of PARTITIONS Y;
  assume P c= G & Q c= G;
  then ERl('/\'P)*ERl('/\'Q) c= ERl('/\'Q)*ERl('/\'P) & ERl('/\'Q)*ERl('/\'P)
  c= ERl('/\'P)*ERl('/\'Q) by A1,Lm1;
  hence thesis by XBOOLE_0:def 10;
end;

theorem Th15:
  G is independent implies All(All(a,P,G),Q,G) = All(All(a,Q,G),P,G)
proof
  set A = G \ {P}, B = G \ {Q};
A1: CompF(P,G) = '/\' A by BVFUNC_2:def 7;
A2: A c= G & B c= G by XBOOLE_1:36;
A3: CompF(Q,G) = '/\' B by BVFUNC_2:def 7;
  assume G is independent;
  then
A4: ERl('/\'A)*ERl '/\'B = ERl ('/\'B)*ERl '/\'A by A2,Th14;
A5: for y being Element of Y holds ( (for x being Element of Y st x in
EqClass(y,CompF(Q,G)) holds B_INF(a,CompF(P,G)).x=TRUE) implies B_INF( B_INF(a,
  CompF(Q,G)),CompF(P,G)).y = TRUE ) & (not (for x being Element of Y st x in
EqClass(y,CompF(Q,G)) holds B_INF(a,CompF(P,G)).x=TRUE) implies B_INF( B_INF(a,
  CompF(Q,G)),CompF(P,G)).y = FALSE)
  proof
    let y be Element of Y;
    hereby
      assume
A6:   for x being Element of Y st x in EqClass(y,CompF(Q,G)) holds
      B_INF(a,CompF(P,G)).x=TRUE;
      for x being Element of Y st x in EqClass(y,CompF(P,G)) holds B_INF(a
      ,CompF(Q,G)).x=TRUE
      proof
        let x be Element of Y;
        assume x in EqClass(y,CompF(P,G)); then
A7:     [x,y] in ERl '/\' A by A1,Th5;
        for z being Element of Y st z in EqClass(x,CompF(Q,G)) holds a.z= TRUE
        proof
          let z be Element of Y;
          assume z in EqClass(x,CompF(Q,G));
          then [z,x] in ERl '/\' B by A3,Th5;
          then [z,y] in (ERl '/\' A)*ERl '/\' B by A4,A7,RELAT_1:def 8;
          then consider u being set such that
A8:       [z,u] in ERl '/\' A and
A9:       [u,y] in ERl '/\' B by RELAT_1:def 8;
          u in field ERl '/\' B by A9,RELAT_1:15;
          then reconsider u as Element of Y by ORDERS_1:12;
          u in EqClass(y,CompF(Q,G)) by A3,A9,Th5;
          then
A10:      B_INF(a,CompF(P,G)).u <> FALSE by A6;
          z in EqClass(u,CompF(P,G)) by A1,A8,Th5;
          hence thesis by A10,BVFUNC_1:def 16;
        end;
        hence thesis by BVFUNC_1:def 16;
      end;
      hence B_INF(B_INF(a,CompF(Q,G)),CompF(P,G)).y = TRUE by BVFUNC_1:def 16;
    end;
    given x being Element of Y such that
A11: x in EqClass(y,CompF(Q,G)) and
A12: B_INF(a,CompF(P,G)).x <> TRUE;
    consider z being Element of Y such that
A13: z in EqClass(x,CompF(P,G)) and
A14: a.z <> TRUE by A12,BVFUNC_1:def 16;
A15: [x,y] in ERl '/\' B by A3,A11,Th5;
    [z,x] in ERl '/\' A by A1,A13,Th5;
    then [z,y] in (ERl '/\' B)*ERl '/\' A by A4,A15,RELAT_1:def 8;
    then consider u being set such that
A16: [z,u] in ERl '/\' B and
A17: [u,y] in ERl '/\' A by RELAT_1:def 8;
    u in field ERl '/\' B by A16,RELAT_1:15;
    then reconsider u as Element of Y by ORDERS_1:12;
    z in EqClass(u,CompF(Q,G)) by A3,A16,Th5;
    then
A18: B_INF(a,CompF(Q,G)).u = FALSE by A14,BVFUNC_1:def 16;
    u in EqClass(y,CompF(P,G)) by A1,A17,Th5;
    hence thesis by A18,BVFUNC_1:def 16;
  end;
  thus All(All(a,P,G),Q,G) = B_INF(All(a,P,G),CompF(Q,G)) by BVFUNC_2:def 9
    .= B_INF( B_INF(a,CompF(P,G)),CompF(Q,G)) by BVFUNC_2:def 9
    .= B_INF( B_INF(a,CompF(Q,G)),CompF(P,G)) by A5,BVFUNC_1:def 16
    .= B_INF(All(a,Q,G),CompF(P,G)) by BVFUNC_2:def 9
    .= All(All(a,Q,G),P,G) by BVFUNC_2:def 9;
end;

theorem
  G is independent implies Ex(Ex(a,P,G),Q,G) = Ex(Ex(a,Q,G),P,G)
proof
  assume
A1: G is independent;
  thus Ex(Ex(a,P,G),Q,G) = 'not' 'not' Ex(Ex(a,P,G),Q,G)
    .= 'not' All('not' Ex(a,P,G),Q,G) by BVFUNC_2:19
    .= 'not' All(All('not' a,P,G),Q,G) by BVFUNC_2:19
    .= 'not' All(All('not' a,Q,G),P,G) by A1,Th15
    .= 'not' All('not' Ex(a,Q,G),P,G) by BVFUNC_2:19
    .= 'not' 'not' Ex(Ex(a,Q,G),P,G) by BVFUNC_2:19
    .= Ex(Ex(a,Q,G),P,G);
end;

theorem
  for a being Function of Y,BOOLEAN, G being Subset of PARTITIONS(
Y), P,Q being a_partition of Y st G is independent holds Ex(All(a,P,G),Q,G) '<'
  All(Ex(a,Q,G),P,G)
proof
  let a be Function of Y,BOOLEAN, G be Subset of PARTITIONS(Y), P,Q be
  a_partition of Y such that
A1: G is independent;
  set A = G \ {P}, B = G \ {Q};
  A c= G & B c= G by XBOOLE_1:36;
  then
A2: ERl('/\'A)*ERl '/\'B = ERl ('/\'B)*ERl '/\'A by A1,Th14;
A3: CompF(P,G) = '/\' A by BVFUNC_2:def 7;
A4: Ex(All(a,P,G),Q,G) = B_SUP(All(a,P,G),CompF(Q,G)) by BVFUNC_2:def 10;
A5: CompF(Q,G) = '/\' B by BVFUNC_2:def 7;
  let x being Element of Y such that
A6: Ex(All(a,P,G),Q,G).x = TRUE;
A7: for z being Element of Y st z in EqClass(x,CompF(P,G)) holds Ex(a,Q,G).
  z=TRUE
  proof
    let z be Element of Y;
    consider y being Element of Y such that
A8: y in EqClass(x,CompF(Q,G)) and
A9: All(a,P,G).y=TRUE by A6,A4,BVFUNC_1:def 17;
    assume z in EqClass(x,CompF(P,G));
    then [z,x] in ERl '/\' A by A3,Th5;
    then
A10: [x,z] in ERl '/\' A by EQREL_1:6;
    [y,x] in ERl '/\' B by A5,A8,Th5;
    then [y,z] in (ERl '/\' A)*ERl '/\' B by A2,A10,RELAT_1:def 8;
    then consider u being set such that
A11: [y,u] in ERl '/\' A and
A12: [u,z] in ERl '/\' B by RELAT_1:def 8;
    u in field ERl '/\' B by A12,RELAT_1:15;
    then reconsider u as Element of Y by ORDERS_1:12;
    [u,y] in ERl '/\' A by A11,EQREL_1:6;
    then All(a,P,G) = B_INF(a,CompF(P,G)) & u in EqClass(y,CompF(P,G)) by A3
,Th5,BVFUNC_2:def 9;
    then
A13: a.u=TRUE by A9,BVFUNC_1:def 16;
    Ex(a,Q,G) = B_SUP(a,CompF(Q,G)) & u in EqClass(z,CompF(Q,G)) by A5,A12,Th5,
BVFUNC_2:def 10;
    hence thesis by A13,BVFUNC_1:def 17;
  end;
  All(Ex(a,Q,G),P,G) = B_INF(Ex(a,Q,G),CompF(P,G)) by BVFUNC_2:def 9;
  hence thesis by A7,BVFUNC_1:def 16;
end;

begin :: Moved from OPOSET_1, 2010.03.11, A.T.

reserve x,y,z for set,
  S, X for non empty set,
  R for Relation of X;

notation
  let A,B be set;
  synonym [#](A,B) for [:A,B:];
end;

definition
  let A,B be set;
  func {}(A,B) -> Relation of A,B equals
  {};
  correctness by RELSET_1:12;
  redefine func [#](A,B) -> Relation of A,B;
  correctness
  proof
    [#](A,B) c= [:A,B:];
    hence thesis;
  end;
end;

registration let A,B be set;
 cluster {}(A,B) -> empty;
 coherence;
end;

theorem
  field id X = X
proof
  dom id X = X & rng id X = X;
  then field id X = X \/ X by RELAT_1:def 6;
  hence thesis;
end;

theorem
  op1 = {[{},{}]}
proof
  {{}} = dom op1 by CARD_1:49,FUNCT_2:def 1;
  then {} in dom op1 by TARSKI:def 1;
  then [{},op1.{}] in op1 by FUNCT_1:def 2;
  then
A1: {[{},op1.{}]} c= op1 by ZFMISC_1:31;
  rng op1 = {op1.{}} by CARD_1:49,FUNCT_2:48;
  then
A2: op1.{} = {} by CARD_1:49,ZFMISC_1:18;
  op1 c= [:{{}},{{}}:] by CARD_1:49;
  then op1 c= {[{},{}]} by ZFMISC_1:29;
  hence thesis by A2,A1,XBOOLE_0:def 10;
end;

theorem
  for A,B being set holds field {}(A,B) = {} by RELAT_1:40;

theorem
  R is_reflexive_in X implies R is reflexive & field R = X
proof
  assume
A1: R is_reflexive_in X;
  then X = field R by Th9;
  hence thesis by A1,RELAT_2:def 9;
end;

theorem
  R is_symmetric_in X implies R is symmetric
proof
  assume
A1: R is_symmetric_in X;
  let x,y be set;
  field R c= X \/ X by RELSET_1:8;
  hence thesis by A1,RELAT_2:def 3;
end;

theorem
  R is symmetric implies R is_symmetric_in S
proof
  assume R is symmetric;
  then
A1: R is_symmetric_in field R by RELAT_2:def 11;
  let x,y be set;
  assume x in S & y in S;
  assume
A2: [x,y] in R;
  then x in field R & y in field R by RELAT_1:15;
  hence thesis by A1,A2,RELAT_2:def 3;
end;

theorem
  R is antisymmetric implies R is_antisymmetric_in S
proof
  assume R is antisymmetric; then
A1: R is_antisymmetric_in field R by RELAT_2:def 12;
  let x,y be set;
  assume x in S & y in S;
  assume
A2: [x,y] in R;
  then x in field R & y in field R by RELAT_1:15;
  hence thesis by A1,A2,RELAT_2:def 4;
end;

theorem
  R is_antisymmetric_in X implies R is antisymmetric
proof
  assume
A1: R is_antisymmetric_in X;
  let x,y be set;
  field R c= X \/ X by RELSET_1:8;
  hence thesis by A1,RELAT_2:def 4;
end;

theorem
  R is transitive implies R is_transitive_in S
proof
  assume R is transitive; then
A1: R is_transitive_in field R by RELAT_2:def 16;
  let x,y,z be set;
  assume x in S & y in S & z in S;
  assume
A2: [x,y] in R; then
A3: x in field R by RELAT_1:15;
  assume
A4: [y,z] in R;
  then y in field R & z in field R by RELAT_1:15;
  hence thesis by A1,A2,A4,A3,RELAT_2:def 8;
end;

theorem
  R is_transitive_in X implies R is transitive
proof
  assume
A1: R is_transitive_in X;
  let x,y,z be set;
  field R c= X \/ X by RELSET_1:8;
  hence thesis by A1,RELAT_2:def 8;
end;

theorem
  R is asymmetric implies R is_asymmetric_in S
proof
  assume R is asymmetric; then
A1: R is_asymmetric_in field R by RELAT_2:def 13;
  let x,y be set;
  assume x in S & y in S;
  assume
A2: [x,y] in R;
  then x in field R & y in field R by RELAT_1:15;
  hence thesis by A1,A2,RELAT_2:def 5;
end;

theorem
  R is_asymmetric_in X implies R is asymmetric
proof
  assume
A1: R is_asymmetric_in X;
  let x,y be set;
  field R c= X \/ X by RELSET_1:8;
  hence thesis by A1,RELAT_2:def 5;
end;

theorem
  R is irreflexive & field R c= S implies R is_irreflexive_in S
proof
  assume that
A1: R is irreflexive and
A2: field R c= S;
  let x be set;
  S = field R \/ ( S \ (field R) ) by A2,XBOOLE_1:45;
  then
A3: x in S implies x in field R or x in S \ (field R) by XBOOLE_0:def 3;
A4: x in S \ (field R) implies not [x,x] in R
  proof
    assume x in S \ (field R);
    then x in S \ (dom R \/ rng R) by RELAT_1:def 6;
    then x in (S \ dom R) /\ (S \ rng R) by XBOOLE_1:53;
    then x in (S \ rng R) by XBOOLE_0:def 4;
    then not x in rng R by XBOOLE_0:def 5;
    hence thesis by XTUPLE_0:def 13;
  end;
  R is_irreflexive_in field R by A1,RELAT_2:def 10;
  hence thesis by A3,A4,RELAT_2:def 2;
end;

theorem
  R is_irreflexive_in X implies R is irreflexive
proof
A1: field R c= X \/ X by RELSET_1:8;
  assume R is_irreflexive_in X;
  then for x being set holds x in field R implies not [x,x] in R by A1,
RELAT_2:def 2;
  then R is_irreflexive_in field R by RELAT_2:def 2;
  hence thesis by RELAT_2:def 10;
end;

:: Some existence conditions on non-empty relations

registration
  cluster empty -> irreflexive asymmetric transitive for Relation;
  coherence
  proof let R be Relation;
    assume
A1:  R is empty;
    hence for x holds x in field R implies not [x,x] in R;
    thus for x,y holds x in field R & y in field R & [x,y] in R implies
  not [y,x] in R by A1;
    thus for x,y,z holds x in field R & y in field R & z in field R &
     [x,y] in R & [y,z] in R implies [x,z] in R by A1;
  end;
end;

:: Double negation property of the internal Complement

definition
  let f be Function;
  attr f is involutive means
  :Def2:
  for x being set st x in dom f holds f.(f.x) = x;
end;

definition
  let X;
  let f be UnOp of X;
  redefine attr f is involutive means
  for x being Element of X holds f.(f.x) = x;
  compatibility
  proof
   dom f = X by PARTFUN1:def 2;
   hence f is involutive implies for x being Element of X holds f.(f.x) = x
   by Def2;
   assume
A1: for x being Element of X holds f.(f.x) = x;
   let x be set;
   assume x in dom f;
   hence thesis by A1;
  end;
end;

registration
  cluster op1 -> involutive for Function;
  coherence
 proof
 op1 is involutive proof let a be Element of 1;
  a = {} by CARD_1:49,TARSKI:def 1;
  hence op1.(op1.a) = a by CARD_1:49,FUNCT_2:50;
  end;
 hence thesis;
end;
end;

registration let X be set;
  cluster id X -> involutive;
  coherence
proof
  set f = id X;
  let a be set;
  assume a in dom f;
  then a in X;
  then f.a = a by FUNCT_1:17;
  hence thesis;
end;
end;