let POS be OrtAfSp; :: thesis: for a, b being Element of POS
for a', b' being Element of (Af POS) st a = a' & b = b' holds
Line a,b = Line a',b'
let a, b be Element of POS; :: thesis: for a', b' being Element of (Af POS) st a = a' & b = b' holds
Line a,b = Line a',b'
let a', b' be Element of (Af POS); :: 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 POS ;
reconsider x' = x as Element of the carrier of (Af POS) ;
LIN a,b,x by A3, Def12;
then LIN a',b',x' by A1, Th55;
hence x1 in Line a',b' by AFF_1:def 2; :: thesis: verum

end;

now

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