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

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