let S be IncStruct ; :: thesis: for F, G being Subset of the Points of S st G c= F & F is planar holds

G is planar

let F, G be Subset of the Points of S; :: thesis: ( G c= F & F is planar implies G is planar )

assume that

A1: G c= F and

A2: F is planar ; :: thesis: G is planar

consider P being PLANE of S such that

A3: F on P by A2;

take P ; :: according to INCSP_1:def 7 :: thesis: G on P

let A be POINT of S; :: according to INCSP_1:def 5 :: thesis: ( A in G implies A on P )

assume A in G ; :: thesis: A on P

hence A on P by A1, A3; :: thesis: verum

G is planar

let F, G be Subset of the Points of S; :: thesis: ( G c= F & F is planar implies G is planar )

assume that

A1: G c= F and

A2: F is planar ; :: thesis: G is planar

consider P being PLANE of S such that

A3: F on P by A2;

take P ; :: according to INCSP_1:def 7 :: thesis: G on P

let A be POINT of S; :: according to INCSP_1:def 5 :: thesis: ( A in G implies A on P )

assume A in G ; :: thesis: A on P

hence A on P by A1, A3; :: thesis: verum