hereby :: according to TOPS_5:def 1 :: thesis: J * f is non-Empty

for S being 1-sorted st S in rng (J * f) holds let y be object ; :: thesis: ( y in rng (J * f) implies y is TopSpace )

assume y in rng (J * f) ; :: thesis: y is TopSpace

then y in rng J by RELAT_1:26, TARSKI:def 3;

hence y is TopSpace by Def1; :: thesis: verum

end;assume y in rng (J * f) ; :: thesis: y is TopSpace

then y in rng J by RELAT_1:26, TARSKI:def 3;

hence y is TopSpace by Def1; :: thesis: verum

not S is empty

proof

hence
J * f is non-Empty
by WAYBEL_3:def 7; :: thesis: verum
let S be 1-sorted ; :: thesis: ( S in rng (J * f) implies not S is empty )

assume S in rng (J * f) ; :: thesis: not S is empty

then S in rng J by RELAT_1:26, TARSKI:def 3;

hence not S is empty by WAYBEL_3:def 7; :: thesis: verum

end;assume S in rng (J * f) ; :: thesis: not S is empty

then S in rng J by RELAT_1:26, TARSKI:def 3;

hence not S is empty by WAYBEL_3:def 7; :: thesis: verum