let Y0, Y1 be TopStruct ; :: thesis: for D0 being Subset of Y0

for D1 being Subset of Y1 st TopStruct(# the carrier of Y0, the topology of Y0 #) = TopStruct(# the carrier of Y1, the topology of Y1 #) & D0 = D1 & D0 is anti-discrete holds

D1 is anti-discrete

let D0 be Subset of Y0; :: thesis: for D1 being Subset of Y1 st TopStruct(# the carrier of Y0, the topology of Y0 #) = TopStruct(# the carrier of Y1, the topology of Y1 #) & D0 = D1 & D0 is anti-discrete holds

D1 is anti-discrete

let D1 be Subset of Y1; :: thesis: ( TopStruct(# the carrier of Y0, the topology of Y0 #) = TopStruct(# the carrier of Y1, the topology of Y1 #) & D0 = D1 & D0 is anti-discrete implies D1 is anti-discrete )

assume A1: TopStruct(# the carrier of Y0, the topology of Y0 #) = TopStruct(# the carrier of Y1, the topology of Y1 #) ; :: thesis: ( not D0 = D1 or not D0 is anti-discrete or D1 is anti-discrete )

assume A2: D0 = D1 ; :: thesis: ( not D0 is anti-discrete or D1 is anti-discrete )

assume A3: D0 is anti-discrete ; :: thesis: D1 is anti-discrete

for D1 being Subset of Y1 st TopStruct(# the carrier of Y0, the topology of Y0 #) = TopStruct(# the carrier of Y1, the topology of Y1 #) & D0 = D1 & D0 is anti-discrete holds

D1 is anti-discrete

let D0 be Subset of Y0; :: thesis: for D1 being Subset of Y1 st TopStruct(# the carrier of Y0, the topology of Y0 #) = TopStruct(# the carrier of Y1, the topology of Y1 #) & D0 = D1 & D0 is anti-discrete holds

D1 is anti-discrete

let D1 be Subset of Y1; :: thesis: ( TopStruct(# the carrier of Y0, the topology of Y0 #) = TopStruct(# the carrier of Y1, the topology of Y1 #) & D0 = D1 & D0 is anti-discrete implies D1 is anti-discrete )

assume A1: TopStruct(# the carrier of Y0, the topology of Y0 #) = TopStruct(# the carrier of Y1, the topology of Y1 #) ; :: thesis: ( not D0 = D1 or not D0 is anti-discrete or D1 is anti-discrete )

assume A2: D0 = D1 ; :: thesis: ( not D0 is anti-discrete or D1 is anti-discrete )

assume A3: D0 is anti-discrete ; :: thesis: D1 is anti-discrete

now :: thesis: for D being Subset of Y1 holds

( not D is open or D1 misses D or D1 c= D )

hence
D1 is anti-discrete
; :: thesis: verum( not D is open or D1 misses D or D1 c= D )

let D be Subset of Y1; :: thesis: ( not D is open or D1 misses D or D1 c= D )

reconsider E = D as Subset of Y0 by A1;

assume D is open ; :: thesis: ( D1 misses D or D1 c= D )

then E in the topology of Y0 by A1, PRE_TOPC:def 2;

then E is open by PRE_TOPC:def 2;

hence ( D1 misses D or D1 c= D ) by A2, A3; :: thesis: verum

end;reconsider E = D as Subset of Y0 by A1;

assume D is open ; :: thesis: ( D1 misses D or D1 c= D )

then E in the topology of Y0 by A1, PRE_TOPC:def 2;

then E is open by PRE_TOPC:def 2;

hence ( D1 misses D or D1 c= D ) by A2, A3; :: thesis: verum