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 A c= B ; :: thesis: A ^d c= B ^d
then A1: B ` c= A ` by SUBSET_1:12;
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
then for y being Element of T st y in B ` holds
not z in U_FT y by A1, Th2;
hence z in B ^d by A2; :: thesis: verum