let o be object ; :: thesis: for p being pair object st Union (sqrtL (p,o)) = {} holds
L_ p = {}
let p be pair object ; :: thesis: ( Union (sqrtL (p,o)) = {} implies L_ p = {} )
assume Union (sqrtL (p,o)) = {} ; :: thesis: L_ p = {}
then (sqrtL (p,o)) . 0 c= {} by ABCMIZ_1:1;
hence L_ p = {} by Th6; :: thesis: verum