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 by Th21;
( [b,b] `1 = b & [b,b] `2 = b ) by MCART_1:7;
then p ## [b,b] by A1, Def6;
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 Th41;
( [b,b] `1 = b & [b,b] `2 = b ) by MCART_1:7;
then p `1 ,p `2 @@ b,b by A2, Def6;
then p `1 = p `2 by Th22, Th23;
hence p in ID M ; :: thesis: verum

end;

end;

then for p being set holds
( p in ID M iff p in [b,b] ~ ) ;
hence ID M = [b,b] ~ by TARSKI:1; :: thesis: verum