theorem :: PENCIL_1:19

for T being TopStruct
for S being Subset of T st S is trivial holds
( S is strong & S is closed_under_lines )