let AS be AffinSpace; 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; ( K // M implies Plane (K,P) = Plane (M,P) )
assume A1:
K // M
; Plane (K,P) = Plane (M,P)
hence
Plane (K,P) = Plane (M,P)
by TARSKI:2; verum