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

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