let POS be OrtAfSp; :: thesis: for a, b being Element of POS
for a9, b9 being Element of AffinStruct(# the carrier of POS, the CONGR of POS #) st a = a9 & b = b9 holds
Line (a,b) = Line (a9,b9)
let a, b be Element of POS; :: thesis: for a9, b9 being Element of AffinStruct(# the carrier of POS, the CONGR of POS #) st a = a9 & b = b9 holds
Line (a,b) = Line (a9,b9)
let a9, b9 be Element of AffinStruct(# the carrier of POS, the CONGR of POS #); :: thesis: ( a = a9 & b = b9 implies Line (a,b) = Line (a9,b9) )
assume A1: ( a = a9 & b = b9 ) ; :: thesis: Line (a,b) = Line (a9,b9)
set X = Line (a,b);
set Y = Line (a9,b9);

now :: thesis: for x1 being object holds
( x1 in Line (a,b) iff x1 in Line (a9,b9) )

let x1 be object ; :: thesis: ( x1 in Line (a,b) iff x1 in Line (a9,b9) )

A2: now :: thesis: ( x1 in Line (a9,b9) implies x1 in Line (a,b) )

assume A3: x1 in Line (a9,b9) ; :: thesis: x1 in Line (a,b)
then reconsider x9 = x1 as Element of AffinStruct(# the carrier of POS, the CONGR of POS #) ;
reconsider x = x9 as Element of POS ;
LIN a9,b9,x9 by A3, AFF_1:def 2;
then LIN a,b,x by A1, Th40;
hence x1 in Line (a,b) by Def10; :: thesis: verum

end;

now :: thesis: ( x1 in Line (a,b) implies x1 in Line (a9,b9) )

assume A4: x1 in Line (a,b) ; :: thesis: x1 in Line (a9,b9)
then reconsider x = x1 as Element of POS ;
reconsider x9 = x as Element of AffinStruct(# the carrier of POS, the CONGR of POS #) ;
LIN a,b,x by A4, Def10;
then LIN a9,b9,x9 by A1, Th40;
hence x1 in Line (a9,b9) by AFF_1:def 2; :: thesis: verum

end;

hence ( x1 in Line (a,b) iff x1 in Line (a9,b9) ) by A2; :: thesis: verum

end;

hence Line (a,b) = Line (a9,b9) by TARSKI:2; :: thesis: verum