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 A1: the topology of Y = {{} ,the carrier of Y} by Def2;

now

thus the carrier of Y in the topology of Y by A1, TARSKI:def 2; :: thesis: ( ( for F being Subset-Family of Y st F c= the topology of Y holds
union F in the topology of Y ) & ( 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 ) )
thus for F being Subset-Family of Y st F c= the topology of Y holds
union F in the topology of Y :: thesis: 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 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 A1, ZFMISC_1:42;
then ( union F = {} or union F = the carrier of Y or union F = {} \/ the carrier of Y ) by ZFMISC_1:2, ZFMISC_1:31, ZFMISC_1:93;
hence union F in the topology of Y by A1, TARSKI:def 2; :: thesis: verum

end;

thus 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 :: thesis: verum

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 ( A in the topology of Y & B in the topology of Y ) ; :: thesis: A /\ B in the topology of Y
then ( ( A = {} or A = the carrier of Y ) & ( B = {} or B = the carrier of Y ) ) by A1, TARSKI:def 2;
hence A /\ B in the topology of Y by A1, TARSKI:def 2; :: thesis: verum

end;

end;

hence Y is TopSpace-like by PRE_TOPC:def 1; :: thesis: verum