Changes by: Yegor N. Bryukhov (ybryukhov at gc.cuny.edu)
Date: 2003-12-15 21:55:45 -0800 (Mon, 15 Dec 2003)
Revision: 5178
Log message:
1.itt_ring - proved all theorems.
2.itt_record - added a theorem on how recordOrt interplays with set.
3.itt_field - original form of isField was incorrect, finally I added
[i:l] to it because I say that car0 is equal to certain set.
Still proof of isField_wf is incomplete yet and huge (it possibly
means that itt_group*, itt_record* and itt_ring have imperfect design).