set F = { A where A is Subset of V : A is linearly-independent } ;

set X = the carrier of V;

{ A where A is Subset of V : A is linearly-independent } c= bool the carrier of V

take TopStruct(# the carrier of V,F #) ; :: thesis: ( the carrier of TopStruct(# the carrier of V,F #) = the carrier of V & the_family_of TopStruct(# the carrier of V,F #) = { A where A is Subset of V : A is linearly-independent } )

thus ( the carrier of TopStruct(# the carrier of V,F #) = the carrier of V & the_family_of TopStruct(# the carrier of V,F #) = { A where A is Subset of V : A is linearly-independent } ) ; :: thesis: verum

set X = the carrier of V;

{ A where A is Subset of V : A is linearly-independent } c= bool the carrier of V

proof

then reconsider F = { A where A is Subset of V : A is linearly-independent } as Subset-Family of the carrier of V ;
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in { A where A is Subset of V : A is linearly-independent } or x in bool the carrier of V )

assume x in { A where A is Subset of V : A is linearly-independent } ; :: thesis: x in bool the carrier of V

then ex A being Subset of the carrier of V st

( x = A & A is linearly-independent ) ;

hence x in bool the carrier of V ; :: thesis: verum

end;assume x in { A where A is Subset of V : A is linearly-independent } ; :: thesis: x in bool the carrier of V

then ex A being Subset of the carrier of V st

( x = A & A is linearly-independent ) ;

hence x in bool the carrier of V ; :: thesis: verum

take TopStruct(# the carrier of V,F #) ; :: thesis: ( the carrier of TopStruct(# the carrier of V,F #) = the carrier of V & the_family_of TopStruct(# the carrier of V,F #) = { A where A is Subset of V : A is linearly-independent } )

thus ( the carrier of TopStruct(# the carrier of V,F #) = the carrier of V & the_family_of TopStruct(# the carrier of V,F #) = { A where A is Subset of V : A is linearly-independent } ) ; :: thesis: verum