let S be non empty non void TopStruct ; :: thesis:
let f be Collineation of S; :: thesis:
let X, Y be Subset of S; :: thesis:
assume that
A1: not X is trivial and
A2: not Y is trivial and
A3: X,Y are_joinable ; :: thesis:
consider g being FinSequence of bool the carrier of S such that
A4: X = g . 1 and
A5: Y = g . (len g) and
A6: for W being Subset of S st W in rng g holds
( W is closed_under_lines & W is strong ) and
A7: for i being Element of NAT st 1 <= i & i < len g holds
2 c= card ((g . i) /\ (g . (i + 1))) by A3;
deffunc H₁( set ) -> Element of bool the carrier of S = f .: (g . $1);
consider p being FinSequence such that
A8: ( len p = len g & ( for k being Nat st k in dom p holds
p . k = H₁(k) ) ) from FINSEQ_1:sch 2();
A9: dom g = Seg (len g) by FINSEQ_1:def 3;
A10: dom p = Seg (len p) by FINSEQ_1:def 3;
rng p c= bool the carrier of S

let o be object ; :: according to TARSKI:def 3 :: thesis:
assume o in rng p ; :: thesis:
then consider i being object such that
A11: i in dom p and
A12: o = p . i by FUNCT_1:def 3;
reconsider i = i as Element of NAT by A11;
g . i in rng g by A8, A10, A9, A11, FUNCT_1:3;
then reconsider gi = g . i as Subset of S ;
p . i = f .: gi by A8, A11;
hence o in bool the carrier of S by A12; :: thesis:

end;

let W be Subset of S; :: thesis:
assume W in rng p ; :: thesis:
then consider i being object such that
A13: i in dom p and
A14: W = p . i by FUNCT_1:def 3;
reconsider i = i as Element of NAT by A13;
g . i in rng g by A8, A10, A9, A13, FUNCT_1:3;
then reconsider gi = g . i as Subset of S ;
gi in rng g by A8, A10, A9, A13, FUNCT_1:3;
then A15: ( gi is strong & gi is closed_under_lines ) by A6;
p . i = f .: gi by A8, A13;
hence ( W is closed_under_lines & W is strong ) by A14, A15, Th16, Th18; :: thesis:

end;

end;