consider R being BinOp of {{} };
1TopSp {{} } = TopStruct(# {{} },(bool {{} }) #) ;
then reconsider T = TopGrStr(# {{} },R,(bool {{} }) #) as non empty TopSpace-like Group-like associative strict TopGrStr by TEX_2:12;
take T ; :: thesis: ( T is strict & T is commutative & T is trivial & T is UnContinuous & T is BinContinuous )
thus ( T is strict & T is commutative & T is trivial ) ; :: thesis: ( T is UnContinuous & T is BinContinuous )

hereby :: according to TOPGRP_1:def 7 :: thesis: T is BinContinuous

set f = inverse_op T;
thus inverse_op T is continuous :: thesis: verum

proof

let P1 be Subset of T; :: according to PRE_TOPC:def 12 :: thesis: ( not P1 is closed or (inverse_op T) " P1 is closed )
assume P1 is closed ; :: thesis: (inverse_op T) " P1 is closed

per cases ( (inverse_op T) " P1 = {} or (inverse_op T) " P1 = {{} } ) by ZFMISC_1:39;

suppose (inverse_op T) " P1 = {} ; :: thesis: (inverse_op T) " P1 is closed

hence (inverse_op T) " P1 is closed ; :: thesis: verum

end;

suppose (inverse_op T) " P1 = {{} } ; :: thesis: (inverse_op T) " P1 is closed

then (inverse_op T) " P1 = [#] T ;
hence (inverse_op T) " P1 is closed ; :: thesis: verum

end;

end;

end;

end;

let f be Function of [:T,T:],T; :: according to TOPGRP_1:def 8 :: thesis: ( f = the multF of T implies f is continuous )
assume f = the multF of T ; :: thesis: f is continuous
A1: the carrier of [:T,T:] = [:{{} },{{} }:] by BORSUK_1:def 5
.= {[{} ,{} ]} by ZFMISC_1:35 ;
let P1 be Subset of T; :: according to PRE_TOPC:def 12 :: thesis: ( not P1 is closed or f " P1 is closed )
assume P1 is closed ; :: thesis: f " P1 is closed

per cases ( f " P1 = {} or f " P1 = {[{} ,{} ]} ) by A1, ZFMISC_1:39;

suppose f " P1 = {} ; :: thesis: f " P1 is closed

hence f " P1 is closed ; :: thesis: verum

end;

suppose f " P1 = {[{} ,{} ]} ; :: thesis: f " P1 is closed

then f " P1 = [#] [:T,T:] by A1;
hence f " P1 is closed ; :: thesis: verum

end;

end;