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 discrete holds
D1 is 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 discrete holds
D1 is 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 discrete implies D1 is 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 discrete or D1 is discrete )
assume A2: D0 = D1 ; :: thesis: ( not D0 is discrete or D1 is discrete )
assume A3: D0 is discrete ; :: thesis: D1 is discrete
now :: thesis: for D being Subset of Y1 st D c= D1 holds
ex G being Subset of Y1 st
( G is open & D1 /\ G = D )
let D be Subset of Y1; :: thesis: ( D c= D1 implies ex G being Subset of Y1 st
( G is open & D1 /\ G = D ) )
reconsider E = D as Subset of Y0 by A1;
assume D c= D1 ; :: thesis: ex G being Subset of Y1 st
( G is open & D1 /\ G = D )
then consider G0 being Subset of Y0 such that
A4: G0 is open and
A5: D0 /\ G0 = E by A2, A3;
reconsider G = G0 as Subset of Y1 by A1;
now :: thesis: ex G being Subset of Y1 st
( G is open & D1 /\ G = D )
take G = G; :: thesis: ( G is open & D1 /\ G = D )
G in the topology of Y1 by A1, A4;
hence G is open ; :: thesis: D1 /\ G = D
thus D1 /\ G = D by A2, A5; :: thesis: verum
end;
hence ex G being Subset of Y1 st
( G is open & D1 /\ G = D ) ; :: thesis: verum
end;
hence D1 is discrete ; :: thesis: verum