let S be IncStruct ; :: thesis: for F, G being Subset of the Points of S st G c= F & F is linear holds
G is linear
let F, G be Subset of the Points of S; :: thesis: ( G c= F & F is linear implies G is linear )
assume that
A1: G c= F and
A2: F is linear ; :: thesis: G is linear
consider L being LINE of S such that
A3: F on L by A2;
take L ; :: according to INCSP_1:def 6 :: thesis: G on L
let A be POINT of S; :: according to INCSP_1:def 4 :: thesis: ( A in G implies A on L )
assume A in G ; :: thesis: A on L
hence A on L by A1, A3; :: thesis: verum