let X be set ; :: thesis: for x being Element of (bspace X) holds (1_ Z_2 ) * x = x
let x be Element of (bspace X); :: thesis: (1_ Z_2 ) * x = x
reconsider c = x as Subset of X ;
(1_ Z_2 ) * x = (1_ Z_2 ) \*\ c by Def6
.= c by Def4 ;
hence (1_ Z_2 ) * x = x ; :: thesis: verum