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
f is bijective by Def4;
then A1: ( f is one-to-one & f is onto ) ;
then A2: rng f = [#] S by FUNCT_2:def 3;
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 g .: X is strong by Th16;
hence f " X is strong by A1, A2, TOPS_2:68; :: thesis: verum