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