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