let V be RealUnitarySpace; :: 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 Th2;
then x = 0. V by A1, Lm1;
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, Th2;
hence x in A by A1, A3, Lm1; :: thesis: verum