let FT be non empty RelStr ; :: thesis: for x being Element of FT
for A being Subset of FT holds
( x in A ^b iff U_FT x meets A )
let x be Element of FT; :: thesis: for A being Subset of FT holds
( x in A ^b iff U_FT x meets A )
let A be Subset of FT; :: thesis: ( x in A ^b iff U_FT x meets A )
thus ( x in A ^b implies U_FT x meets A ) :: thesis: ( U_FT x meets A implies x in A ^b )

proof

assume x in A ^b ; :: thesis: U_FT x meets A
then ex y being Element of FT st
( y = x & U_FT y meets A ) ;
hence U_FT x meets A ; :: thesis: verum

end;

assume U_FT x meets A ; :: thesis: x in A ^b
hence x in A ^b ; :: thesis: verum