let S be IncStruct ; :: thesis: for P being PLANE of S
for G, F being Subset of the Points of S st G c= F & F on P holds
G on P
let P be PLANE of S; :: thesis: for G, F being Subset of the Points of S st G c= F & F on P holds
G on P
let G, F be Subset of the Points of S; :: thesis: ( G c= F & F on P implies G on P )
assume that
A1: G c= F and
A2: F on P ; :: 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, A2, Def5; :: thesis: verum