begin
theorem
theorem
theorem
theorem Th4:
theorem
theorem Th6:
begin
:: deftheorem defines Proj WAYBEL24:def 1 :
theorem Th7:
:: deftheorem defines Proj WAYBEL24:def 2 :
theorem Th8:
theorem Th9:
theorem Th10:
theorem Th11:
theorem Th12:
theorem
theorem Th14:
theorem Th15:
theorem
theorem Th17:
theorem
theorem Th19:
begin
:: deftheorem Def3 defines ContMaps WAYBEL24:def 3 :
theorem Th20:
theorem Th21:
theorem
theorem Th23:
theorem
theorem Th25:
theorem Th26:
theorem Th27:
theorem Th28:
Lm1:
for S being non empty RelStr
for D being non empty Subset of holds D = { i where i is Element of : i in D }
theorem Th29:
theorem Th30:
theorem Th31:
theorem Th32:
theorem Th33:
theorem
theorem Th35:
theorem
theorem
theorem