let T be non empty RelStr ; :: thesis: for A being Subset of T st T is filled holds
A ^d c= A
let A be Subset of T; :: thesis: ( T is filled implies A ^d c= A )
assume A1: T is filled ; :: thesis: A ^d c= A
thus A ^d c= A :: thesis: verum

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in A ^d or x in A )
assume A2: x in A ^d ; :: thesis: x in A
then reconsider z = x as Element of T ;

now :: thesis: x in A

assume not x in A ; :: thesis: contradiction
then A3: x in A ` by A2, SUBSET_1:29;
x in U_FT z by A1, FIN_TOPO:def 4;
hence contradiction by A2, A3, Th2; :: thesis: verum

end;

hence x in A ; :: thesis: verum

end;