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

( 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