defpred S_{1}[ 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_{1}[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

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

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