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