The intention of this page is presentation of thesis, which should be proven in all possible cases occurring during writing Mizar articles. Whenever it is possible, two examples are presented: the first - with a simple definiens, and the second - with a complex one.

In case of Statements possible skeletons of the formulas are presented.

In cases of quite complex thesis (e.g. conjunctions containing 4 conjuncts) thesis are divided into simpler sub-thesis.

Remark: involutiveness, projectivity and idempotence have been not implemented for redefined functors.

1. Introduction
2. Statements
3. Definitions
   1. Predicates
   2. Modes
   3. Functors (means, equals)
   4. Attributes
4. Redefinitions
   1. Result Type is being changed
      1. Modes
      2. Functors
   2. Definiens is being changed
      1. Predicates
      2. Modes
      3. Functors (means, equals)
      4. Attributes
5. Clusters
6. Properties
   1. Predicates
      1. reflexivity
      2. irreflexivity
      3. symmetry
      4. asymmetry
      5. connectedness
   2. Functors
      1. involutiveness (means, equals)
      2. projectivity (means, equals)
      3. commutativity (means, equals)
      4. idempotence (means, equals)
7. Properties in Redefinitions
   1. Predicates
      1. reflexivity
      2. irreflexivity
      3. symmetry
      4. asymmetry
      5. connectedness
   2. Functors
      1. commutativity
8. Definitional_Expansions
   1. Predicates
      1. non permissive
      2. permissive
   2. Modes
      1. non permissive
      2. permissive
   3. Attributes
      1. non permissive
      2. permissive

theorem
  phi[X]
  proof
    thus phi[X];
  end;

theorem
  phi[X] & psi[Y]
  proof
    thus phi[X];
    thus psi[Y];
  end;

theorem
  phi[X] implies psi[X]
  proof
    assume phi[X];
    thus psi[X];
  end;

theorem
  phi[X] iff psi[X]
  proof
    thus phi[X] implies psi[X];
    thus psi[X] implies phi[X];
  end;

theorem
  phi[X] iff psi[X]
  proof
    hereby 
      assume phi[X];
      thus psi[X];
    end;
    assume psi[X];
    thus phi[X];
  end;

theorem
  phi[X] or psi[X]
  proof
    assume not phi[X];
    thus psi[X];
  end;

theorem
  for X being set holds phi[X]
  proof
    let X be set;
    thus phi[X];
  end;

theorem
  ex X being set st phi[X]
  proof
    take X;
    thus phi[X];
  end;

definition
  let X, Y be set;
  pred X = Y means phi_1[X,Y];
end;

definition
  let X, Y be set;
  pred X = Y means
    phi_1[X,Y] if C1[X,Y],
    phi_2[X,Y] if C2[X,Y],
    phi_3[X,Y] if C3[X,Y]
    otherwise phi_4[X,Y];
  consistency
  proof
    thus C1[X,Y] & C2[X,Y] implies (phi_1[X,Y] iff phi_2[X,Y]);
    thus C1[X,Y] & C3[X,Y] implies (phi_1[X,Y] iff phi_3[X,Y]);
    thus C2[X,Y] & C3[X,Y] implies (phi_2[X,Y] iff phi_3[X,Y]);
  end;
end;

Modes

definition
  let X be set;
  mode Subset of X -> set means phi[it,X];
  existence
  proof
    thus ex A being set st phi[A,X];
  end;
end;

definition
  let X be set;
  mode Subset of X -> set means
    phi_1[X,it] if C1[X],
    phi_2[X,it] if C2[X],
    phi_3[X,it] if C3[X]
    otherwise phi_4[X,it];
  existence
  proof
    thus C1[X] implies ex A being set st phi_1[X,A];
    thus C2[X] implies ex A being set st phi_2[X,A];
    thus C3[X] implies ex A being set st phi_3[X,A];
    thus not C1[X] & not C2[X] & not C3[X] implies ex A being set st phi_4[X,A];
  end;
  consistency
  proof
    let IT be set;
    thus C1[X] & C2[X] implies (phi_1[X,IT] iff phi_2[X,IT]);
    thus C1[X] & C3[X] implies (phi_1[X,IT] iff phi_3[X,IT]);
    thus C2[X] & C3[X] implies (phi_2[X,IT] iff phi_3[X,IT]);
  end;
