defpred S1[ 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 S1[x,y] & S1[x,z] holds
y = z
proof
let x, y, z be object ; :: thesis: ( S1[x,y] & S1[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 S1[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 ;
hence y = z by ; :: 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 & S1[y,x] ) ) from 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 ;
then A12: { the carrier of R} c= FinSETS by ;
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 ; :: 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 ;
the InternalRel of R in FinSETS by ;
then [ the carrier of R, the InternalRel of R] in FinSETS by ;
hence x in X by ; :: 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