let AS be AffinSpace; :: thesis: for X being Subset of AS st AS is not AffinPlane & X is being_plane holds
ex q being Element of AS st not q in X
let X be Subset of AS; :: thesis: ( AS is not AffinPlane & X is being_plane implies ex q being Element of AS st not q in X )
assume that
A1: AS is not AffinPlane and
A2: X is being_plane ; :: thesis: not for q being Element of AS holds q in X
assume A3: for q being Element of AS holds q in X ; :: thesis: contradiction
A4: the carrier of AS c= X

proof

for x being set st x in the carrier of AS holds
x in X by A3;
hence the carrier of AS c= X by TARSKI:def 3; :: thesis: verum

end;

for a, b, c, d being Element of AS st not a,b // c,d holds
ex q being Element of AS st
( a,b // a,q & c,d // c,q )

proof

let a, b, c, d be Element of AS; :: thesis: ( not a,b // c,d implies ex q being Element of AS st
( a,b // a,q & c,d // c,q ) )
assume A5: not a,b // c,d ; :: thesis: ex q being Element of AS st
( a,b // a,q & c,d // c,q )
then A6: ( a <> b & c <> d ) by AFF_1:12;
set M = Line a,b;
set N = Line c,d;
( a in X & b in X & c in X & d in X ) by A4, TARSKI:def 3;
then A7: ( Line a,b c= X & Line c,d c= X ) by A2, A6, Th19;
A8: ( Line a,b is being_line & Line c,d is being_line ) by A6, AFF_1:def 3;
A10: ( a in Line a,b & b in Line a,b & c in Line c,d & d in Line c,d ) by AFF_1:26;
then consider q being Element of AS such that
A11: ( q in Line a,b & q in Line c,d ) by A5, A8, A2, A7, Th22, AFF_1:53;
( LIN a,b,q & LIN c,d,q ) by A8, A10, A11, AFF_1:33;
then ( a,b // a,q & c,d // c,q ) by AFF_1:def 1;
hence ex q being Element of AS st
( a,b // a,q & c,d // c,q ) ; :: thesis: verum

end;

hence contradiction by A1, DIRAF:def 8; :: thesis: verum