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 ) and
A2: a <> b and
A3: K is being_line ; :: thesis: K = Line a,b
reconsider K' = K as Subset of (Af POS) ;
reconsider a' = a, b' = b as Element of (Af POS) ;
K' is being_line by A3, Th58;
then K' = Line a',b' by A1, A2, AFF_1:71;
hence K = Line a,b by Th56; :: thesis: verum