let U be non empty set ; :: thesis: (Inter ({} U),({} U)) ^ = Inter ([#] U),([#] U)
(Inter ({} U),({} U)) ^ = Inter ([#] U),(({} U) ` ) by ThDop1;
hence (Inter ({} U),({} U)) ^ = Inter ([#] U),([#] U) ; :: thesis: verum