:: Preliminaries to Structures
:: by Library Committee
::
:: Received January 6, 1995
:: Copyright (c) 1995 Association of Mizar Users
:: deftheorem Def1 defines empty STRUCT_0:def 1 :
:: deftheorem defines {} STRUCT_0:def 2 :
:: deftheorem defines [#] STRUCT_0:def 3 :
:: deftheorem defines id STRUCT_0:def 4 :
:: deftheorem defines in STRUCT_0:def 5 :
:: deftheorem defines 0. STRUCT_0:def 6 :
:: deftheorem defines 1. STRUCT_0:def 7 :
:: deftheorem Def8 defines degenerated STRUCT_0:def 8 :
:: deftheorem Def9 defines trivial STRUCT_0:def 9 :
:: deftheorem Def10 defines trivial STRUCT_0:def 10 :
:: deftheorem Def11 defines finite STRUCT_0:def 11 :
:: deftheorem Def12 defines zero STRUCT_0:def 12 :
:: deftheorem Def13 defines void STRUCT_0:def 13 :
:: deftheorem defines --> STRUCT_0:def 14 :
:: deftheorem defines zero STRUCT_0:def 15 :
:: deftheorem defines non-zero STRUCT_0:def 16 :
:: deftheorem defines card STRUCT_0:def 17 :