let POS be OrtAfSp; :: thesis: for K being Subset of
for a, b being Element of st a in K & b in K & a <> b & K is being_line holds
K = Line a,b
let K be Subset of ; :: thesis: for a, b being Element of st a in K & b in K & a <> b & K is being_line holds
K = Line a,b
let a, b be Element of ; :: 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 a' = a, b' = b as Element of ;
reconsider K' = K as Subset of ;
K' is being_line by A2, Th58;
then K' = Line a',b' by A1, AFF_1:71;
hence K = Line a,b by Th56; :: thesis: verum