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

let o be set ; :: according to TARSKI:def 3 :: thesis:
assume o in rng p ; :: thesis:
then consider i being set such that
A7: ( i in dom p & o = p . i ) by FUNCT_1:def 5;
reconsider i = i as Element of NAT by A7;
g . i in rng g by A4, A6, A7, FUNCT_1:12;
then reconsider gi = g . i as Subset of S ;
p . i = f .: gi by A4, A7;
hence o in bool the carrier of S by A7; :: thesis:

end;

then reconsider p = p as FinSequence of bool the carrier of S by FINSEQ_1:def 4;
take p ; :: according to PENCIL_2:def 3 :: thesis:
1 in dom g by A2, A3, FUNCT_1:def 4;
hence f .: X = p . 1 by A3, A4, A6; :: thesis:
len g in dom g by A2, A3, FUNCT_1:def 4;
hence f .: Y = p . (len p) by A3, A4, A6; :: thesis:
thus for W being Subset of S st W in rng p holds
( W is closed_under_lines & W is strong ) :: thesis:

let W be Subset of S; :: thesis:
assume W in rng p ; :: thesis:
then consider i being set such that
A8: ( i in dom p & W = p . i ) by FUNCT_1:def 5;
reconsider i = i as Element of NAT by A8;
g . i in rng g by A4, A6, A8, FUNCT_1:12;
then reconsider gi = g . i as Subset of S ;
gi in rng g by A4, A6, A8, FUNCT_1:12;
then A9: ( gi is strong & gi is closed_under_lines ) by A3;
p . i = f .: gi by A4, A8;
hence ( W is closed_under_lines & W is strong ) by A8, A9, Th16, Th18; :: thesis:

end;

thus for i being Element of NAT st 1 <= i & i < len p holds
2 c= card ((p . i) /\ (p . (i + 1))) :: thesis:

let i be Element of NAT ; :: thesis:
assume A10: ( 1 <= i & i < len p ) ; :: thesis:
then A11: 2 c= card ((g . i) /\ (g . (i + 1))) by A3, A4;
i in dom g by A4, A10, FINSEQ_3:27;
then A12: g . i in rng g by FUNCT_1:12;
(g . i) /\ (g . (i + 1)) c= g . i by XBOOLE_1:17;
then reconsider gg = (g . i) /\ (g . (i + 1)) as Subset of S by A12, XBOOLE_1:1;
i in dom g by A4, A10, FINSEQ_3:27;
then A13: p . i = f .: (g . i) by A4, A6;
A14: 1 <= i + 1 by A10, NAT_1:13;
i + 1 <= len p by A10, NAT_1:13;
then i + 1 in dom p by A14, FINSEQ_3:27;
then A15: p . (i + 1) = f .: (g . (i + 1)) by A4;
not gg is trivial by A11, PENCIL_1:4;
then not f .: gg is trivial by Th14;
then not (f .: (g . i)) /\ (f .: (g . (i + 1))) is trivial by A1, FUNCT_1:121;
hence 2 c= card ((p . i) /\ (p . (i + 1))) by A13, A15, PENCIL_1:4; :: thesis:

end;