let M be MidSp; :: thesis: for b being Element of M holds ID M = [b,b] ~
let b be Element of M; :: thesis: ID M = [b,b] ~
for p being Element of [: the carrier of M, the carrier of M:] holds
( p in ID M iff p in [b,b] ~ )
proof
let p be Element of [: the carrier of M, the carrier of M:]; :: thesis: ( p in ID M iff p in [b,b] ~ )
thus ( p in ID M implies p in [b,b] ~ ) :: thesis: ( p in [b,b] ~ implies p in ID M )
proof
assume p in ID M ; :: thesis: p in [b,b] ~
then ex q being Element of [: the carrier of M, the carrier of M:] st
( p = q & q `1 = q `2 ) ;
then A1: p `1 ,p `2 @@ b,b ;
p ## [b,b] by A1;
hence p in [b,b] ~ ; :: thesis: verum
end;
thus ( p in [b,b] ~ implies p in ID M ) :: thesis: verum
proof
assume p in [b,b] ~ ; :: thesis: p in ID M
then A2: p ## [b,b] by Th26;
p `1 ,p `2 @@ b,b by A2;
then p `1 = p `2 by Th11, Th12;
hence p in ID M ; :: thesis: verum
end;
end;
then for p being object holds
( p in ID M iff p in [b,b] ~ ) ;
hence ID M = [b,b] ~ by TARSKI:2; :: thesis: verum