defpred S1[ set ] means for y being Element of AS st y = $1 holds
LIN a,b,y;
consider X being Subset of AS such that
A1:
for x being set holds
( x in X iff ( x in the carrier of AS & S1[x] ) )
from SUBSET_1:sch 1();
take
X
; for x being Element of AS holds
( x in X iff LIN a,b,x )
let x be Element of AS; ( x in X iff LIN a,b,x )
thus
( x in X implies LIN a,b,x )
by A1; ( LIN a,b,x implies x in X )
assume
LIN a,b,x
; x in X
then
for y being Element of AS st y = x holds
LIN a,b,y
;
hence
x in X
by A1; verum