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] ~ )

( p in ID M iff p in [b,b] ~ ) ;

hence ID M = [b,b] ~ by TARSKI:2; :: thesis: verum

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

then
for p being object holds
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 )

end;thus ( p in ID M implies p in [b,b] ~ ) :: thesis: ( p in [b,b] ~ implies p in ID M )

proof

thus
( p in [b,b] ~ implies p in ID M )
:: thesis: verum
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;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

( p in ID M iff p in [b,b] ~ ) ;

hence ID M = [b,b] ~ by TARSKI:2; :: thesis: verum