let X1, X2 be Subset of AS; ( ( for x being Element of AS holds
( x in X1 iff LIN a,b,x ) ) & ( for x being Element of AS holds
( x in X2 iff LIN a,b,x ) ) implies X1 = X2 )
assume that
A2:
for x being Element of AS holds
( x in X1 iff LIN a,b,x )
and
A3:
for x being Element of AS holds
( x in X2 iff LIN a,b,x )
; X1 = X2
for x being object holds
( x in X1 iff x in X2 )
by A2, A3;
hence
X1 = X2
by TARSKI:2; verum