hereby :: thesis: ( W1 is not Subspace of W2 implies ex b₁ being Subset of (Subspaces V) st b₁ = {} )

defpred S₁[ set ] means for W being Subspace of V st W = $1 holds
( W1 is Subspace of W & W is Subspace of W2 );
set A = Subspaces V;
assume W1 is Subspace of W2 ; :: thesis: ex X being Subset of (Subspaces V) st
for W being strict Subspace of V holds
( ( W in X implies ( W1 is Subspace of W & W is Subspace of W2 ) ) & ( W1 is Subspace of W & W is Subspace of W2 implies W in X ) )
consider X being Subset of (Subspaces V) such that
A1: for x being set holds
( x in X iff ( x in Subspaces V & S₁[x] ) ) from SUBSET_1:sch 1();
take X = X; :: thesis: for W being strict Subspace of V holds
( ( W in X implies ( W1 is Subspace of W & W is Subspace of W2 ) ) & ( W1 is Subspace of W & W is Subspace of W2 implies W in X ) )
let W be strict Subspace of V; :: thesis: ( ( W in X implies ( W1 is Subspace of W & W is Subspace of W2 ) ) & ( W1 is Subspace of W & W is Subspace of W2 implies W in X ) )
thus ( W in X implies ( W1 is Subspace of W & W is Subspace of W2 ) ) by A1; :: thesis: ( W1 is Subspace of W & W is Subspace of W2 implies W in X )
assume ( W1 is Subspace of W & W is Subspace of W2 ) ; :: thesis: W in X
then A2: S₁[W] ;
W in Subspaces V by VECTSP_5:def 3;
hence W in X by A1, A2; :: thesis: verum

end;

hereby :: thesis: verum

reconsider W = {} as Subset of (Subspaces V) by XBOOLE_1:2;
assume W1 is not Subspace of W2 ; :: thesis: ex W being Subset of (Subspaces V) st W = {}
take W = W; :: thesis: W = {}
thus W = {} ; :: thesis: verum

end;