defpred S_{1}[ 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_{1}[x,y] & S_{1}[x,z] holds

y = z

A6: for x being object holds

( x in X iff ex y being object st

( y in FinSETS & S_{1}[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 ) )

( X in X iff ex R being strict RelStr st

( X = R & the carrier of R in FinSETS ) ) ; :: thesis: verum

( $1 = [ the carrier of R, the InternalRel of R] & $2 = R );

A1: for x, y, z being object st S

y = z

proof

consider X being set such that
let x, y, z be object ; :: thesis: ( S_{1}[x,y] & S_{1}[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_{1}[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;given R1 being strict RelStr such that A2: x = [ the carrier of R1, the InternalRel of R1] and

A3: y = R1 ; :: thesis: ( not S

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

A6: for x being object holds

( x in X iff ex y being object st

( y in FinSETS & S

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

hence
for X being object holds
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 )

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;( 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

given R being strict RelStr such that A13:
x = R
and
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;( 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

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

( X in X iff ex R being strict RelStr st

( X = R & the carrier of R in FinSETS ) ) ; :: thesis: verum