let T be TopStruct ; :: thesis: for S being Subset of T st S is trivial holds
( S is strong & S is closed_under_lines )
let S be Subset of T; :: thesis: ( S is trivial implies ( S is strong & S is closed_under_lines ) )
assume A1: S is trivial ; :: thesis: ( S is strong & S is closed_under_lines )
thus S is strong :: thesis: S is closed_under_lines

proof

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

proof

per cases ( x = y or x <> y ) ;

suppose x = y ; :: thesis: x,y are_collinear

hence x,y are_collinear ; :: thesis: verum

end;

suppose x <> y ; :: thesis: x,y are_collinear

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

end;

end;

end;

end;

thus S is closed_under_lines :: thesis: verum

proof

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

end;