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

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 )

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

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

hence
contradiction
by A1, DIRAF:def 7; :: thesis: verum
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 ) )

set M = Line (a,b);

set N = Line (c,d);

A4: ( a in Line (a,b) & b in Line (a,b) ) by AFF_1:15;

A5: ( c in Line (c,d) & d in Line (c,d) ) by AFF_1:15;

assume A6: not a,b // c,d ; :: thesis: ex q being Element of AS st

( a,b // a,q & c,d // c,q )

then A7: a <> b by AFF_1:3;

then A8: Line (a,b) is being_line by AFF_1:def 3;

A9: c <> d by A6, AFF_1:3;

then A10: Line (c,d) is being_line by AFF_1:def 3;

( c in X & d in X ) by A3;

then A11: Line (c,d) c= X by A2, A9, Th19;

( a in X & b in X ) by A3;

then Line (a,b) c= X by A2, A7, Th19;

then consider q being Element of AS such that

A12: q in Line (a,b) and

A13: q in Line (c,d) by A2, A6, A11, A8, A10, A4, A5, Th22, AFF_1:39;

LIN c,d,q by A10, A5, A13, AFF_1:21;

then A14: c,d // c,q by AFF_1:def 1;

LIN a,b,q by A8, A4, A12, AFF_1:21;

then a,b // a,q by AFF_1:def 1;

hence ex q being Element of AS st

( a,b // a,q & c,d // c,q ) by A14; :: thesis: verum

end;( a,b // a,q & c,d // c,q ) )

set M = Line (a,b);

set N = Line (c,d);

A4: ( a in Line (a,b) & b in Line (a,b) ) by AFF_1:15;

A5: ( c in Line (c,d) & d in Line (c,d) ) by AFF_1:15;

assume A6: not a,b // c,d ; :: thesis: ex q being Element of AS st

( a,b // a,q & c,d // c,q )

then A7: a <> b by AFF_1:3;

then A8: Line (a,b) is being_line by AFF_1:def 3;

A9: c <> d by A6, AFF_1:3;

then A10: Line (c,d) is being_line by AFF_1:def 3;

( c in X & d in X ) by A3;

then A11: Line (c,d) c= X by A2, A9, Th19;

( a in X & b in X ) by A3;

then Line (a,b) c= X by A2, A7, Th19;

then consider q being Element of AS such that

A12: q in Line (a,b) and

A13: q in Line (c,d) by A2, A6, A11, A8, A10, A4, A5, Th22, AFF_1:39;

LIN c,d,q by A10, A5, A13, AFF_1:21;

then A14: c,d // c,q by AFF_1:def 1;

LIN a,b,q by A8, A4, A12, AFF_1:21;

then a,b // a,q by AFF_1:def 1;

hence ex q being Element of AS st

( a,b // a,q & c,d // c,q ) by A14; :: thesis: verum