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 )
proof
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
proof
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;
A c= component x
proof
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;
hence A = component x by A3; :: thesis: verum
end;
( A = component x implies for y being object st [x,y] in EqCl the InternalRel of R holds
y in A )
proof
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;
hence ( A = component x iff for y being object holds
( y in A iff [x,y] in EqCl the InternalRel of R ) ) by A1, Th28; :: thesis: verum