let X be non empty TopSpace; :: thesis: for Y0 being non empty SubSpace of X

for A being Subset of X st A = the carrier of Y0 holds

( Y0 is maximal_anti-discrete iff A is maximal_anti-discrete )

let Y0 be non empty SubSpace of X; :: thesis: for A being Subset of X st A = the carrier of Y0 holds

( Y0 is maximal_anti-discrete iff A is maximal_anti-discrete )

let A be Subset of X; :: thesis: ( A = the carrier of Y0 implies ( Y0 is maximal_anti-discrete iff A is maximal_anti-discrete ) )

assume A1: A = the carrier of Y0 ; :: thesis: ( Y0 is maximal_anti-discrete iff A is maximal_anti-discrete )

thus ( Y0 is maximal_anti-discrete implies A is maximal_anti-discrete ) :: thesis: ( A is maximal_anti-discrete implies Y0 is maximal_anti-discrete )

then Y0 is anti-discrete by A1, Th67;

hence Y0 is maximal_anti-discrete by A8; :: thesis: verum

for A being Subset of X st A = the carrier of Y0 holds

( Y0 is maximal_anti-discrete iff A is maximal_anti-discrete )

let Y0 be non empty SubSpace of X; :: thesis: for A being Subset of X st A = the carrier of Y0 holds

( Y0 is maximal_anti-discrete iff A is maximal_anti-discrete )

let A be Subset of X; :: thesis: ( A = the carrier of Y0 implies ( Y0 is maximal_anti-discrete iff A is maximal_anti-discrete ) )

assume A1: A = the carrier of Y0 ; :: thesis: ( Y0 is maximal_anti-discrete iff A is maximal_anti-discrete )

thus ( Y0 is maximal_anti-discrete implies A is maximal_anti-discrete ) :: thesis: ( A is maximal_anti-discrete implies Y0 is maximal_anti-discrete )

proof

assume A7:
A is maximal_anti-discrete
; :: thesis: Y0 is maximal_anti-discrete
assume A2:
Y0 is maximal_anti-discrete
; :: thesis: A is maximal_anti-discrete

hence A is maximal_anti-discrete by A3; :: thesis: verum

end;A3: now :: thesis: for D being Subset of X st D is anti-discrete & A c= D holds

A = D

A is anti-discrete
by A1, A2, Th66;A = D

let D be Subset of X; :: thesis: ( D is anti-discrete & A c= D implies A = D )

assume A4: D is anti-discrete ; :: thesis: ( A c= D implies A = D )

assume A5: A c= D ; :: thesis: A = D

then D <> {} by A1;

then consider X0 being non empty strict SubSpace of X such that

A6: D = the carrier of X0 by TSEP_1:10;

X0 is anti-discrete by A4, A6, Th67;

hence A = D by A1, A2, A5, A6; :: thesis: verum

end;assume A4: D is anti-discrete ; :: thesis: ( A c= D implies A = D )

assume A5: A c= D ; :: thesis: A = D

then D <> {} by A1;

then consider X0 being non empty strict SubSpace of X such that

A6: D = the carrier of X0 by TSEP_1:10;

X0 is anti-discrete by A4, A6, Th67;

hence A = D by A1, A2, A5, A6; :: thesis: verum

hence A is maximal_anti-discrete by A3; :: thesis: verum

A8: now :: thesis: for X0 being SubSpace of X st X0 is anti-discrete & the carrier of Y0 c= the carrier of X0 holds

the carrier of Y0 = the carrier of X0

A is anti-discrete
by A7;the carrier of Y0 = the carrier of X0

let X0 be SubSpace of X; :: thesis: ( X0 is anti-discrete & the carrier of Y0 c= the carrier of X0 implies the carrier of Y0 = the carrier of X0 )

reconsider D = the carrier of X0 as Subset of X by TSEP_1:1;

assume X0 is anti-discrete ; :: thesis: ( the carrier of Y0 c= the carrier of X0 implies the carrier of Y0 = the carrier of X0 )

then A9: D is anti-discrete by Th66;

assume the carrier of Y0 c= the carrier of X0 ; :: thesis: the carrier of Y0 = the carrier of X0

hence the carrier of Y0 = the carrier of X0 by A1, A7, A9; :: thesis: verum

end;reconsider D = the carrier of X0 as Subset of X by TSEP_1:1;

assume X0 is anti-discrete ; :: thesis: ( the carrier of Y0 c= the carrier of X0 implies the carrier of Y0 = the carrier of X0 )

then A9: D is anti-discrete by Th66;

assume the carrier of Y0 c= the carrier of X0 ; :: thesis: the carrier of Y0 = the carrier of X0

hence the carrier of Y0 = the carrier of X0 by A1, A7, A9; :: thesis: verum

then Y0 is anti-discrete by A1, Th67;

hence Y0 is maximal_anti-discrete by A8; :: thesis: verum