let POS be non empty ParOrtStr ; :: thesis: for a, b, c, d being Element of POS
for a', b', c', d' being Element of (Af POS) st a = a' & b = b' & c = c' & d = d' holds
( a,b // c,d iff a',b' // c',d' )
let a, b, c, d be Element of POS; :: thesis: for a', b', c', d' being Element of (Af POS) st a = a' & b = b' & c = c' & d = d' holds
( a,b // c,d iff a',b' // c',d' )
let a', b', c', d' be Element of the carrier of (Af POS); :: thesis: ( a = a' & b = b' & c = c' & d = d' implies ( a,b // c,d iff a',b' // c',d' ) )
assume A1: ( a = a' & b = b' & c = c' & d = d' ) ; :: thesis: ( a,b // c,d iff a',b' // c',d' )
set AF = Af POS;

hereby :: thesis: ( a',b' // c',d' implies a,b // c,d )

assume a,b // c,d ; :: thesis: a',b' // c',d'
then [[a',b'],[c',d']] in the CONGR of (Af POS) by A1, ANALOAF:def 2;
hence a',b' // c',d' by ANALOAF:def 2; :: thesis: verum

end;

assume a',b' // c',d' ; :: thesis: a,b // c,d
then [[a,b],[c,d]] in the CONGR of POS by A1, ANALOAF:def 2;
hence a,b // c,d by ANALOAF:def 2; :: thesis: verum