let S be 1 -element 1-sorted ; :: thesis: for s being Point of S
for F being Subset-Family of S st F is Cover of S holds
{s} in F
let s be Point of S; :: thesis: for F being Subset-Family of S st F is Cover of S holds
{s} in F
let F be Subset-Family of S; :: thesis: ( F is Cover of S implies {s} in F )
assume A1: the carrier of S c= union F ; :: according to SETFAM_1:def 11 :: thesis: {s} in F
consider d being Element of S such that
A2: the carrier of S = {d} by TEX_1:def 1;
s in the carrier of S ;
then consider Z being set such that
A3: s in Z and
A4: Z in F by A1, TARSKI:def 4;
A5: s = d by ZFMISC_1:def 10;
Z = {s}
proof
thus for x being object st x in Z holds
x in {s} by A4, A2, A5; :: according to TARSKI:def 3,XBOOLE_0:def 10 :: thesis: {s} c= Z
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in {s} or x in Z )
thus ( not x in {s} or x in Z ) by A3, TARSKI:def 1; :: thesis: verum
end;
hence {s} in F by A4; :: thesis: verum