end;

Functors

definition
  let X, Y be set;
  func X \/ Y -> set means phi[it,X,Y];
  existence
  proof
    thus ex A being set st phi[A,X,Y];
  end;
  uniqueness
  proof
    thus for A, B being set st phi[A,X,Y] & phi[B,X,Y] holds A = B;
  end;
end;

definition
  let X, Y be set;
  func X \/ Y -> set means
    phi_1[it,X,Y] if C1[X,Y],
    phi_2[it,X,Y] if C2[X,Y],
    phi_3[it,X,Y] if C3[X,Y]
    otherwise phi_4[it,X,Y];
  existence
  proof
    thus C1[X,Y] implies ex A being set st phi_1[A,X,Y];
    thus C2[X,Y] implies ex A being set st phi_2[A,X,Y];
    thus C3[X,Y] implies ex A being set st phi_3[A,X,Y];
    thus not C1[X,Y] & not C2[X,Y] & not C3[X,Y] implies 
         ex A being set st phi_4[A,X,Y]];
  end;
  uniqueness
  proof
    let A, B be set;
    thus C1[X,Y] & phi_1[A,X,Y] & phi_1[B,X,Y] implies A = B;
    thus C2[X,Y] & phi_2[A,X,Y] & phi_2[B,X,Y] implies A = B;
    thus C3[X,Y] & phi_3[A,X,Y] & phi_3[B,X,Y] implies A = B;
    thus not C1[X,Y] & not C2[X,Y] & not C3[X,Y] & 
         phi_4[A,X,Y] & phi_4[B,X,Y] implies A = B;
  end;
  consistency
  proof
    let IT be set;
    thus C1[X,Y] & C2[X,Y] implies (phi_1[IT,X,Y] iff phi_2[IT,X,Y]);
    thus C1[X,Y] & C3[X,Y] implies (phi_1[IT,X,Y] iff phi_3[IT,X,Y]);
    thus C2[X,Y] & C3[X,Y] implies (phi_2[IT,X,Y] iff phi_3[IT,X,Y]);
  end;
end;

definition
  let X, Y be set;
  func X \/ Y -> set equals tau(X,Y);
  coherence
  proof
    thus tau(X,Y) is set;
  end;
end;

definition
  let X, Y be set;
  func X \/ Y -> set equals
    tau_1(X,Y) if C1[X,Y],
    tau_2(X,Y) if C2[X,Y],
    tau_3(X,Y) if C3[X,Y]
    otherwise tau_4(X,Y);
  coherence
  proof
    thus C1[X,Y] implies tau_1(X,Y) is set;
    thus C2[X,Y] implies tau_2(X,Y) is set;
    thus C3[X,Y] implies tau_3(X,Y) is set;
    thus not C1[X,Y] & not C2[X,Y] & not C3[X,Y] implies tau_4(X,Y) is set;
  end;
  consistency
  proof
    let IT be set;
    thus phi_1[X,Y] & phi_2[X,Y] implies (IT = tau_1(X,Y) iff IT = tau_2(X,Y));
    thus phi_1[X,Y] & phi_3[X,Y] implies (IT = tau_1(X,Y) iff IT = tau_3(X,Y));
    thus phi_2[X,Y] & phi_3[X,Y] implies (IT = tau_2(X,Y) iff IT = tau_3(X,Y));
  end;
end;

Attributes

definition
  let X be set;
  attr X is empty means phi[X];
end;

definition
  let X be set;
  attr X is empty means
    phi_1[X] if C1[X],
    phi_2[X] if C2[X],
    phi_3[X] if C3[X]
    otherwise phi_4[X];
  consistency
  proof
    thus C1[X] & C2[X] implies (phi_1[X] iff phi_2[X]);
    thus C1[X] & C3[X] implies (phi_1[X] iff phi_3[X]);
    thus C2[X] & C3[X] implies (phi_2[X] iff phi_3[X]);
  end;
