let AS be AffinSpace; for K, P being Subset of AS st K // P holds
Plane (K,P) = P
let K, P be Subset of AS; ( K // P implies Plane (K,P) = P )
set X = Plane (K,P);
assume A1:
K // P
; Plane (K,P) = P
then A2:
P is being_line
by AFF_1:36;
now for x being object st x in Plane (K,P) holds
x in Plet x be
object ;
( x in Plane (K,P) implies x in P )assume
x in Plane (
K,
P)
;
x in Pthen 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:43;
then
b,
a // P
by AFF_1:34;
hence
x in P
by A2, A3, A6, AFF_1:23;
verum end;
then A7:
Plane (K,P) c= P
;
K is being_line
by A1, AFF_1:36;
then
P c= Plane (K,P)
by Th14;
hence
Plane (K,P) = P
by A7, XBOOLE_0:def 10; verum