begin
theorem
theorem
theorem
theorem
begin
theorem Th5:
theorem
theorem Th7:
theorem
begin
:: deftheorem Def1 defines <= YELLOW_2:def 1 :
theorem
canceled;
theorem
begin
:: deftheorem defines Image YELLOW_2:def 2 :
theorem
canceled;
theorem
begin
theorem
theorem
theorem
theorem
theorem
theorem Th18:
theorem
begin
theorem
theorem Th21:
theorem Th22:
theorem
begin
theorem Th24:
theorem Th25:
theorem Th26:
theorem Th27:
theorem Th28:
theorem
theorem Th30:
theorem Th31:
theorem Th32:
theorem Th33:
theorem Th34:
theorem Th35:
theorem
theorem
begin
theorem Th38:
theorem
theorem Th40:
theorem
theorem Th42:
theorem Th43:
theorem Th44:
theorem
theorem Th46:
theorem Th47:
theorem Th48:
theorem Th49:
theorem Th50:
begin
:: deftheorem Def3 defines SupMap YELLOW_2:def 3 :
theorem Th51:
theorem
theorem Th53:
:: deftheorem Def4 defines IdsMap YELLOW_2:def 4 :
theorem Th54:
begin
:: deftheorem defines \\/ YELLOW_2:def 5 :
:: deftheorem defines //\ YELLOW_2:def 6 :
theorem
theorem
theorem