let Y be TopStruct ; :: thesis: ( Y is anti-discrete implies Y is TopSpace-like )
assume Y is anti-discrete ; :: thesis: Y is TopSpace-like
then A4: the topology of Y = {{}, the carrier of Y} ;
A5: for A, B being Subset of Y st A in the topology of Y & B in the topology of Y holds
A /\ B in the topology of Y
proof
let A, B be Subset of Y; :: thesis: ( A in the topology of Y & B in the topology of Y implies A /\ B in the topology of Y )
assume that
A6: A in the topology of Y and
A7: B in the topology of Y ; :: thesis: A /\ B in the topology of Y
A8: ( B = {} or B = the carrier of Y ) by A4, A7, TARSKI:def 2;
( A = {} or A = the carrier of Y ) by A4, A6, TARSKI:def 2;
hence A /\ B in the topology of Y by A4, A8, TARSKI:def 2; :: thesis: verum
end;
A9: for F being Subset-Family of Y st F c= the topology of Y holds
union F in the topology of Y
proof
let F be Subset-Family of Y; :: thesis: ( F c= the topology of Y implies union F in the topology of Y )
assume F c= the topology of Y ; :: thesis: union F in the topology of Y
then ( F = {} or F = {{}} or F = { the carrier of Y} or F = {{}, the carrier of Y} ) by A4, ZFMISC_1:36;
then ( union F = {} or union F = the carrier of Y or union F = {} \/ the carrier of Y ) by ZFMISC_1:2, ZFMISC_1:25, ZFMISC_1:75;
hence union F in the topology of Y by A4, TARSKI:def 2; :: thesis: verum
end;
the carrier of Y in the topology of Y by A4, TARSKI:def 2;
hence Y is TopSpace-like by A9, A5, PRE_TOPC:def 1; :: thesis: verum