for S being IncStruct
for L being LINE of S
for F, G being Subset of the Points of S st G c= F & F on L holds
G on L ;