let S, T be Subset of (Subspaces V); :: thesis: ( ( W1 is Subspace of W2 & ( for W being strict Subspace of V holds
( W in S iff ( W1 is Subspace of W & W is Subspace of W2 ) ) ) & ( for W being strict Subspace of V holds
( W in T iff ( W1 is Subspace of W & W is Subspace of W2 ) ) ) implies S = T ) & ( W1 is not Subspace of W2 & S = {} & T = {} implies S = T ) )

now :: thesis: ( W1 is Subspace of W2 & ( for W being strict Subspace of V holds
( W in S iff ( W1 is Subspace of W & W is Subspace of W2 ) ) ) & ( for W being strict Subspace of V holds
( W in T iff ( W1 is Subspace of W & W is Subspace of W2 ) ) ) implies S = T )

assume W1 is Subspace of W2 ; :: thesis: ( ( for W being strict Subspace of V holds
( W in S iff ( W1 is Subspace of W & W is Subspace of W2 ) ) ) & ( for W being strict Subspace of V holds
( W in T iff ( W1 is Subspace of W & W is Subspace of W2 ) ) ) implies S = T )
assume that
A3: for W being strict Subspace of V holds
( W in S iff ( W1 is Subspace of W & W is Subspace of W2 ) ) and
A4: for W being strict Subspace of V holds
( W in T iff ( W1 is Subspace of W & W is Subspace of W2 ) ) ; :: thesis: S = T

now :: thesis: for x being object holds
( ( x in S implies x in T ) & ( x in T implies x in S ) )

let x be object ; :: thesis: ( ( x in S implies x in T ) & ( x in T implies x in S ) )
thus ( x in S implies x in T ) :: thesis: ( x in T implies x in S )

proof

assume A5: x in S ; :: thesis: x in T
then consider x1 being strict Subspace of V such that
A6: x1 = x by VECTSP_5:def 3;
( x1 in S iff ( W1 is Subspace of x1 & x1 is Subspace of W2 ) ) by A3;
hence x in T by A4, A5, A6; :: thesis: verum

end;

assume A7: x in T ; :: thesis: x in S
then consider x1 being strict Subspace of V such that
A8: x1 = x by VECTSP_5:def 3;
( x1 in T iff ( W1 is Subspace of x1 & x1 is Subspace of W2 ) ) by A4;
hence x in S by A3, A7, A8; :: thesis: verum

end;

hence S = T by TARSKI:2; :: thesis: verum

end;

hence ( ( W1 is Subspace of W2 & ( for W being strict Subspace of V holds
( W in S iff ( W1 is Subspace of W & W is Subspace of W2 ) ) ) & ( for W being strict Subspace of V holds
( W in T iff ( W1 is Subspace of W & W is Subspace of W2 ) ) ) implies S = T ) & ( W1 is not Subspace of W2 & S = {} & T = {} implies S = T ) ) ; :: thesis: verum