let S be TopStruct ; :: thesis: for X being Subset of S st X is closed_under_lines & X is strong holds
X,X are_joinable

let X be Subset of S; :: thesis: ( X is closed_under_lines & X is strong implies X,X are_joinable )
assume A1: ( X is closed_under_lines & X is strong ) ; :: thesis: X,X are_joinable
reconsider f = <*X*> as FinSequence of bool the carrier of S ;
take f ; :: according to PENCIL_2:def 3 :: thesis: ( X = f . 1 & X = f . (len f) & ( for W being Subset of S st W in rng f holds
( W is closed_under_lines & W is strong ) ) & ( for i being Element of NAT st 1 <= i & i < len f holds
2 c= card ((f . i) /\ (f . (i + 1))) ) )

thus X = f . 1 by FINSEQ_1:40; :: thesis: ( X = f . (len f) & ( for W being Subset of S st W in rng f holds
( W is closed_under_lines & W is strong ) ) & ( for i being Element of NAT st 1 <= i & i < len f holds
2 c= card ((f . i) /\ (f . (i + 1))) ) )

len f = 1 by FINSEQ_1:40;
hence X = f . (len f) by FINSEQ_1:40; :: thesis: ( ( for W being Subset of S st W in rng f holds
( W is closed_under_lines & W is strong ) ) & ( for i being Element of NAT st 1 <= i & i < len f holds
2 c= card ((f . i) /\ (f . (i + 1))) ) )

thus for W being Subset of S st W in rng f holds
( W is closed_under_lines & W is strong ) :: thesis: for i being Element of NAT st 1 <= i & i < len f holds
2 c= card ((f . i) /\ (f . (i + 1)))
proof
let W be Subset of S; :: thesis: ( W in rng f implies ( W is closed_under_lines & W is strong ) )
assume W in rng f ; :: thesis: ( W is closed_under_lines & W is strong )
then W in {X} by FINSEQ_1:38;
hence ( W is closed_under_lines & W is strong ) by ; :: thesis: verum
end;
let i be Element of NAT ; :: thesis: ( 1 <= i & i < len f implies 2 c= card ((f . i) /\ (f . (i + 1))) )
assume that
A2: 1 <= i and
A3: i < len f ; :: thesis: 2 c= card ((f . i) /\ (f . (i + 1)))
thus 2 c= card ((f . i) /\ (f . (i + 1))) by ; :: thesis: verum