end;

definition
  let X, Y be set;
  redefine pred X c= Y means phi_1[X,Y];
  compatibility
  proof
    thus X c= Y iff phi_1[X,Y];
  end;
end;

definition
  let X, Y be set;
  redefine pred X c= Y means
    phi_1[X,Y] if C1[X,Y],
    phi_2[X,Y] if C2[X,Y],
    phi_3[X,Y] if C3[X,Y]
    otherwise phi_4[X,Y];
  consistency;
  compatibility
  proof
    thus C1[X,Y] implies (X c= Y iff phi_1[X,Y]);
    thus C2[X,Y] implies (X c= Y iff phi_2[X,Y]);
    thus C3[X,Y] implies (X c= Y iff phi_3[X,Y]);
    thus not C1[X,Y] & not C2[X,Y] & not C3[X,Y] implies
         (X c= Y iff phi_4[X,Y]);
  end;
end;

Modes

definition
  let X be set;
  redefine mode Subset of X -> new_type;
  coherence
  proof
    thus for A being Subset of X holds A is new_type;
  end;
end;

definition
  let X be set;
  redefine mode Subset of X means phi_1[it,X];
  compatibility
  proof
    let A be set;
    thus A is Subset of X iff phi_1[A,X];
  end;
end;

definition
  let X be set;
  redefine mode Subset of X means
    phi_1[it,X] if G1[X],
    phi_2[it,X] if G2[X],
    phi_3[it,X] if G3[X]
    otherwise phi_4[it,X];
  compatibility
  proof
    let A be set;
    thus G1[X] implies (A is Subset of X iff phi_1[A,X]);
    thus G2[X] implies (A is Subset of X iff phi_2[A,X]);
    thus G3[X] implies (A is Subset of X iff phi_3[A,X]);
    thus not G1[X] & not G2[X] & not G3[X] implies
         (A is Subset of X iff phi_4[A,X]);
  end;
  consistency;
end;

Functors

definition
  let X be set;
  redefine func +X -> new_type;
  coherence
  proof
    thus +X is new_type;
  end;
end;

definition
  let X be set;
  redefine func +X means phi_1[it,X];
  compatibility
  proof
    let A be set;
    thus A = +X iff phi_1[A,X];
  end;  
end;

definition
  let X be set;
  redefine func +X means
    phi_1[it,X] if G1[X],
    phi_2[it,X] if G2[X],
    phi_3[it,X] if G3[X]
    otherwise phi_4[it,X];
  consistency;
  compatibility
  proof
    let A be set;
    thus G1[X] implies (A = +X iff phi_1[A,X]);
    thus G2[X] implies (A = +X iff phi_2[A,X]);
    thus G3[X] implies (A = +X iff phi_3[A,X]);
    thus not G1[X] & not G2[X] & not G3[X] implies (A = +X iff phi_4[A,X]);
  end;
end;

definition
  let X be set;
  redefine func +X equals tau_1(X);
  compatibility
  proof
    let A be set;
    thus A = +X iff A = tau_1(X);
  end;  
end;

definition
  let X be set;
  redefine func +X equals
    tau_1(X) if G1[X],
    tau_2(X) if G2[X],
    tau_3(X) if G3[X]
    otherwise tau_4(X);
  consistency;
  compatibility
  proof
    let A be set;
    thus G1[X] implies (A = +X iff A = tau_1(A));
    thus G2[X] implies (A = +X iff A = tau_2(A));
    thus G3[X] implies (A = +X iff A = tau_3(A));
    thus not G1[X] & not G2[X] & not G3[X] implies (A = +X iff A = tau_4(A));
  end;
end;

Attributes

definition
  let X be set;
  redefine attr X is empty means phi_1[X];
  compatibility
  proof
    thus X is empty iff phi_1[X];
  end;
end;

