let FMT be non empty FMT_Space_Str ; :: thesis: for x being Element of
for A being Subset of holds
( x in A ^Foi iff ex V being Subset of st
( V in U_FMT x & V c= A ) )
let x be Element of ; :: thesis: for A being Subset of holds
( x in A ^Foi iff ex V being Subset of st
( V in U_FMT x & V c= A ) )
let A be Subset of ; :: thesis: ( x in A ^Foi iff ex V being Subset of st
( V in U_FMT x & V c= A ) )
thus ( x in A ^Foi implies ex V being Subset of st
( V in U_FMT x & V c= A ) ) :: thesis: ( ex V being Subset of st
( V in U_FMT x & V c= A ) implies x in A ^Foi )

proof

assume x in A ^Foi ; :: thesis: ex V being Subset of st
( V in U_FMT x & V c= A )
then ex y being Element of st
( y = x & ex V being Subset of st
( V in U_FMT y & V c= A ) ) ;
hence ex V being Subset of st
( V in U_FMT x & V c= A ) ; :: thesis: verum

end;

assume ex V being Subset of st
( V in U_FMT x & V c= A ) ; :: thesis: x in A ^Foi
hence x in A ^Foi ; :: thesis: verum