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, Th5;
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 :: thesis: for x being object st x in { x where x is Element of CS1 : S₁[x] } holds
x in CS1

let x be object ; :: 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:20;
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 3;
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;