defpred S₁[ object , object ] means ex R being strict RelStr st
( $1 = [ the carrier of R, the InternalRel of R] & $2 = R );
A1: for x, y, z being object st S₁[x,y] & S₁[x,z] holds
y = z

proof

let x, y, z be object ; :: thesis: ( S₁[x,y] & S₁[x,z] implies y = z )
given R1 being strict RelStr such that A2: x = [ the carrier of R1, the InternalRel of R1] and
A3: y = R1 ; :: thesis: ( not S₁[x,z] or y = z )
given R2 being strict RelStr such that A4: x = [ the carrier of R2, the InternalRel of R2] and
A5: z = R2 ; :: thesis: y = z
the carrier of R1 = the carrier of R2 by A2, A4, XTUPLE_0:1;
hence y = z by A2, A3, A4, A5, XTUPLE_0:1; :: thesis: verum

end;

consider X being set such that
A6: for x being object holds
( x in X iff ex y being object st
( y in FinSETS & S₁[y,x] ) ) from TARSKI:sch 1(A1);
take X ; :: thesis: for X being object holds
( X in X iff ex R being strict RelStr st
( X = R & the carrier of R in FinSETS ) )
for x being object holds
( x in X iff ex R being strict RelStr st
( x = R & the carrier of R in FinSETS ) )

proof

let x be object ; :: thesis: ( x in X iff ex R being strict RelStr st
( x = R & the carrier of R in FinSETS ) )
thus ( x in X implies ex R being strict RelStr st
( x = R & the carrier of R in FinSETS ) ) :: thesis: ( ex R being strict RelStr st
( x = R & the carrier of R in FinSETS ) implies x in X )

proof

assume x in X ; :: thesis: ex R being strict RelStr st
( x = R & the carrier of R in FinSETS )
then consider y being object such that
A7: y in FinSETS and
A8: ex R being strict RelStr st
( y = [ the carrier of R, the InternalRel of R] & x = R ) by A6;
consider R being strict RelStr such that
A9: y = [ the carrier of R, the InternalRel of R] and
A10: x = R by A8;
A11: { the carrier of R} in {{ the carrier of R, the InternalRel of R},{ the carrier of R}} by TARSKI:def 2;
{{ the carrier of R, the InternalRel of R},{ the carrier of R}} c= FinSETS by A7, A9, ORDINAL1:def 2;
then A12: { the carrier of R} c= FinSETS by A11, ORDINAL1:def 2;
the carrier of R in { the carrier of R} by TARSKI:def 1;
hence ex R being strict RelStr st
( x = R & the carrier of R in FinSETS ) by A10, A12; :: thesis: verum

end;

given R being strict RelStr such that A13: x = R and
A14: the carrier of R in FinSETS ; :: thesis: x in X
consider R being strict RelStr such that
A15: x = R and
A16: the carrier of R in FinSETS by A13, A14;
the InternalRel of R in FinSETS by A16, Th1;
then [ the carrier of R, the InternalRel of R] in FinSETS by A16, CLASSES2:58;
hence x in X by A6, A15; :: thesis: verum

end;

hence for X being object holds
( X in X iff ex R being strict RelStr st
( X = R & the carrier of R in FinSETS ) ) ; :: thesis: verum