consider X being non empty strict discrete TopSpace;
take X ; :: thesis: ( X is extremally_disconnected & X is strict )

now

let A be Subset of X; :: thesis: ( A is open implies Cl A is open )
assume A1: A is open ; :: thesis: Cl A is open
A is closed by Th18;
hence Cl A is open by A1, PRE_TOPC:52; :: thesis: verum

end;

hence ( X is extremally_disconnected & X is strict ) by Def4; :: thesis: verum