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 )
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
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 H1( 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 = H1(k) ) ) from 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
proof
let o be object ; :: according to TARSKI:def 3 :: thesis: ( not o in rng p or o in bool the carrier of S )
assume o in rng p ; :: thesis: o in bool the carrier of S
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 ;
then reconsider gi = g . i as Subset of S ;
p . i = f .: gi by ;
hence o in bool the carrier of S by A12; :: thesis: verum
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: ( f .: X = p . 1 & f .: Y = p . (len p) & ( for W being Subset of S st W in rng p holds
( W is closed_under_lines & W is strong ) ) & ( for i being Element of NAT st 1 <= i & i < len p holds
2 c= card ((p . i) /\ (p . (i + 1))) ) )

1 in dom g by ;
hence f .: X = p . 1 by A4, A8, A10, A9; :: thesis: ( f .: Y = p . (len p) & ( for W being Subset of S st W in rng p holds
( W is closed_under_lines & W is strong ) ) & ( for i being Element of NAT st 1 <= i & i < len p holds
2 c= card ((p . i) /\ (p . (i + 1))) ) )

len g in dom g by ;
hence f .: Y = p . (len p) by A5, A8, A10, A9; :: thesis: ( ( for W being Subset of S st W in rng p holds
( W is closed_under_lines & W is strong ) ) & ( for i being Element of NAT st 1 <= i & i < len p holds
2 c= card ((p . i) /\ (p . (i + 1))) ) )

thus for W being Subset of S st W in rng p holds
( W is closed_under_lines & W is strong ) :: thesis: for i being Element of NAT st 1 <= i & i < len p holds
2 c= card ((p . i) /\ (p . (i + 1)))
proof
let W be Subset of S; :: thesis: ( W in rng p implies ( W is closed_under_lines & W is strong ) )
assume W in rng p ; :: thesis: ( W is closed_under_lines & W is strong )
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 ;
then reconsider gi = g . i as Subset of S ;
gi in rng g by ;
then A15: ( gi is strong & gi is closed_under_lines ) by A6;
p . i = f .: gi by ;
hence ( W is closed_under_lines & W is strong ) by ; :: thesis: verum
end;
A16: f is bijective by Def4;
thus for i being Element of NAT st 1 <= i & i < len p holds
2 c= card ((p . i) /\ (p . (i + 1))) :: thesis: verum
proof
let i be Element of NAT ; :: thesis: ( 1 <= i & i < len p implies 2 c= card ((p . i) /\ (p . (i + 1))) )
assume that
A17: 1 <= i and
A18: i < len p ; :: thesis: 2 c= card ((p . i) /\ (p . (i + 1)))
A19: (g . i) /\ (g . (i + 1)) c= g . i by XBOOLE_1:17;
i in dom g by ;
then g . i in rng g by FUNCT_1:3;
then reconsider gg = (g . i) /\ (g . (i + 1)) as Subset of S by ;
2 c= card ((g . i) /\ (g . (i + 1))) by A7, A8, A17, A18;
then not gg is trivial by PENCIL_1:4;
then not f .: gg is trivial by Th14;
then A20: not (f .: (g . i)) /\ (f .: (g . (i + 1))) is trivial by ;
A21: i + 1 <= len p by ;
1 <= i + 1 by ;
then i + 1 in dom p by ;
then A22: p . (i + 1) = f .: (g . (i + 1)) by A8;
i in dom g by ;
then p . i = f .: (g . i) by A8, A10, A9;
hence 2 c= card ((p . i) /\ (p . (i + 1))) by ; :: thesis: verum
end;