set SAC = the Sorts of A -carrier_of (CComp s1);
set CS = Class (CompClass E,(CComp s1));
defpred S₁[ set ] means ex x being set st
( x in the Sorts of A . s1 & $1 = Class (CompClass E,(CComp s1)),x );

per cases ( Class (CompClass E,(CComp s1)) is empty or not Class (CompClass E,(CComp s1)) is empty ) ;

suppose A1: Class (CompClass E,(CComp s1)) is empty ; :: thesis: ex b₁ being Subset of (Class (CompClass E,(CComp s1))) st
for z being set holds
( z in b₁ iff ex x being set st
( x in the Sorts of A . s1 & z = Class (CompClass E,(CComp s1)),x ) )

reconsider CS1 = {} as Subset of (Class (CompClass E,(CComp s1))) by XBOOLE_1:2;
take CS1 ; :: thesis: for z being set holds
( z in CS1 iff ex x being set st
( x in the Sorts of A . s1 & z = Class (CompClass E,(CComp s1)),x ) )
let z be set ; :: thesis: ( z in CS1 iff ex x being set st
( x in the Sorts of A . s1 & z = Class (CompClass E,(CComp s1)),x ) )
thus ( z in CS1 implies S₁[z] ) ; :: thesis: ( ex x being set st
( x in the Sorts of A . s1 & z = Class (CompClass E,(CComp s1)),x ) implies z in CS1 )
assume S₁[z] ; :: thesis: z in CS1
then consider x being set such that
A2: x in the Sorts of A . s1 and
z = Class (CompClass E,(CComp s1)),x ;
x in the Sorts of A -carrier_of (CComp s1) by A2, Th6;
hence z in CS1 by A1; :: thesis: verum

end;

suppose not Class (CompClass E,(CComp s1)) is empty ; :: thesis: ex b₁ being Subset of (Class (CompClass E,(CComp s1))) st
for z being set holds
( z in b₁ iff ex x being set st
( x in the Sorts of A . s1 & z = Class (CompClass E,(CComp s1)),x ) )

then reconsider CS1 = Class (CompClass E,(CComp s1)) as non empty Subset-Family of (the Sorts of A -carrier_of (CComp s1)) ;
set CC = { x where x is Element of CS1 : S₁[x] } ;

now

let x be set ; :: thesis: ( x in { x where x is Element of CS1 : S₁[x] } implies x in CS1 )
assume x in { x where x is Element of CS1 : S₁[x] } ; :: thesis: x in CS1
then ex y being Element of CS1 st
( x = y & S₁[y] ) ;
hence x in CS1 ; :: thesis: verum

end;

then reconsider CC2 = { x where x is Element of CS1 : S₁[x] } as Subset of (Class (CompClass E,(CComp s1))) by TARSKI:def 3;
take CC2 ; :: thesis: for z being set holds
( z in CC2 iff ex x being set st
( x in the Sorts of A . s1 & z = Class (CompClass E,(CComp s1)),x ) )
for x being set holds
( x in { x where x is Element of CS1 : S₁[x] } iff S₁[x] )

proof

let x be set ; :: thesis: ( x in { x where x is Element of CS1 : S₁[x] } iff S₁[x] )

hereby :: thesis: ( S₁[x] implies x in { x where x is Element of CS1 : S₁[x] } )

assume x in { x where x is Element of CS1 : S₁[x] } ; :: thesis: S₁[x]
then ex x1 being Element of CS1 st
( x = x1 & S₁[x1] ) ;
hence S₁[x] ; :: thesis: verum

end;

assume A3: S₁[x] ; :: thesis: x in { x where x is Element of CS1 : S₁[x] }
then consider y being set such that
A4: y in the Sorts of A . s1 and
A5: x = Class (CompClass E,(CComp s1)),y ;
s1 in CComp s1 by EQREL_1:28;
then the Sorts of A . s1 in { (the Sorts of A . s) where s is Element of S : s in CComp s1 } ;
then y in union { (the Sorts of A . s) where s is Element of S : s in CComp s1 } by A4, TARSKI:def 4;
then x in Class (CompClass E,(CComp s1)) by A5, EQREL_1:def 5;
hence x in { x where x is Element of CS1 : S₁[x] } by A3; :: thesis: verum

end;

hence for z being set holds
( z in CC2 iff ex x being set st
( x in the Sorts of A . s1 & z = Class (CompClass E,(CComp s1)),x ) ) ; :: thesis: verum

end;

end;