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 maximal_discrete holds
D1 is maximal_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 maximal_discrete holds
D1 is maximal_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 maximal_discrete implies D1 is maximal_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 maximal_discrete or D1 is maximal_discrete )
assume A2: D0 = D1 ; :: thesis: ( not D0 is maximal_discrete or D1 is maximal_discrete )
assume A3: D0 is maximal_discrete ; :: thesis: D1 is maximal_discrete
then D0 is discrete by Def7;
then A4: D1 is discrete by A1, A2, Th25;

now

let D be Subset of Y1; :: thesis: ( D is discrete & D1 c= D implies D1 = D )
assume A5: D is discrete ; :: thesis: ( D1 c= D implies D1 = D )
assume A6: D1 c= D ; :: thesis: D1 = D
reconsider E = D as Subset of Y0 by A1;
( E is discrete & D0 c= E ) by A1, A2, A5, A6, Th25;
hence D1 = D by A2, A3, Def7; :: thesis: verum

end;

hence D1 is maximal_discrete by A4, Def7; :: thesis: verum