let V be RealLinearSpace; :: 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

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, Th15;

hence x in A by A1, A3, Lm2; :: thesis: verum

( 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

set y = the Element of A;
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 Th15;

then x = 0. V by A1, Lm2;

hence x in {(0. V)} by TARSKI:def 1; :: thesis: verum

end;assume x in A ; :: thesis: x in {(0. V)}

then x in Lin A by Th15;

then x = 0. V by A1, Lm2;

hence x in {(0. V)} by TARSKI:def 1; :: thesis: verum

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, Th15;

hence x in A by A1, A3, Lm2; :: thesis: verum