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 H_{1}( 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_{1}(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

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 A1, A4, FUNCT_1:def 2;

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 A2, A5, FUNCT_1:def 2;

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)))

thus for i being Element of NAT st 1 <= i & i < len p holds

2 c= card ((p . i) /\ (p . (i + 1))) :: thesis: verum

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 H

consider p being FinSequence such that

A8: ( len p = len g & ( for k being Nat st k in dom p holds

p . k = H

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

then reconsider p = p as FinSequence of bool the carrier of S by FINSEQ_1:def 4;
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 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: verum

end;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 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: verum

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 A1, A4, FUNCT_1:def 2;

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 A2, A5, FUNCT_1:def 2;

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

A16:
f is bijective
by Def4;
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 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: verum

end;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 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: verum

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 A8, A17, A18, FINSEQ_3:25;

then g . i in rng g by FUNCT_1:3;

then reconsider gg = (g . i) /\ (g . (i + 1)) as Subset of S by A19, XBOOLE_1:1;

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 A16, FUNCT_1:62;

A21: i + 1 <= len p by A18, NAT_1:13;

1 <= i + 1 by A17, NAT_1:13;

then i + 1 in dom p by A21, FINSEQ_3:25;

then A22: p . (i + 1) = f .: (g . (i + 1)) by A8;

i in dom g by A8, A17, A18, FINSEQ_3:25;

then p . i = f .: (g . i) by A8, A10, A9;

hence 2 c= card ((p . i) /\ (p . (i + 1))) by A22, A20, PENCIL_1:4; :: thesis: verum

end;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 A8, A17, A18, FINSEQ_3:25;

then g . i in rng g by FUNCT_1:3;

then reconsider gg = (g . i) /\ (g . (i + 1)) as Subset of S by A19, XBOOLE_1:1;

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 A16, FUNCT_1:62;

A21: i + 1 <= len p by A18, NAT_1:13;

1 <= i + 1 by A17, NAT_1:13;

then i + 1 in dom p by A21, FINSEQ_3:25;

then A22: p . (i + 1) = f .: (g . (i + 1)) by A8;

i in dom g by A8, A17, A18, FINSEQ_3:25;

then p . i = f .: (g . i) by A8, A10, A9;

hence 2 c= card ((p . i) /\ (p . (i + 1))) by A22, A20, PENCIL_1:4; :: thesis: verum