let AS be AffinSpace; :: thesis: for K, P being Subset of AS st K is being_line holds
P c= Plane (K,P)
let K, P be Subset of AS; :: thesis: ( K is being_line implies P c= Plane (K,P) )
assume A1: K is being_line ; :: thesis: P c= Plane (K,P)
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in P or x in Plane (K,P) )
assume A2: x in P ; :: thesis: x in Plane (K,P)
then reconsider a = x as Element of AS ;
a,a // K by A1, AFF_1:33;
hence x in Plane (K,P) by A2; :: thesis: verum