let T be TopStruct ; :: thesis:
let S be Subset of T; :: thesis:
assume A1: S is trivial ; :: thesis:
thus S is strong :: thesis:

proof

let x, y be Point of T; :: according to PENCIL_1:def 3 :: thesis:
assume A2: ( x in S & y in S ) ; :: thesis:
thus x,y are_collinear :: thesis:

proof

per cases ;

suppose x = y ; :: thesis:

hence x,y are_collinear ; :: thesis:

end;

suppose x <> y ; :: thesis:

then 2 c= card S by A2, Th2;
hence x,y are_collinear by A1, Th4; :: thesis:

end;

end;

end;

end;

thus S is closed_under_lines :: thesis:

proof

let l be Block of T; :: according to PENCIL_1:def 2 :: thesis:
A3: card (l /\ S) c= card S by CARD_1:11, XBOOLE_1:17;
assume 2 c= card (l /\ S) ; :: thesis:
then 2 c= card S by A3;
hence l c= S by A1, Th4; :: thesis:

end;