let D1, D2 be set ; :: thesis: ( ( for x being set holds

( x in D1 iff x is Linear_Combination of V ) ) & ( for x being set holds

( x in D2 iff x is Linear_Combination of V ) ) implies D1 = D2 )

assume A2: for x being set holds

( x in D1 iff x is Linear_Combination of V ) ; :: thesis: ( ex x being set st

( ( x in D2 implies x is Linear_Combination of V ) implies ( x is Linear_Combination of V & not x in D2 ) ) or D1 = D2 )

assume A3: for x being set holds

( x in D2 iff x is Linear_Combination of V ) ; :: thesis: D1 = D2

thus D1 c= D2 :: according to XBOOLE_0:def 10 :: thesis: D2 c= D1

assume x in D2 ; :: thesis: x in D1

then x is Linear_Combination of V by A3;

hence x in D1 by A2; :: thesis: verum

( x in D1 iff x is Linear_Combination of V ) ) & ( for x being set holds

( x in D2 iff x is Linear_Combination of V ) ) implies D1 = D2 )

assume A2: for x being set holds

( x in D1 iff x is Linear_Combination of V ) ; :: thesis: ( ex x being set st

( ( x in D2 implies x is Linear_Combination of V ) implies ( x is Linear_Combination of V & not x in D2 ) ) or D1 = D2 )

assume A3: for x being set holds

( x in D2 iff x is Linear_Combination of V ) ; :: thesis: D1 = D2

thus D1 c= D2 :: according to XBOOLE_0:def 10 :: thesis: D2 c= D1

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in D2 or x in D1 )
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in D1 or x in D2 )

assume x in D1 ; :: thesis: x in D2

then x is Linear_Combination of V by A2;

hence x in D2 by A3; :: thesis: verum

end;assume x in D1 ; :: thesis: x in D2

then x is Linear_Combination of V by A2;

hence x in D2 by A3; :: thesis: verum

assume x in D2 ; :: thesis: x in D1

then x is Linear_Combination of V by A3;

hence x in D1 by A2; :: thesis: verum