let T be non empty RelStr ; :: thesis: for A, B being Subset of T st A c= B holds
A ^d c= B ^d
let A, B be Subset of T; :: thesis: ( A c= B implies A ^d c= B ^d )
assume A1: A c= B ; :: thesis: A ^d c= B ^d
let z be set ; :: according to TARSKI:def 3 :: thesis: ( not z in A ^d or z in B ^d )
assume A2: z in A ^d ; :: thesis: z in B ^d
B ` c= A ` by A1, SUBSET_1:31;
then for y being Element of T st y in B ` holds
not z in U_FT y by A2, Th2;
hence z in B ^d by A2; :: thesis: verum