let AS be AffinSpace; :: thesis: 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; :: thesis: ( 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
; :: thesis: 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 & P is being_line & not K // P )
and
A2:
X = Plane K,P
by Def2;
consider a, b being Element of AS such that
A3:
( a in P & b in P )
and
A4:
a <> b
by A1, AFF_1:31;
set Q = a * K;
A5:
( K // a * K & a in a * K & a * K is being_line )
by A1, Def3, Th27;
then consider c being Element of AS such that
A6:
a <> c
and
A7:
c in a * K
by AFF_1:32;
take
a
; :: thesis: ex b, c being Element of AS st
( a in X & b in X & c in X & not LIN a,b,c )
take
b
; :: thesis: ex c being Element of AS st
( a in X & b in X & c in X & not LIN a,b,c )
take
c
; :: thesis: ( a in X & b in X & c in X & not LIN a,b,c )
A8:
P c= Plane K,P
by A1, Th14;
hence
( a in X & b in X )
by A2, A3; :: thesis: ( c in X & not LIN a,b,c )
a * K c= Plane K,P
by A1, A3, A5, A8, Lm4;
hence
c in X
by A2, A7; :: thesis: not LIN a,b,c
thus
not LIN a,b,c
:: thesis: verumproof
assume
LIN a,
b,
c
;
:: thesis: contradiction
then
c in P
by A1, A3, A4, AFF_1:39;
hence
contradiction
by A1, A3, A5, A6, A7, AFF_1:30;
:: thesis: verum
end;