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 :: 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 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