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:2; :: thesis: verum