let R be RelStr ; :: thesis: for x being Element of R

for A being set holds

( A = component x iff for y being object holds

( y in A iff [x,y] in EqCl the InternalRel of R ) )

let x be Element of R; :: thesis: for A being set holds

( A = component x iff for y being object holds

( y in A iff [x,y] in EqCl the InternalRel of R ) )

let A be set ; :: thesis: ( A = component x iff for y being object holds

( y in A iff [x,y] in EqCl the InternalRel of R ) )

set IR = the InternalRel of R;

A1: ( ( for y being object holds

( y in A iff [x,y] in EqCl the InternalRel of R ) ) implies A = component x )

y in A )

( y in A iff [x,y] in EqCl the InternalRel of R ) ) by A1, Th28; :: thesis: verum

for A being set holds

( A = component x iff for y being object holds

( y in A iff [x,y] in EqCl the InternalRel of R ) )

let x be Element of R; :: thesis: for A being set holds

( A = component x iff for y being object holds

( y in A iff [x,y] in EqCl the InternalRel of R ) )

let A be set ; :: thesis: ( A = component x iff for y being object holds

( y in A iff [x,y] in EqCl the InternalRel of R ) )

set IR = the InternalRel of R;

A1: ( ( for y being object holds

( y in A iff [x,y] in EqCl the InternalRel of R ) ) implies A = component x )

proof

( A = component x implies for y being object st [x,y] in EqCl the InternalRel of R holds
assume A2:
for y being object holds

( y in A iff [x,y] in EqCl the InternalRel of R ) ; :: thesis: A = component x

A3: component x c= A

end;( y in A iff [x,y] in EqCl the InternalRel of R ) ; :: thesis: A = component x

A3: component x c= A

proof

A c= component x
let a be object ; :: according to TARSKI:def 3 :: thesis: ( not a in component x or a in A )

assume a in component x ; :: thesis: a in A

then [a,x] in EqCl the InternalRel of R by EQREL_1:19;

then [x,a] in EqCl the InternalRel of R by EQREL_1:6;

hence a in A by A2; :: thesis: verum

end;assume a in component x ; :: thesis: a in A

then [a,x] in EqCl the InternalRel of R by EQREL_1:19;

then [x,a] in EqCl the InternalRel of R by EQREL_1:6;

hence a in A by A2; :: thesis: verum

proof

hence
A = component x
by A3; :: thesis: verum
let a be object ; :: according to TARSKI:def 3 :: thesis: ( not a in A or a in component x )

assume a in A ; :: thesis: a in component x

then [x,a] in EqCl the InternalRel of R by A2;

then [a,x] in EqCl the InternalRel of R by EQREL_1:6;

hence a in component x by EQREL_1:19; :: thesis: verum

end;assume a in A ; :: thesis: a in component x

then [x,a] in EqCl the InternalRel of R by A2;

then [a,x] in EqCl the InternalRel of R by EQREL_1:6;

hence a in component x by EQREL_1:19; :: thesis: verum

y in A )

proof

hence
( A = component x iff for y being object holds
assume A4:
A = component x
; :: thesis: for y being object st [x,y] in EqCl the InternalRel of R holds

y in A

let y be object ; :: thesis: ( [x,y] in EqCl the InternalRel of R implies y in A )

assume [x,y] in EqCl the InternalRel of R ; :: thesis: y in A

then [y,x] in EqCl the InternalRel of R by EQREL_1:6;

hence y in A by A4, EQREL_1:19; :: thesis: verum

end;y in A

let y be object ; :: thesis: ( [x,y] in EqCl the InternalRel of R implies y in A )

assume [x,y] in EqCl the InternalRel of R ; :: thesis: y in A

then [y,x] in EqCl the InternalRel of R by EQREL_1:6;

hence y in A by A4, EQREL_1:19; :: thesis: verum

( y in A iff [x,y] in EqCl the InternalRel of R ) ) by A1, Th28; :: thesis: verum