let X, Y be Equivalence_Relation of the carrier of R; :: thesis: ( ( for x, y being object holds
( [x,y] in X iff ( x in the carrier of R & y in the carrier of R & ex p being FinSequence of the carrier of R st
( 1 < len p & p . 1 = x & p . (len p) = y & ( for n being Nat st 2 <= n & n <= len p & not [(p . n),(p . (n - 1))] in the InternalRel of R holds
[(p . (n - 1)),(p . n)] in the InternalRel of R ) ) ) ) ) & ( for x, y being object holds
( [x,y] in Y iff ( x in the carrier of R & y in the carrier of R & ex p being FinSequence of the carrier of R st
( 1 < len p & p . 1 = x & p . (len p) = y & ( for n being Nat st 2 <= n & n <= len p & not [(p . n),(p . (n - 1))] in the InternalRel of R holds
[(p . (n - 1)),(p . n)] in the InternalRel of R ) ) ) ) ) implies X = Y )
defpred S1[ object , object ] means ( $1 in the carrier of R & $2 in the carrier of R & ex p being FinSequence of the carrier of R st
( 1 < len p & p . 1 = $1 & p . (len p) = $2 & ( for n being Nat st 2 <= n & n <= len p & not [(p . n),(p . (n - 1))] in the InternalRel of R holds
[(p . (n - 1)),(p . n)] in the InternalRel of R ) ) );
assume A51: for x, y being object holds
( [x,y] in X iff S1[x,y] ) ; :: thesis: ( ex x, y being object st
( ( [x,y] in Y implies ( x in the carrier of R & y in the carrier of R & ex p being FinSequence of the carrier of R st
( 1 < len p & p . 1 = x & p . (len p) = y & ( for n being Nat st 2 <= n & n <= len p & not [(p . n),(p . (n - 1))] in the InternalRel of R holds
[(p . (n - 1)),(p . n)] in the InternalRel of R ) ) ) ) implies ( x in the carrier of R & y in the carrier of R & ex p being FinSequence of the carrier of R st
( 1 < len p & p . 1 = x & p . (len p) = y & ( for n being Nat st 2 <= n & n <= len p & not [(p . n),(p . (n - 1))] in the InternalRel of R holds
[(p . (n - 1)),(p . n)] in the InternalRel of R ) ) & not [x,y] in Y ) ) or X = Y )
assume A52: for x, y being object holds
( [x,y] in Y iff S1[x,y] ) ; :: thesis: X = Y
for x, y being object holds
( [x,y] in X iff [x,y] in Y )
proof
let x, y be object ; :: thesis: ( [x,y] in X iff [x,y] in Y )
hereby :: thesis: ( [x,y] in Y implies [x,y] in X )
assume [x,y] in X ; :: thesis: [x,y] in Y
then S1[x,y] by A51;
hence [x,y] in Y by A52; :: thesis: verum
end;
assume [x,y] in Y ; :: thesis: [x,y] in X
then S1[x,y] by A52;
hence [x,y] in X by A51; :: thesis: verum
end;
hence X = Y by RELAT_1:def 2; :: thesis: verum