let S be non empty non void TopStruct ; :: thesis: for f being Collineation of S
for X being Subset of S st X is strong holds
f " X is strong
let f be Collineation of S; :: thesis: for X being Subset of S st X is strong holds
f " X is strong
reconsider g = f " as Collineation of S by Th13;
let X be Subset of S; :: thesis: ( X is strong implies f " X is strong )
assume X is strong ; :: thesis: f " X is strong
then A1: g .: X is strong by Th16;
A2: f is bijective by Def4;
then rng f = [#] S by FUNCT_2:def 3;
hence f " X is strong by A2, A1, TOPS_2:55; :: thesis: verum