defpred S₁[ 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 & S₁[x] ) ) from SUBSET_1:sch 1();
take X ; :: thesis: for x being Element of AS holds
( x in X iff LIN a,b,x )
let x be Element of AS; :: thesis: ( x in X iff LIN a,b,x )
thus ( x in X implies LIN a,b,x ) by A1; :: thesis: ( LIN a,b,x implies x in X )
assume LIN a,b,x ; :: thesis: x in X
then for y being Element of AS st y = x holds
LIN a,b,y ;
hence x in X by A1; :: thesis: verum