let S be non empty non void TopStruct ; 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; 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; ( 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
; 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; verum