let T be non empty TopSpace; :: thesis: for B being Basis of T

for V being Subset of T holds Int V = union { G where G is Subset of T : ( G in B & G c= V ) }

let B be Basis of T; :: thesis: for V being Subset of T holds Int V = union { G where G is Subset of T : ( G in B & G c= V ) }

let V be Subset of T; :: thesis: Int V = union { G where G is Subset of T : ( G in B & G c= V ) }

set X = { G where G is Subset of T : ( G in B & G c= V ) } ;

set Y = { G where G is Subset of T : ( G in B & G c= Int V ) } ;

{ G where G is Subset of T : ( G in B & G c= V ) } = { G where G is Subset of T : ( G in B & G c= Int V ) }

for V being Subset of T holds Int V = union { G where G is Subset of T : ( G in B & G c= V ) }

let B be Basis of T; :: thesis: for V being Subset of T holds Int V = union { G where G is Subset of T : ( G in B & G c= V ) }

let V be Subset of T; :: thesis: Int V = union { G where G is Subset of T : ( G in B & G c= V ) }

set X = { G where G is Subset of T : ( G in B & G c= V ) } ;

set Y = { G where G is Subset of T : ( G in B & G c= Int V ) } ;

{ G where G is Subset of T : ( G in B & G c= V ) } = { G where G is Subset of T : ( G in B & G c= Int V ) }

proof

hence
Int V = union { G where G is Subset of T : ( G in B & G c= V ) }
by Th9; :: thesis: verum
thus
{ G where G is Subset of T : ( G in B & G c= V ) } c= { G where G is Subset of T : ( G in B & G c= Int V ) }
:: according to XBOOLE_0:def 10 :: thesis: { G where G is Subset of T : ( G in B & G c= Int V ) } c= { G where G is Subset of T : ( G in B & G c= V ) }

assume e in { G where G is Subset of T : ( G in B & G c= Int V ) } ; :: thesis: e in { G where G is Subset of T : ( G in B & G c= V ) }

then consider G being Subset of T such that

A4: ( e = G & G in B ) and

A5: G c= Int V ;

Int V c= V by TOPS_1:16;

then G c= V by A5;

hence e in { G where G is Subset of T : ( G in B & G c= V ) } by A4; :: thesis: verum

end;proof

let e be object ; :: according to TARSKI:def 3 :: thesis: ( not e in { G where G is Subset of T : ( G in B & G c= Int V ) } or e in { G where G is Subset of T : ( G in B & G c= V ) } )
let e be object ; :: according to TARSKI:def 3 :: thesis: ( not e in { G where G is Subset of T : ( G in B & G c= V ) } or e in { G where G is Subset of T : ( G in B & G c= Int V ) } )

assume e in { G where G is Subset of T : ( G in B & G c= V ) } ; :: thesis: e in { G where G is Subset of T : ( G in B & G c= Int V ) }

then consider G being Subset of T such that

A1: e = G and

A2: G in B and

A3: G c= V ;

G c= Int V by A2, A3, Th10, TOPS_1:24;

hence e in { G where G is Subset of T : ( G in B & G c= Int V ) } by A1, A2; :: thesis: verum

end;assume e in { G where G is Subset of T : ( G in B & G c= V ) } ; :: thesis: e in { G where G is Subset of T : ( G in B & G c= Int V ) }

then consider G being Subset of T such that

A1: e = G and

A2: G in B and

A3: G c= V ;

G c= Int V by A2, A3, Th10, TOPS_1:24;

hence e in { G where G is Subset of T : ( G in B & G c= Int V ) } by A1, A2; :: thesis: verum

assume e in { G where G is Subset of T : ( G in B & G c= Int V ) } ; :: thesis: e in { G where G is Subset of T : ( G in B & G c= V ) }

then consider G being Subset of T such that

A4: ( e = G & G in B ) and

A5: G c= Int V ;

Int V c= V by TOPS_1:16;

then G c= V by A5;

hence e in { G where G is Subset of T : ( G in B & G c= V ) } by A4; :: thesis: verum