definition
  let X be set;
  redefine attr X is empty means
    phi_1[X] if C1[X],
    phi_2[X] if C2[X],
    phi_3[X] if C3[X]
    otherwise phi_4[X];
  compatibility
  proof
    thus C1[X] implies (X is empty iff phi_1[X]);
    thus C2[X] implies (X is empty iff phi_2[X]);
    thus C3[X] implies (X is empty iff phi_3[X]);
    thus not C1[X] & not C2[X] & not C3[X] implies (X is empty iff phi_4[X]);
  end;
  consistency;
end;

definition
  let X be non empty set;
  cluster non empty finite Subset of X;
  existence
  proof
    thus ex A being Subset of X st A is non empty finite;
  end;
end;

Conditional Clusters

definition
  cluster trivial -> finite set;
  coherence
  proof
    thus for A being set st A is trivial holds A is finite;
  end;
end;

definition
  let X be finite set;
  cluster -> finite Subset of X;
  coherence
  proof
    thus for A being Subset of X holds A is finite;
  end;
end;

Functorial Clusters

definition
  let X be set; let Y be non empty set;
  cluster X \/ Y -> non empty;
  coherence
  proof
    thus X \/ Y is non empty;
  end;
end;

definition
  let X, Y be set;
  pred X = Y means psi_1[X,Y];
  reflexivity
  proof
    thus for A being set holds psi_1[A,A];
  end;
end;

definition
  let X, Y be set;
  pred X = Y means
    phi_1[X,Y] if C1[X,Y],
    phi_2[X,Y] if C2[X,Y],
    phi_3[X,Y] if C3[X,Y]
    otherwise phi_4[X,Y];
  consistency;
  reflexivity
  proof
    let A be set;
    thus C1[A,A] implies phi_1[A,A];
    thus C2[A,A] implies phi_2[A,A];
    thus C3[A,A] implies phi_3[A,A];
    thus not C1[A,A] & not C2[A,A] & not C3[A,A] implies phi_4[A,A];
  end;
end;

definition
  let X, Y be set;
  pred X = Y means psi_1[X,Y];
  irreflexivity
  proof
    thus for A being set holds not psi_1[A,A];
  end;
end;

definition
  let X, Y be set;
  pred X = Y means
    phi_1[X,Y] if C1[X,Y],
    phi_2[X,Y] if C2[X,Y],
    phi_3[X,Y] if C3[X,Y]
    otherwise phi_4[X,Y];
  consistency;
  irreflexivity
  proof
    let A be set;
    thus not
    (
       (C1[A,A] implies phi_1[A,A]) &
       (C2[A,A] implies phi_2[A,A]) &
       (C3[A,A] implies phi_3[A,A]) &
       (not C1[A,A] & not C2[A,A] & not C3[A,A] implies phi_4[A,A])
    );
  end;
end;

definition
  let X, Y be set;
  pred X = Y means psi_1[X,Y];
  symmetry
  proof
    thus for A, B being set holds psi_1[A,B] implies psi_1[B,A];
  end;
end;

definition
  let X, Y be set;
  pred X = Y means
    phi_1[X,Y] if C1[X,Y],
    phi_2[X,Y] if C2[X,Y],
    phi_3[X,Y] if C3[X,Y]
    otherwise phi_4[X,Y];
  consistency;
  symmetry
  proof
    let A, B be set;
    thus 
      (C1[A,B] implies phi_1[A,B]) &
      (C2[A,B] implies phi_2[A,B]) &
      (C3[A,B] implies phi_3[A,B]) &
      (not C1[A,B] & not C2[A,B]& not C3[A,B] implies phi_4[A,B])
    implies 
      (C1[B,A] implies phi_1[B,A]) &
      (C2[B,A] implies phi_2[B,A]) &
      (C3[B,A] implies phi_3[B,A]) &
      (not C1[B,A] & not C2[B,A] & not C3[B,A] implies phi_4[B,A]);
  end;
end;

definition
  let X, Y be set;
  pred X = Y means psi_1[X,Y];
  asymmetry
  proof
    thus for A, B being set holds psi_1[A,B] implies not psi_1[B,A];
  end;
end;

