### Statements

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;