let R be non empty RelStr ; :: thesis: (f_0 R) . {} = {}

{ u where u is Element of R : (tau R) . u meets {} R } c= {}

{ u where u is Element of R : (tau R) . u meets {} R } c= {}

proof

hence
(f_0 R) . {} = {}
by Defff; :: thesis: verum
let y be object ; :: according to TARSKI:def 3 :: thesis: ( not y in { u where u is Element of R : (tau R) . u meets {} R } or y in {} )

assume y in { u where u is Element of R : (tau R) . u meets {} R } ; :: thesis: y in {}

then consider u being Element of R such that

A1: ( u = y & (tau R) . u meets {} R ) ;

thus y in {} by A1; :: thesis: verum

end;assume y in { u where u is Element of R : (tau R) . u meets {} R } ; :: thesis: y in {}

then consider u being Element of R such that

A1: ( u = y & (tau R) . u meets {} R ) ;

thus y in {} by A1; :: thesis: verum