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 ; :: 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) ; :: 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 A1, TARSKI:def 1; :: 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 A2, A3, FINSEQ_1:40; :: thesis: verum