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

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