let POS be OrtAfSp; :: thesis: for a, b being Element of
for a', b' being Element of st a = a' & b = b' holds
Line a,b = Line a',b'
let a, b be Element of ; :: thesis: for a', b' being Element of st a = a' & b = b' holds
Line a,b = Line a',b'
let a', b' be Element of ; :: thesis: ( a = a' & b = b' implies Line a,b = Line a',b' )
assume A1: ( a = a' & b = b' ) ; :: thesis: Line a,b = Line a',b'
set X = Line a,b;
set Y = Line a',b';

now

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

A2: now

assume A3: x1 in Line a',b' ; :: thesis: x1 in Line a,b
then reconsider x' = x1 as Element of ;
reconsider x = x' as Element of ;
LIN a',b',x' 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 a',b'
then reconsider x = x1 as Element of ;
reconsider x' = x as Element of ;
LIN a,b,x by A4, Def12;
then LIN a',b',x' by A1, Th55;
hence x1 in Line a',b' by AFF_1:def 2; :: thesis: verum

end;

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

end;

hence Line a,b = Line a',b' by TARSKI:2; :: thesis: verum