let GF be Ring; :: thesis: for V being LeftMod of GF
for A being Subset of V holds
( not Lin A = (0). V or A = {} or A = {(0. V)} )
let V be LeftMod of GF; :: thesis: for A being Subset of V holds
( not Lin A = (0). V or A = {} or A = {(0. V)} )
let A be Subset of V; :: thesis: ( not Lin A = (0). V or A = {} or A = {(0. V)} )
assume that
A1: Lin A = (0). V and
A2: A <> {} ; :: thesis: A = {(0. V)}
thus A c= {(0. V)} :: according to XBOOLE_0:def 10 :: thesis: {(0. V)} c= A
proof
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in A or x in {(0. V)} )
assume x in A ; :: thesis: x in {(0. V)}
then x in Lin A by Th8;
then x = 0. V by A1, VECTSP_4:35;
hence x in {(0. V)} by TARSKI:def 1; :: thesis: verum
end;
set y = the Element of A;
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in {(0. V)} or x in A )
assume x in {(0. V)} ; :: thesis: x in A
then A3: x = 0. V by TARSKI:def 1;
( the Element of A in A & the Element of A in Lin A ) by A2, Th8;
hence x in A by A1, A3, VECTSP_4:35; :: thesis: verum