let S, T be Subset-Family of (k Subspaces_of V); :: thesis: ( ( for X being set holds
( X in S iff ex W1, W2 being Subspace of V st
( W1 is Subspace of W2 & (dim W1) + 1 = k & dim W2 = k + 1 & X = pencil W1,W2,k ) ) ) & ( for X being set holds
( X in T iff ex W1, W2 being Subspace of V st
( W1 is Subspace of W2 & (dim W1) + 1 = k & dim W2 = k + 1 & X = pencil W1,W2,k ) ) ) implies S = T )
assume that
A3: for X being set holds
( X in S iff ex W1, W2 being Subspace of V st
( W1 is Subspace of W2 & (dim W1) + 1 = k & dim W2 = k + 1 & X = pencil W1,W2,k ) ) and
A4: for X being set holds
( X in T iff ex W1, W2 being Subspace of V st
( W1 is Subspace of W2 & (dim W1) + 1 = k & dim W2 = k + 1 & X = pencil W1,W2,k ) ) ; :: thesis: S = T

now

let x be set ; :: 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 W1, W2 being Subspace of V st
( W1 is Subspace of W2 & (dim W1) + 1 = k & dim W2 = k + 1 & x = pencil W1,W2,k ) by A3;
hence x in T by A4; :: thesis: verum

end;

assume x in T ; :: thesis: x in S
then ex W1, W2 being Subspace of V st
( W1 is Subspace of W2 & (dim W1) + 1 = k & dim W2 = k + 1 & x = pencil W1,W2,k ) by A4;
hence x in S by A3; :: thesis: verum

end;

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