let Y be non empty TopStruct ; :: thesis: for F being Subset-Family of Y st F is anti-discrete-set-family & meet F <> {} holds
union F is anti-discrete
let F be Subset-Family of Y; :: thesis: ( F is anti-discrete-set-family & meet F <> {} implies union F is anti-discrete )
assume A1: F is anti-discrete-set-family ; :: thesis: ( not meet F <> {} or union F is anti-discrete )
assume A2: meet F <> {} ; :: thesis: union F is anti-discrete
for G being Subset of Y holds
( not G is open or union F misses G or union F c= G )
proof
let G be Subset of Y; :: thesis: ( not G is open or union F misses G or union F c= G )
assume A3: G is open ; :: thesis: ( union F misses G or union F c= G )
assume union F meets G ; :: thesis: union F c= G
then consider A0 being set such that
A4: A0 in F and
A5: A0 meets G by ZFMISC_1:80;
reconsider A0 = A0 as Subset of Y by A4;
A0 is anti-discrete by A1, A4;
then A6: A0 c= G by A3, A5;
meet F c= A0 by A4, SETFAM_1:3;
then A7: meet F c= G by A6;
for B being set st B in F holds
B c= G
proof
let B be set ; :: thesis: ( B in F implies B c= G )
assume A8: B in F ; :: thesis: B c= G
then reconsider B0 = B as Subset of Y ;
meet F c= B0 by A8, SETFAM_1:3;
then B0 /\ G <> {} by A2, A7, XBOOLE_1:3, XBOOLE_1:19;
then A9: B0 meets G ;
B0 is anti-discrete by A1, A8;
hence B c= G by A3, A9; :: thesis: verum
end;
hence union F c= G by ZFMISC_1:76; :: thesis: verum
end;
hence union F is anti-discrete ; :: thesis: verum