let AS be AffinSpace; :: thesis: for K, P being Subset of AS st K // P holds
Plane K,P = P
let K, P be Subset of AS; :: thesis: ( K // P implies Plane K,P = P )
set X = Plane K,P;
assume A1: K // P ; :: thesis: Plane K,P = P
then A2: P is being_line by AFF_1:50;

now

let x be set ; :: thesis: ( x in Plane K,P implies x in P )
assume x in Plane K,P ; :: thesis: x in P
then consider a being Element of AS such that
A3: x = a and
A4: ex b being Element of AS st
( a,b // K & b in P ) ;
consider b being Element of AS such that
A5: a,b // K and
A6: b in P by A4;
a,b // P by A1, A5, AFF_1:57;
then b,a // P by AFF_1:48;
hence x in P by A2, A3, A6, AFF_1:37; :: thesis: verum

end;

then A7: Plane K,P c= P by TARSKI:def 3;
K is being_line by A1, AFF_1:50;
then P c= Plane K,P by Th14;
hence Plane K,P = P by A7, XBOOLE_0:def 10; :: thesis: verum