definition
  let X, Y be set;
  pred X = Y means
    phi_1[X,Y] if C1[X,Y],
    phi_2[X,Y] if C2[X,Y],
    phi_3[X,Y] if C3[X,Y]
    otherwise phi_4[X,Y];
  consistency;
  asymmetry
  proof
    let A, B be set;
    thus 
      (C1[A,B] implies phi_1[A,B]) &
      (C2[A,B] implies phi_2[A,B]) &
      (C3[A,B] implies phi_3[A,B]) &
      (not C1[A,B] & not C2[A,B]& not C3[A,B] implies phi_4[A,B])
    implies
     not (
         (C1[B,A] implies phi_1[B,A]) &
         (C2[B,A] implies phi_2[B,A]) &
         (C3[B,A] implies phi_3[B,A]) &
         (not C1[B,A] & not C2[B,A] & not C3[B,A] implies phi_4[B,A])
     );
  end;
end;

definition
  let X, Y be set;
  pred X = Y means psi_1[X,Y];
  connectedness
  proof
    thus for A, B being set holds psi_1[A,B] or psi_1[B,A];
  end;
end;

definition
  let X, Y be set;
  pred X c= Y means
    phi_1[X,Y] if C1[X,Y],
    phi_2[X,Y] if C2[X,Y],
    phi_3[X,Y] if C3[X,Y]
    otherwise phi_4[X,Y];
  consistency;
  connectedness
  proof
    let A, B be set;
    thus 
      not (
          (C1[A,B] implies phi_1[A,B]) &
          (C2[A,B] implies phi_2[A,B]) &
          (C3[A,B] implies phi_3[A,B]) &
          (not C1[A,B] & not C2[A,B]& not C3[A,B] implies phi_4[A,B])
      )
    implies
         (C1[B,A] implies phi_1[B,A]) &
         (C2[B,A] implies phi_2[B,A]) &
         (C3[B,A] implies phi_3[B,A]) &
         (not C1[B,A] & not C2[B,A] & not C3[B,A] implies phi_4[B,A]);
  end;
end;

Properties - Functors

definition
  let X be set;
  func +X -> set means psi_1[it,X];
  existence;
  uniqueness;
  involutiveness
  proof
    thus for r, A being set st psi_1[r,A] holds psi_1[A,r];
  end;
end;

definition
  let X be set;
  func +X -> set means
    phi_1[it,X] if G1[X],
    phi_2[it,X] if G2[X],
    phi_3[it,X] if G3[X]
    otherwise phi_4[it,X];
  existence;
  uniqueness;
  consistency;
  involutiveness
  proof
    let IT, x be set;
    thus
      (G1[x] implies phi_1[IT,x]) &
      (G2[x] implies phi_2[IT,x]) &
      (G3[x] implies phi_3[IT,x]) &
      (not G1[x] & not G2[x] & not G3[x] implies phi_4[IT,x])
    implies
      (G1[IT] implies phi_1[x,IT]) &
      (G2[IT] implies phi_2[x,IT]) &
      (G3[IT] implies phi_3[x,IT]) &
      (not G1[IT] & not G2[IT] & not G3[IT] implies phi_4[x,IT]);
  end;
end;

definition
  let X be set;
  func +X -> set equals tau_1(X);
  coherence;
  involutiveness
  proof
    thus for r, A being set st r = tau_1(A) holds A = tau_1(r);
  end;
end;

definition
  let X be set;
  func +X -> set equals
    tau_1(X) if G1[X],
    tau_2(X) if G2[X],
    tau_3(X) if G3[X]
    otherwise tau_4(X);
  coherence;
  consistency;
  involutiveness
  proof
    let IT, x be set;
    thus 
      (G1[x] implies IT = tau_1(x)) &
      (G2[x] implies IT = tau_2(x)) &
      (G3[x] implies IT = tau_3(x)) &
      (not G1[x] & not G2[x] & not G3[x] implies IT = tau_4(x))
    implies
      (G1[IT] implies x = tau_1(IT)) &
      (G2[IT] implies x = tau_2(IT)) &
      (G3[IT] implies x = tau_3(IT)) &
      (not G1[IT] & not G2[IT] & not G3[IT] implies x = tau_4(IT));
  end;
end;

