let A1, A2 be Element of L; :: thesis: ( a [= A1 & b [= A1 & ( for x being Element of L st a [= x & b [= x holds
A1 [= x ) & a [= A2 & b [= A2 & ( for x being Element of L st a [= x & b [= x holds
A2 [= x ) implies A1 = A2 )
assume that
A1: ( a [= A1 & b [= A1 & ( for x being Element of L st a [= x & b [= x holds
A1 [= x ) ) and
A2: ( a [= A2 & b [= A2 & ( for x being Element of L st a [= x & b [= x holds
A2 [= x ) ) ; :: thesis: A1 = A2
a3: A1 [= A2 by A1, A2;
B2: A2 [= A1 by A1, A2;
A1 [= A1 by ISum;
hence A1 = A2 by a3, DefB2, B2; :: thesis: verum