### Definitions

#### Predicates

```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 - means

```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;
```

#### Functors - equals

```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;
```