let AS be AffinSpace; for a being Element of AS
for Q, K, P being Subset of AS st a in Q & a in Plane K,P & K // Q holds
Q c= Plane K,P
let a be Element of AS; for Q, K, P being Subset of AS st a in Q & a in Plane K,P & K // Q holds
Q c= Plane K,P
let Q, K, P be Subset of AS; ( a in Q & a in Plane K,P & K // Q implies Q c= Plane K,P )
assume that
A1:
a in Q
and
A2:
a in Plane K,P
and
A3:
K // Q
; Q c= Plane K,P
now A4:
Plane K,
P = Plane Q,
P
by A3, Th16;
let x be
set ;
( x in Q implies x in Plane K,P )assume A5:
x in Q
;
x in Plane K,Preconsider c =
x as
Element of
AS by A5;
A6:
Q is
being_line
by A3, AFF_1:50;
consider b being
Element of
AS such that A7:
a,
b // K
and A8:
b in P
by A2, Lm3;
a,
b // Q
by A3, A7, AFF_1:57;
then
b in Q
by A1, A6, AFF_1:37;
then
c,
b // Q
by A5, A6, AFF_1:37;
hence
x in Plane K,
P
by A8, A4;
verum end;
hence
Q c= Plane K,P
by TARSKI:def 3; verum