let POS be OrtAfSp; :: thesis: for K being Subset of POS
for a, b being Element of POS st a in K & b in K & a <> b & K is being_line holds
K = Line (a,b)
let K be Subset of POS; :: thesis: for a, b being Element of POS st a in K & b in K & a <> b & K is being_line holds
K = Line (a,b)
let a, b be Element of POS; :: thesis: ( a in K & b in K & a <> b & K is being_line implies K = Line (a,b) )
assume that
A1: ( a in K & b in K & a <> b ) and
A2: K is being_line ; :: thesis: K = Line (a,b)
reconsider a9 = a, b9 = b as Element of AffinStruct(# the carrier of POS, the CONGR of POS #) ;
reconsider K9 = K as Subset of AffinStruct(# the carrier of POS, the CONGR of POS #) ;
K9 is being_line by A2, Th43;
then K9 = Line (a9,b9) by A1, AFF_1:57;
hence K = Line (a,b) by Th41; :: thesis: verum