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