definition
  let X be set;
  func +X -> set means psi_1[it,X];
  existence;
  uniqueness;
  projectivity
  proof
    thus for r, A being set st psi_1[r,A] holds psi_1[r,r];
  end;
end;

definition
  let X be set;
  func +X -> set means
    phi_1[it,X] if G1[X],
    phi_2[it,X] if G2[X],
    phi_3[it,X] if G3[X]
    otherwise phi_4[it,X];
  existence;
  uniqueness;
  consistency;
  projectivity
  proof
    let IT, x be set;
    thus
      (G1[x] implies phi_1[IT,x]) &
      (G2[x] implies phi_2[IT,x]) &
      (G3[x] implies phi_3[IT,x]) &
      (not G1[x] & not G2[x] & not G3[x] implies phi_4[IT,x])
    implies
      (G1[IT] implies phi_1[IT,IT]) &
      (G2[IT] implies phi_2[IT,IT]) &
      (G3[IT] implies phi_3[IT,IT]) &
      (not G1[IT] & not G2[IT] & not G3[IT] implies phi_4[IT,IT]);
  end;
end;

definition
  let X be set;
  func +X -> set equals tau_1(X);
  coherence;
  projectivity
  proof
    thus for r, A being set st r = tau_1(A) holds r = tau_1(r);
  end;
end;

definition
  let X be set;
  func +X -> set equals
    tau_1(X) if G1[X],
    tau_2(X) if G2[X],
    tau_3(X) if G3[X]
    otherwise tau_4(X);
  coherence;
  consistency;
  projectivity
  proof
    let IT, x be set;
    thus 
      (G1[x] implies IT = tau_1(x)) &
      (G2[x] implies IT = tau_2(x)) &
      (G3[x] implies IT = tau_3(x)) &
      (not G1[x] & not G2[x] & not G3[x] implies IT = tau_4(x))
    implies
      (G1[IT] implies IT = tau_1(IT)) &
      (G2[IT] implies IT = tau_2(IT)) &
      (G3[IT] implies IT = tau_3(IT)) &
      (not G1[IT] & not G2[IT] & not G3[IT] implies IT = tau_4(IT));
  end;
end;

definition
  let X, Y be set;
  func X + Y -> set means psi_1[it,X,Y];
  existence;
  uniqueness;
  commutativity
  proof
    thus for r, A, B being set holds psi_1[r,A,B] implies psi_1[r,B,A];
  end;
end;

definition
  let X, Y be set;
  func X + Y -> set means
    psi_1[it,X,Y] if C1[X,Y],
    psi_2[it,X,Y] if C2[X,Y],
    psi_3[it,X,Y] if C3[X,Y]
    otherwise psi_4[it,X,Y];
  existence;
  uniqueness;
  consistency;
  commutativity
  proof
    let IT, x, y be set;
    thus
      (C1[x,y] implies psi_1[IT,x,y]) &
      (C2[x,y] implies psi_2[IT,x,y]) &
      (C3[x,y] implies psi_3[IT,x,y]) &
      (not C1[x,y] & not C2[x,y] & not C3[x,y] implies psi_4[IT,x,y])
    implies
      (C1[y,x] implies psi_1[IT,y,x]) &
      (C2[y,x] implies psi_2[IT,y,x]) &
      (C3[y,x] implies psi_3[IT,y,x]) &
      (not C1[y,x] & not C2[y,x] & not C3[y,x] implies psi_4[IT,y,x]);
  end;
end;

definition
  let X, Y be set;
  func X + Y -> set equals tau_1(X,Y);
  coherence;
  commutativity
  proof
    thus for r, A, B being set st r = tau_1(A,B) holds r = tau_1(B,A);
  end;
end;

