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

proof

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

end;

assume U_FT x c= A ; :: thesis: x in A ^i
hence x in A ^i ; :: thesis: verum