let S, T be Subset-Family of (m Subspaces_of V); :: thesis: ( ( for X being set holds
( X in S iff ex W being Subspace of V st
( dim W = n & X = m Subspaces_of W ) ) ) & ( for X being set holds
( X in T iff ex W being Subspace of V st
( dim W = n & X = m Subspaces_of W ) ) ) implies S = T )
assume that
A4: for X being set holds
( X in S iff ex W being Subspace of V st
( dim W = n & X = m Subspaces_of W ) ) and
A5: for X being set holds
( X in T iff ex W being Subspace of V st
( dim W = n & X = m Subspaces_of W ) ) ; :: 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 X in S ; :: thesis: X in T
then ex W being Subspace of V st
( dim W = n & X = m Subspaces_of W ) by A4;
hence X in T by A5; :: thesis: verum

end;

assume X in T ; :: thesis: X in S
then ex W being Subspace of V st
( dim W = n & X = m Subspaces_of W ) by A5;
hence X in S by A4; :: thesis: verum

end;

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