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