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

( x in D1 iff x is strict Subspace of V ) ) & ( for x being object holds

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

assume A10: for x being object holds

( x in D1 iff x is strict Subspace of V ) ; :: thesis: ( ex x being object st

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

assume A11: for x being object holds

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

( x in D1 iff x is strict Subspace of V ) ) & ( for x being object holds

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

assume A10: for x being object holds

( x in D1 iff x is strict Subspace of V ) ; :: thesis: ( ex x being object st

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

assume A11: for x being object holds

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

now :: thesis: for x being object holds

( ( x in D1 implies x in D2 ) & ( x in D2 implies x in D1 ) )

hence
D1 = D2
by TARSKI:2; :: thesis: verum( ( x in D1 implies x in D2 ) & ( x in D2 implies x in D1 ) )

let x be object ; :: thesis: ( ( x in D1 implies x in D2 ) & ( x in D2 implies x in D1 ) )

thus ( x in D1 implies x in D2 ) :: thesis: ( x in D2 implies x in D1 )

then x is strict Subspace of V by A11;

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

end;thus ( x in D1 implies x in D2 ) :: thesis: ( x in D2 implies x in D1 )

proof

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

then x is strict Subspace of V by A10;

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

end;then x is strict Subspace of V by A10;

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

then x is strict Subspace of V by A11;

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