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