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:36;

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; :: thesis: verum

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:36;

now :: thesis: for x being object st x in Plane (K,P) holds

x in P

then A7:
Plane (K,P) c= P
;x in P

let x be object ; :: 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:43;

then b,a // P by AFF_1:34;

hence x in P by A2, A3, A6, AFF_1:23; :: thesis: verum

end;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:43;

then b,a // P by AFF_1:34;

hence x in P by A2, A3, A6, AFF_1:23; :: thesis: verum

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; :: thesis: verum