let AS be AffinSpace; for X being Subset of AS st X is being_plane holds
ex a, b, c being Element of AS st
( a in X & b in X & c in X & not LIN a,b,c )
let X be Subset of AS; ( X is being_plane implies ex a, b, c being Element of AS st
( a in X & b in X & c in X & not LIN a,b,c ) )
assume
X is being_plane
; ex a, b, c being Element of AS st
( a in X & b in X & c in X & not LIN a,b,c )
then consider K, P being Subset of AS such that
A1:
K is being_line
and
A2:
P is being_line
and
A3:
not K // P
and
A4:
X = Plane (K,P)
;
consider a, b being Element of AS such that
A5:
a in P
and
A6:
b in P
and
A7:
a <> b
by A2, AFF_1:19;
set Q = a * K;
consider c being Element of AS such that
A8:
a <> c
and
A9:
c in a * K
by A1, Th27, AFF_1:20;
take
a
; ex b, c being Element of AS st
( a in X & b in X & c in X & not LIN a,b,c )
take
b
; ex c being Element of AS st
( a in X & b in X & c in X & not LIN a,b,c )
take
c
; ( a in X & b in X & c in X & not LIN a,b,c )
A10:
P c= Plane (K,P)
by A1, Th14;
hence
( a in X & b in X )
by A4, A5, A6; ( c in X & not LIN a,b,c )
A11:
( K // a * K & a in a * K )
by A1, Def3;
then
a * K c= Plane (K,P)
by A5, A10, Lm4;
hence
c in X
by A4, A9; not LIN a,b,c
A12:
a * K is being_line
by A1, Th27;
thus
not LIN a,b,c
verumproof
assume
LIN a,
b,
c
;
contradiction
then
c in P
by A2, A5, A6, A7, AFF_1:25;
hence
contradiction
by A2, A3, A5, A11, A12, A8, A9, AFF_1:18;
verum
end;