let AS be AffinSpace; :: thesis: for a, b being Element of AS ex A being Subset of AS st
( a in A & b in A & A is being_line )
let a, b be Element of AS; :: thesis: ex A being Subset of AS st
( a in A & b in A & A is being_line )
LIN a,b,b by AFF_1:7;
then ex A being Subset of AS st
( A is being_line & a in A & b in A & b in A ) by AFF_1:21;
hence ex A being Subset of AS st
( a in A & b in A & A is being_line ) ; :: thesis: verum