let POS be OrtAfSp; :: thesis: for a, b being Element of POS
for a9, b9 being Element of (Af 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 (Af POS) st a = a9 & b = b9 holds
Line (a,b) = Line (a9,b9)
let a9, b9 be Element of (Af 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

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

A2: now

assume A3: x1 in Line (a9,b9) ; :: thesis: x1 in Line (a,b)
then reconsider x9 = x1 as Element of (Af 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, Th55;
hence x1 in Line (a,b) by Def12; :: thesis: verum

end;

now

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 (Af POS) ;
LIN a,b,x by A4, Def12;
then LIN a9,b9,x9 by A1, Th55;
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:1; :: thesis: verum