definition
  let X, Y be set;
  func X + Y -> set equals
    tau_1(X,Y) if C1[X,Y],
    tau_2(X,Y) if C2[X,Y],
    tau_3(X,Y) if C3[X,Y]
    otherwise tau_4(X,Y);
  coherence;
  consistency;
  commutativity
  proof
    let IT, x, y be set;
    thus
      (C1[x,y] implies IT = tau_1(x,y)) &
      (C2[x,y] implies IT = tau_2(x,y)) &
      (C3[x,y] implies IT = tau_3(x,y)) &
      (not C1[x,y] & not C2[x,y] & not C3[x,y] implies IT = tau_4(x,y))
    implies
      (C1[y,x] implies IT = tau_1(y,x)) &
      (C2[y,x] implies IT = tau_2(y,x)) &
      (C3[y,x] implies IT = tau_3(y,x)) &
      (not C1[y,x] & not C2[y,x] & not C3[y,x] implies IT = tau_4(y,x));
  end;
end;

definition
  let X, Y be set;
  func X + Y -> set means psi_1[it,X,Y];
  existence;
  uniqueness;
  idempotence
  proof
    thus for A being set holds psi_1[A,A,A];
  end;
end;

definition
  let X, Y be set;
  func X + Y -> set means
    psi_1[it,X,Y] if C1[X,Y],
    psi_2[it,X,Y] if C2[X,Y],
    psi_3[it,X,Y] if C3[X,Y]
    otherwise psi_4[it,X,Y];
  existence;
  uniqueness;
  consistency;
  idempotence
  proof
    let IT be set;
    thus C1[IT,IT] implies psi_1[IT,IT,IT];
    thus C2[IT,IT] implies psi_2[IT,IT,IT];
    thus C3[IT,IT] implies psi_3[IT,IT,IT];
    thus not C1[IT,IT] & not C2[IT,IT] & not C3[IT,IT]
         implies psi_4[IT,IT,IT];
  end;
end;

definition
  let X, Y be set;
  func X + Y -> set equals F(X,Y);
  coherence;
  idempotence
  proof
    thus for A being set holds A = F(A,A);
  end;
end;

definition
  let X, Y be set;
  func X + Y -> set equals
    tau_1(X,Y) if C1[X,Y],
    tau_2(X,Y) if C2[X,Y],
    tau_3(X,Y) if C3[X,Y]
    otherwise tau_4(X,Y);
  coherence;
  consistency;
  idempotence
  proof
    let IT be set;
    thus C1[IT,IT] implies IT = tau_1(IT,IT);
    thus C2[IT,IT] implies IT = tau_2(IT,IT);
    thus C3[IT,IT] implies IT = tau_3(IT,IT);
    thus not C1[IT,IT] & not C2[IT,IT] & not C3[IT,IT]
         implies IT = tau_4(IT,IT);
  end;
end;

definition
  let X, Y be set;
  redefine pred X c= Y;
  reflexivity
  proof
    thus for x being set holds x c= x;
  end;
end;

definition
  let X, Y be set;
  redefine pred X c= Y;
  irreflexivity
  proof
    thus for x being set holds not x c= x;
  end;
end;

definition
  let X, Y be set;
  redefine pred X c= Y;
  symmetry
  proof
    thus for x, y being set st x c= y holds y c= x;
  end;
end;

definition
  let X, Y be set;
  redefine pred X c= Y;
  asymmetry
  proof
    thus for x, y being set st x c= y holds not y c= x;
  end;
end;

definition
  let X, Y be set;
  redefine pred X c= Y;
  connectedness
  proof
    thus for x, y being set holds x c= y or y c= x;
  end;
end;

Properties - Functors

definition
  let X, Y be set;
  redefine func X + Y;
  commutativity
  proof
    thus for x, y being set holds x + y = y + x;
  end;
end;

definition
  let X, Y be set;
  pred X c= Y means phi_1[X,Y];
end;

X c= Y
proof
  thus phi_1[X,Y];
end;

definition
  let X, Y be set;
  pred X c= Y means
    phi_1[X,Y] if C1[X,Y],
    phi_2[X,Y] if C2[X,Y],
    phi_3[X,Y] if C3[X,Y]
    otherwise phi_4[X,Y];
  consistency;
  connectedness;
end;

