let AS be AffinSpace; :: thesis: for a, b, c being Element of AS
for M being Subset of AS st M is being_line & a in M & b in M & a <> b & not c in M holds
not LIN a,b,c
let a, b, c be Element of AS; :: thesis: for M being Subset of AS st M is being_line & a in M & b in M & a <> b & not c in M holds
not LIN a,b,c
let M be Subset of AS; :: thesis: ( M is being_line & a in M & b in M & a <> b & not c in M implies not LIN a,b,c )
assume A1: ( M is being_line & a in M & b in M & a <> b & not c in M ) ; :: thesis: not LIN a,b,c
assume LIN a,b,c ; :: thesis: contradiction
then ex N being Subset of AS st
( N is being_line & a in N & b in N & c in N ) by AFF_1:21;
hence contradiction by A1, AFF_1:18; :: thesis: verum