let T be non empty TopStruct ; :: thesis: ( T is trivial implies T is homogeneous )
assume A1: T is trivial ; :: 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 A1, STRUCT_0:def 10; :: thesis: verum