let L be non empty right_complementable add-associative right_zeroed left-distributive left_unital doubleLoopStr ; :: thesis: for I being non empty left-ideal Subset of L
for x being Element of L st x in I holds
- x in I
let I be non empty left-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: (- (1. L)) * x in I by Def2;
0. L = (0. L) * x
.= ((1. L) + (- (1. L))) * x by RLVECT_1:def 10
.= ((1. L) * x) + ((- (1. L)) * x) by VECTSP_1:def 3
.= x + ((- (1. L)) * x) ;
hence - x in I by A1, RLVECT_1:def 10; :: thesis: verum