let R be non empty RelStr ; :: thesis: (f_1 R) . {} = {}
{ u where u is Element of R : (UncertaintyMap R) . u meets {} R } c= {}

proof

let y be object ; :: according to TARSKI:def 3 :: thesis: ( not y in { u where u is Element of R : (UncertaintyMap R) . u meets {} R } or y in {} )
assume y in { u where u is Element of R : (UncertaintyMap R) . u meets {} R } ; :: thesis: y in {}
then consider u being Element of R such that
A1: ( u = y & (UncertaintyMap R) . u meets {} R ) ;
thus y in {} by A1; :: thesis: verum

end;

hence (f_1 R) . {} = {} by Defff; :: thesis: verum