let D1, D2 be set ; :: thesis: ( ( for x being object holds
( x in D1 iff ex W being strict Subspace of M st W = x ) ) & ( for x being object holds
( x in D2 iff ex W being strict Subspace of M st W = x ) ) implies D1 = D2 )
assume A11: for x being object holds
( x in D1 iff ex W being strict Subspace of M st x = W ) ; :: thesis: ( ex x being object st
( ( x in D2 implies ex W being strict Subspace of M st W = x ) implies ( ex W being strict Subspace of M st W = x & not x in D2 ) ) or D1 = D2 )
assume A12: for x being object holds
( x in D2 iff ex W being strict Subspace of M st x = W ) ; :: thesis: D1 = D2

now :: thesis: for x being object holds
( ( 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 )

proof

assume x in D1 ; :: thesis: x in D2
then ex W being strict Subspace of M st x = W by A11;
hence x in D2 by A12; :: thesis: verum

end;

assume x in D2 ; :: thesis: x in D1
then ex W being strict Subspace of M st x = W by A12;
hence x in D1 by A11; :: thesis: verum

end;

hence D1 = D2 by TARSKI:2; :: thesis: verum