let T be 1 -element TopStruct ; :: thesis: T is homogeneous
let p, q be Point of T; :: according to TOPGRP_1:def 6 :: thesis: ex f being Homeomorphism of T st f . p = q
take id T ; :: thesis: (id T) . p = q
thus (id T) . p = q by STRUCT_0:def 10; :: thesis: verum