let L be non empty right_complementable add-associative right_zeroed right-distributive right_unital doubleLoopStr ; :: thesis: for I being non empty right-ideal Subset of L
for x being Element of L st x in I holds
- x in I
let I be non empty right-ideal Subset of L; :: thesis: for x being Element of L st x in I holds
- x in I
let x be Element of L; :: thesis: ( x in I implies - x in I )
assume x in I ; :: thesis: - x in I
then A1: x * (- (1. L)) in I by Def3;
0. L = x * (0. L)
.= x * ((1. L) + (- (1. L))) by RLVECT_1:def 10
.= (x * (1. L)) + (x * (- (1. L))) by VECTSP_1:def 2
.= x + (x * (- (1. L))) ;
hence - x in I by A1, RLVECT_1:def 10; :: thesis: verum