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

proof

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

end;

assume ( U_FT x meets A & U_FT x meets A ` ) ; :: thesis: x in A ^delta
hence x in A ^delta ; :: thesis: verum