let S be IncSpace; :: thesis: for L being LINE of S
for P being PLANE of S
for F being Subset of the Points of S st F on L & L on P holds
F on P
let L be LINE of S; :: thesis: for P being PLANE of S
for F being Subset of the Points of S st F on L & L on P holds
F on P
let P be PLANE of S; :: thesis: for F being Subset of the Points of S st F on L & L on P holds
F on P
let F be Subset of the Points of S; :: thesis: ( F on L & L on P implies F on P )
assume that
A1: F on L and
A2: L on P ; :: thesis: F on P
let A be POINT of S; :: according to INCSP_1:def 5 :: thesis: ( A in F implies A on P )
assume A in F ; :: thesis: A on P
then A on L by A1, Def4;
hence A on P by A2, Def17; :: thesis: verum