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