let FT be non empty RelStr ; :: thesis: for x being Element of FT

for A being Subset of FT holds

( x in A ^i iff U_FT x c= A )

let x be Element of FT; :: thesis: for A being Subset of FT holds

( x in A ^i iff U_FT x c= A )

let A be Subset of FT; :: 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 )

hence x in A ^i ; :: thesis: verum

for A being Subset of FT holds

( x in A ^i iff U_FT x c= A )

let x be Element of FT; :: thesis: for A being Subset of FT holds

( x in A ^i iff U_FT x c= A )

let A be Subset of FT; :: 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
U_FT x c= A
; :: thesis: x in A ^i
assume
x in A ^i
; :: thesis: U_FT x c= A

then ex y being Element of FT st

( y = x & U_FT y c= A ) ;

hence U_FT x c= A ; :: thesis: verum

end;then ex y being Element of FT st

( y = x & U_FT y c= A ) ;

hence U_FT x c= A ; :: thesis: verum

hence x in A ^i ; :: thesis: verum