X c= Y
proof
  per cases;
  case C1[X,Y];
  thus phi_1[X,Y];
  case C2[X,Y];
  thus phi_2[X,Y];
  case C3[X,Y];
  thus phi_3[X,Y];
  case not C1[X,Y] & not C2[X,Y] & not C3[X,Y];
  thus phi_4[X,Y];
end;

definition
  let X, Y be set;
  assume alpha[X,Y];
  pred X c= Y means phi_1[X,Y];
end;

X c= Y
proof
  thus alpha[X,Y];
  thus phi_1[X,Y];
end;

definition
  let X, Y be set;
  assume alpha[X,Y];
  pred X c= Y means
    phi_1[X,Y] if C1[X,Y],
    phi_2[X,Y] if C2[X,Y],
    phi_3[X,Y] if C3[X,Y]
    otherwise phi_4[X,Y];
  consistency;
end;

X c= Y
proof
  thus alpha[X,Y];
  per cases;
  case C1[X,Y];
  thus phi_1[X,Y];
  case C2[X,Y];
  thus phi_2[X,Y];
  case C3[X,Y];
  thus phi_3[X,Y];
  case not C1[X,Y] & not C2[X,Y] & not C3[X,Y];
  thus phi_4[X,Y];
end;

Definitional Expansions - Modes

definition
  let X be set;
  mode Subset of X -> set means phi_1[it,X];
  existence;
end;

Y is Subset of X
proof
  thus phi_1[Y,X];
end;

definition
  let X be set;
  mode Subset of X -> set means
    phi_1[it,X] if G1[X],
    phi_2[it,X] if G2[X],
    phi_3[it,X] if G3[X]
    otherwise phi_4[it,X];
  existence;
  consistency;
end;

Y is Subset of X
proof
  per cases;
  case G1[X];
  thus phi_1[Y,X];
  case G2[X];
  thus phi_2[Y,X];
  case G3[X];
  thus phi_3[Y,X];
  case not G1[X] & not G2[X] & not G3[X];
  thus phi_4[Y,X];
end;

definition
  let X be set;
  assume beta[X];
  mode Subset of X -> set means phi_1[it,X];
  existence;
end;

Y is Subset of X
proof
  thus beta[X];
  thus phi_1[Y,X];
end;

definition
  let X be set;
  assume beta[X];
  mode Subset of X -> set means
    phi_1[it,X] if G1[X],
    phi_2[it,X] if G2[X],
    phi_3[it,X] if G3[X]
    otherwise phi_4[it,X];
  existence;
  consistency;
end;

Y is Subset of X
proof
  thus beta[X];
  per cases;
  case G1[X];
  thus phi_1[Y,X];
  case G2[X];
  thus phi_2[Y,X];
  case G3[X];
  thus phi_3[Y,X];
  case not G1[X] & not G2[X] & not G3[X];
  thus phi_4[Y,X];
end;

Definitional Expansions - Attributes

definition
  let X be set;
  attr X is empty means phi_1[X];
end;

X is empty
proof
  thus phi_1[X];
end;

definition
  let X be set;
  attr X is empty means
    phi_1[X] if C1[X],
    phi_2[X] if C2[X],
    phi_3[X] if C3[X]
    otherwise phi_4[X];
  consistency;
end;

X is empty
proof
  per cases;
  case C1[X];
  thus phi_1[X];
  case C2[X];
  thus phi_2[X];
  case C3[X];
  thus phi_3[X];
  case not C1[X] & not C2[X] & not C3[X];
  thus phi_4[X];
end;

definition
  let X be set;
  assume beta[X];
  attr X is empty means phi_1[X];
end;

X is empty
proof
  thus beta[X];
  thus phi_1[X];
end;

definition
  let X be set;
  assume beta[X];
  attr X is empty means
    phi_1[X] if C1[X],
    phi_2[X] if C2[X],
    phi_3[X] if C3[X]
    otherwise phi_4[X];
  consistency;
end;

X is empty
proof
  thus beta[X];
  per cases;
  case C1[X];
  thus phi_1[X];
  case C2[X];
  thus phi_2[X];
  case C3[X];
  thus phi_3[X];
  case not C1[X] & not C2[X] & not C3[X];
  thus phi_4[X];
end;