theorem Th11: :: ALGSTR_2:11

for L being non empty doubleLoopStr holds
( L is _Skew-Field iff ( ( for a being Element of L holds a + (0. L) = a ) & ( for a being Element of L ex x being Element of L st a + x = 0. L ) & ( for a, b, c being Element of L holds (a + b) + c = a + (b + c) ) & ( for a, b being Element of L holds a + b = b + a ) & 0. L <> 1. L & ( for a being Element of L holds a * (1. L) = a ) & ( for a being Element of L st a <> 0. L holds
ex x being Element of L st a * x = 1. L ) & ( for a being Element of L holds a * (0. L) = 0. L ) & ( for a being Element of L holds (0. L) * a = 0. L ) & ( for a, b, c being Element of L holds (a * b) * c = a * (b * c) ) & ( for a, b, c being Element of L holds a * (b + c) = (a * b) + (a * c) ) & ( for a, b, c being Element of L holds (b + c) * a = (b * a) + (c * a) ) ) )