let L be non empty right_complementable add-associative right_zeroed left-distributive left_unital doubleLoopStr ; :: thesis: for I being LeftIdeal of L
for x, y being Element of L st x in I & y in I holds
x - y in I
let I be LeftIdeal of L; :: thesis: for x, y being Element of L st x in I & y in I holds
x - y in I
let x, y be Element of L; :: thesis: ( x in I & y in I implies x - y in I )
assume that
A1: x in I and
A2: y in I ; :: thesis: x - y in I
- y in I by A2, Th13;
hence x - y in I by A1, Def1; :: thesis: verum