let S1, S2 be set ; :: thesis: ( ( for x being object holds

( x in S1 iff ex W being strict Subspace of V st

( W = x & dim W = n ) ) ) & ( for x being object holds

( x in S2 iff ex W being strict Subspace of V st

( W = x & dim W = n ) ) ) implies S1 = S2 )

assume that

A6: for x being object holds

( x in S1 iff ex W being strict Subspace of V st

( W = x & dim W = n ) ) and

A7: for x being object holds

( x in S2 iff ex W being strict Subspace of V st

( W = x & dim W = n ) ) ; :: thesis: S1 = S2

for x being object holds

( x in S1 iff x in S2 )

( x in S1 iff ex W being strict Subspace of V st

( W = x & dim W = n ) ) ) & ( for x being object holds

( x in S2 iff ex W being strict Subspace of V st

( W = x & dim W = n ) ) ) implies S1 = S2 )

assume that

A6: for x being object holds

( x in S1 iff ex W being strict Subspace of V st

( W = x & dim W = n ) ) and

A7: for x being object holds

( x in S2 iff ex W being strict Subspace of V st

( W = x & dim W = n ) ) ; :: thesis: S1 = S2

for x being object holds

( x in S1 iff x in S2 )

proof

hence
S1 = S2
by TARSKI:2; :: thesis: verum
let x be object ; :: thesis: ( x in S1 iff x in S2 )

then ex W being strict Subspace of V st

( W = x & dim W = n ) by A7;

hence x in S1 by A6; :: thesis: verum

end;hereby :: thesis: ( x in S2 implies x in S1 )

assume
x in S2
; :: thesis: x in S1assume
x in S1
; :: thesis: x in S2

then ex W being strict Subspace of V st

( W = x & dim W = n ) by A6;

hence x in S2 by A7; :: thesis: verum

end;then ex W being strict Subspace of V st

( W = x & dim W = n ) by A6;

hence x in S2 by A7; :: thesis: verum

then ex W being strict Subspace of V st

( W = x & dim W = n ) by A7;

hence x in S1 by A6; :: thesis: verum