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

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