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