let S be non empty non void TopStruct ; :: thesis: for f being Collineation of S

for X, Y being Subset of S st not X is trivial & not Y is trivial & X,Y are_joinable holds

f " X,f " Y are_joinable

let f be Collineation of S; :: thesis: for X, Y being Subset of S st not X is trivial & not Y is trivial & X,Y are_joinable holds

f " X,f " Y are_joinable

let X, Y be Subset of S; :: thesis: ( not X is trivial & not Y is trivial & X,Y are_joinable implies f " X,f " Y are_joinable )

reconsider g = f " as Collineation of S by Th13;

assume that

A1: not X is trivial and

A2: not Y is trivial and

A3: X,Y are_joinable ; :: thesis: f " X,f " Y are_joinable

A4: f is bijective by Def4;

then A5: rng f = [#] S by FUNCT_2:def 3;

then A6: f " Y = g .: Y by A4, TOPS_2:55;

f " X = g .: X by A4, A5, TOPS_2:55;

hence f " X,f " Y are_joinable by A6, A1, A2, A3, Th20; :: thesis: verum

for X, Y being Subset of S st not X is trivial & not Y is trivial & X,Y are_joinable holds

f " X,f " Y are_joinable

let f be Collineation of S; :: thesis: for X, Y being Subset of S st not X is trivial & not Y is trivial & X,Y are_joinable holds

f " X,f " Y are_joinable

let X, Y be Subset of S; :: thesis: ( not X is trivial & not Y is trivial & X,Y are_joinable implies f " X,f " Y are_joinable )

reconsider g = f " as Collineation of S by Th13;

assume that

A1: not X is trivial and

A2: not Y is trivial and

A3: X,Y are_joinable ; :: thesis: f " X,f " Y are_joinable

A4: f is bijective by Def4;

then A5: rng f = [#] S by FUNCT_2:def 3;

then A6: f " Y = g .: Y by A4, TOPS_2:55;

f " X = g .: X by A4, A5, TOPS_2:55;

hence f " X,f " Y are_joinable by A6, A1, A2, A3, Th20; :: thesis: verum