take PreferenceStr(# {{}},({} ({{}},{{}})),({} ({{}},{{}})),({} ({{}},{{}})) #) ; :: thesis: ( not PreferenceStr(# {{}},({} ({{}},{{}})),({} ({{}},{{}})),({} ({{}},{{}})) #) is empty & PreferenceStr(# {{}},({} ({{}},{{}})),({} ({{}},{{}})),({} ({{}},{{}})) #) is strict )
thus ( not PreferenceStr(# {{}},({} ({{}},{{}})),({} ({{}},{{}})),({} ({{}},{{}})) #) is empty & PreferenceStr(# {{}},({} ({{}},{{}})),({} ({{}},{{}})),({} ({{}},{{}})) #) is strict ) ; :: thesis: verum