begin
theorem
theorem Th2:
theorem
begin
theorem Th4:
theorem Th5:
theorem
theorem Th7:
theorem
Lm1:
for G being Group
for A, B being Subset of st A c= B holds
A " c= B "
theorem Th9:
theorem Th10:
theorem Th11:
theorem Th12:
theorem Th13:
theorem Th14:
theorem Th15:
:: deftheorem Def1 defines * TOPGRP_1:def 1 :
:: deftheorem Def2 defines * TOPGRP_1:def 2 :
theorem Th16:
theorem Th17:
theorem Th18:
theorem Th19:
begin
theorem Th20:
theorem Th21:
theorem
theorem
theorem
theorem Th25:
theorem
theorem
theorem Th28:
theorem Th29:
begin
:: deftheorem Def3 defines Homeomorphism TOPGRP_1:def 3 :
:: deftheorem Def4 defines Homeomorphism TOPGRP_1:def 4 :
theorem Th30:
Lm2:
for T being TopStruct
for f being Function of T,T st T is empty holds
f is being_homeomorphism
theorem Th31:
:: deftheorem Def5 defines HomeoGroup TOPGRP_1:def 5 :
theorem
theorem Th33:
theorem
:: deftheorem Def6 defines homogeneous TOPGRP_1:def 6 :
theorem
theorem Th36:
begin
:: deftheorem Def7 defines UnContinuous TOPGRP_1:def 7 :
:: deftheorem Def8 defines BinContinuous TOPGRP_1:def 8 :
theorem Th37:
theorem Th38:
theorem Th39:
theorem Th40:
theorem Th41:
theorem
theorem Th43:
theorem Th44:
theorem Th45:
theorem Th46:
theorem Th47:
theorem Th48:
theorem Th49:
theorem Th50:
theorem Th51:
theorem Th52:
theorem Th53:
theorem Th54:
theorem Th55:
theorem Th56:
theorem Th57:
theorem Th58:
theorem
theorem Th60:
theorem