let AS be AffinSpace; :: thesis: for K, M, P being Subset of AS st K // M holds
Plane K,P = Plane M,P
let K, M, P be Subset of AS; :: thesis: ( K // M implies Plane K,P = Plane M,P )
assume A1: K // M ; :: thesis: Plane K,P = Plane M,P

now

let x be set ; :: thesis: ( x in Plane K,P iff x in Plane M,P )

A2: now

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

end;

now

assume x in Plane K,P ; :: thesis: x in Plane M,P
then consider a being Element of AS such that
A7: x = a and
A8: ex b being Element of AS st
( a,b // K & b in P ) ;
consider b being Element of AS such that
A9: a,b // K and
A10: b in P by A8;
a,b // M by A1, A9, AFF_1:57;
hence x in Plane M,P by A7, A10; :: thesis: verum

end;

hence ( x in Plane K,P iff x in Plane M,P ) by A2; :: thesis: verum

end;

hence Plane K,P = Plane M,P by TARSKI:2; :: thesis: verum